[Merged by Bors] - Rename `Mem𝓛p` to `MemLp` by fpvandoorn · Pull Request #22164 · leanprover-community/mathlib4

fpvandoorn · 2025-02-21T14:25:24Z

Search + replace emℒp by emLp
Automatically added deprecations (roughly) by using the regex replace (theorem|lemma|def) ([^ \n]*)emLp([^ \n]*)(((?!\n\n)[\s\S])*)$ >

$1 $2emLp$3$4

@[deprecated (since := "2025-02-21")] 
alias $2em𝓛p$3 := $2emLp$3

Undid unwanted alias replaces by alias ([^ ]*)emLp([^ ]*) > alias $1em𝓛p$2 (but had to manually change some aliases back that were not deprecated)
A few lemmas use 𝓛p to refer to eLpNorm, which are now renamed to use eLpNorm

…ing deprecations

github-actions · 2025-02-21T14:26:23Z

PR summary eedcedfe0d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ AntitoneOn.memLp_isCompact
+ AntitoneOn.memLp_of_measure_ne_top
+ AntitoneOn.memLp_top
+ LipschitzWith.comp_memLp
+ MeasureTheory.MemLp.of_comp_antilipschitzWith
+ MemLp
+ MemLp.add
+ MemLp.ae_eq
+ MemLp.aefinStronglyMeasurable
+ MemLp.aestronglyMeasurable
+ MemLp.comp_measurePreserving
+ MemLp.comp_of_map
+ MemLp.condExp
+ MemLp.condExpL2_ae_eq_condExp
+ MemLp.condExpL2_ae_eq_condExp'
+ MemLp.congr_norm
+ MemLp.const_inner
+ MemLp.const_mul
+ MemLp.const_smul
+ MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero
+ MemLp.eLpNorm_eq_integral_rpow_norm
+ MemLp.eLpNorm_indicator_le
+ MemLp.eLpNorm_indicator_le'
+ MemLp.eLpNorm_indicator_le_of_meas
+ MemLp.eLpNorm_indicator_norm_ge_le
+ MemLp.eLpNorm_indicator_norm_ge_pos_le
+ MemLp.eLpNorm_lt_top
+ MemLp.eLpNorm_mk_lt_top
+ MemLp.eLpNorm_ne_top
+ MemLp.exists_boundedContinuous_eLpNorm_sub_le
+ MemLp.exists_boundedContinuous_integral_rpow_sub_le
+ MemLp.exists_eLpNorm_indicator_compl_lt
+ MemLp.exists_hasCompactSupport_eLpNorm_sub_le
+ MemLp.exists_hasCompactSupport_integral_rpow_sub_le
+ MemLp.finStronglyMeasurable_of_stronglyMeasurable
+ MemLp.im
+ MemLp.indicator
+ MemLp.induction
+ MemLp.induction_dense
+ MemLp.induction_stronglyMeasurable
+ MemLp.inner_const
+ MemLp.integrable
+ MemLp.integrable_mul
+ MemLp.integrable_norm_pow
+ MemLp.integrable_norm_pow'
+ MemLp.integrable_norm_rpow
+ MemLp.integrable_norm_rpow'
+ MemLp.integrable_sq
+ MemLp.integral_indicator_norm_ge_le
+ MemLp.integral_indicator_norm_ge_nonneg_le
+ MemLp.integral_indicator_norm_ge_nonneg_le_of_meas
+ MemLp.isProbabilityMeasure_of_indepFun
+ MemLp.left_of_add_measure
+ MemLp.locallyIntegrable
+ MemLp.meas_ge_lt_top
+ MemLp.meas_ge_lt_top'
+ MemLp.memℒp_of_exponent_le
+ MemLp.memℒp_of_exponent_le_of_measure_support_ne_top
+ MemLp.mono
+ MemLp.mono'
+ MemLp.mono_exponent
+ MemLp.mono_exponent_of_measure_support_ne_top
+ MemLp.mono_measure
+ MemLp.mul
+ MemLp.mul'
+ MemLp.neg
+ MemLp.norm
+ MemLp.norm_rpow
+ MemLp.norm_rpow_div
+ MemLp.of_bilin
+ MemLp.of_bound
+ MemLp.of_discrete
+ MemLp.of_le
+ MemLp.of_le_mul
+ MemLp.of_measure_le_smul
+ MemLp.of_nnnorm_le_mul
+ MemLp.piecewise
+ MemLp.prod
+ MemLp.prod'
+ MemLp.re
+ MemLp.restrict
+ MemLp.right_of_add_measure
+ MemLp.smul
+ MemLp.smul_measure
+ MemLp.sub
+ MemLp.toLp_const
+ MemLp.uniformIntegrable_of_identDistrib
+ MemLp.uniformIntegrable_of_identDistrib_aux
+ MemLp.zero
+ MemLp.zero'
+ MonotoneOn.memLp_isCompact
+ MonotoneOn.memLp_of_measure_ne_top
+ MonotoneOn.memLp_top
+ Submartingale.memLp_limitProcess
+ _root_.Continuous.memLp_of_hasCompactSupport
+ _root_.Continuous.memLp_top_of_hasCompactSupport
+ _root_.HasCompactSupport.memLp_of_bound
+ _root_.MeasurableEmbedding.memLp_map_measure_iff
+ _root_.MeasurableEquiv.memLp_map_measure_iff
+ _root_.MeasureTheory.AEStronglyMeasurable.memLp_truncation
+ _root_.MeasureTheory.MemLp.abs
+ _root_.MeasureTheory.MemLp.evariance_lt_top
+ _root_.MeasureTheory.MemLp.evariance_ne_top
+ _root_.MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt
+ _root_.MeasureTheory.MemLp.inf
+ _root_.MeasureTheory.MemLp.neg_part
+ _root_.MeasureTheory.MemLp.ofReal
+ _root_.MeasureTheory.MemLp.ofReal_variance_eq
+ _root_.MeasureTheory.MemLp.pos_part
+ _root_.MeasureTheory.MemLp.sup
+ _root_.MeasureTheory.memLp_re_im_iff
+ cauchySeq_Lp_iff_cauchySeq_eLpNorm
+ cauchy_complete_eLpNorm
+ comp_memLp
+ comp_memLp'
+ completeSpace_lp_of_cauchy_complete_eLpNorm
+ evariance_lt_top_iff_memLp
+ measure_lt_top_of_memLp_indicator
+ measure_preimage_lt_top_of_memLp
+ measure_support_lt_top_of_memLp
+ memL1_smul_of_L1_withDensity
+ memL1_smul_of_ℒ1_withDensity
+ memLp_add_of_disjoint
+ memLp_approxOn
+ memLp_approxOn_range
+ memLp_comp_iff_of_antilipschitz
+ memLp_congr_ae
+ memLp_congr_norm
+ memLp_const
+ memLp_const_iff
+ memLp_finset_sum
+ memLp_finset_sum'
+ memLp_iff_finMeasSupp
+ memLp_iff_integrable
+ memLp_indicator_const
+ memLp_indicator_iff_restrict
+ memLp_limitProcess_of_eLpNorm_bdd
+ memLp_lineDeriv
+ memLp_map_measure_iff
+ memLp_measure_zero
+ memLp_neg_iff
+ memLp_norm_iff
+ memLp_norm_rpow_iff
+ memLp_of_bounded
+ memLp_of_cauchy_tendsto
+ memLp_of_finite_measure_preimage
+ memLp_of_isFiniteMeasure
+ memLp_of_memLp_trim
+ memLp_of_mem_interior_integrableExpSet
+ memLp_one_iff_integrable
+ memLp_snd
+ memLp_stoppedProcess
+ memLp_stoppedProcess_of_mem_finset
+ memLp_stoppedValue
+ memLp_stoppedValue_of_mem_finset
+ memLp_top_const
+ memLp_top_of_bound
+ memLp_trim_of_mem_lpMeasSubgroup
+ memLp_two_iff_integrable_sq
+ memLp_two_iff_integrable_sq_norm
+ memLp_zero
+ memLp_zero_iff_aestronglyMeasurable
+ mem_L1_toReal_of_lintegral_ne_top
+ mem_Lp_iff_memLp
+ tendsto_Lp_iff_tendsto_eLpNorm
+ tendsto_Lp_iff_tendsto_eLpNorm'
+ tendsto_Lp_iff_tendsto_eLpNorm''
+ tendsto_Lp_of_tendsto_eLpNorm
++ memLp_iff
++ memLp_top
++++ memLp
++---- memℒp
+-+- norm_toLp
+-+- toLp
+-+- toLp_add
+-+- toLp_neg
+-+- toLp_sub
+-+- toLp_zero
+-- memℒp_iff
+-- memℒp_top
- Memℒp.add
- Memℒp.eLpNormEssSup_indicator_norm_ge_eq_zero
- Memℒp.eLpNorm_indicator_le
- Memℒp.eLpNorm_indicator_le'
- Memℒp.eLpNorm_indicator_le_of_meas
- Memℒp.eLpNorm_indicator_norm_ge_le
- Memℒp.eLpNorm_indicator_norm_ge_pos_le
- Memℒp.induction
- Memℒp.induction_dense
- Memℒp.integrable
- Memℒp.integrable_mul
- Memℒp.integrable_norm_pow
- Memℒp.integrable_norm_pow'
- Memℒp.integrable_norm_rpow
- Memℒp.integrable_norm_rpow'
- Memℒp.integral_indicator_norm_ge_le
- Memℒp.integral_indicator_norm_ge_nonneg_le
- Memℒp.integral_indicator_norm_ge_nonneg_le_of_meas
- Memℒp.memℒp_of_exponent_le
- Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top
- Memℒp.sub
- _root_.MeasureTheory.AEStronglyMeasurable.memℒp_truncation
- _root_.MeasureTheory.Memℒp.exists_simpleFunc_eLpNorm_sub_lt
- measure_lt_top_of_memℒp_indicator
- measure_preimage_lt_top_of_memℒp
- measure_support_lt_top_of_memℒp
- memℒ1_smul_of_L1_withDensity
- memℒp_approxOn
- memℒp_approxOn_range
- memℒp_finset_sum
- memℒp_finset_sum'
- memℒp_iff_finMeasSupp
- memℒp_iff_integrable
- memℒp_of_finite_measure_preimage
- memℒp_of_isFiniteMeasure
- memℒp_one_iff_integrable
- memℒp_stoppedProcess
- memℒp_stoppedProcess_of_mem_finset
- memℒp_stoppedValue
- memℒp_stoppedValue_of_mem_finset
- memℒp_zero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.02)

Current number	Change	Type
43	1	large files

Current commit eedcedfe0d
Reference commit 5949d4d779

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

EtienneC30 · 2025-02-21T19:24:51Z

Thanks!
maintainer merge

github-actions · 2025-02-21T19:25:13Z

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

sgouezel · 2025-02-21T20:26:26Z

bors r+

* Search + replace `emℒp` by `emLp` * Automatically added deprecations (roughly) by using the regex replace `(theorem|lemma|def) ([^ \n]*)emLp([^ \n]*)(((?!\n\n)[\s\S])*)$` > ``` $1 $2emLp$3$4 @[deprecated (since := "2025-02-21")] alias $2em𝓛p$3 := $2emLp$3 ``` * Undid unwanted alias replaces by `alias ([^ ]*)emLp([^ ]*)` > `alias $1em𝓛p$2` (but had to manually change some aliases back that were not deprecated) * A few lemmas use `𝓛p` to refer to `eLpNorm`, which are now renamed to use `eLpNorm`

mathlib-bors · 2025-02-21T20:47:19Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: chore(*): add `@[fun_prop]` (#22183) chore(RingTheory): generalize universes for `isUnramified_iff_map_eq` (#22185) chore(Algebra/GroupPower/IterateHom): move all lemmas earlier (#22132) feat(Probability): ae filter and integrability wrt a composition of kernel and measure (#22074) feat(CategoryTheory): forgetting the group structure on the codomain of left-exact functors (#21973) feat(CategoryTheory): embeddings for opposites of Grothendieck abelian categories (#22182) feat(CategoryTheory): `AsSmall C` is abelian (#22184) feat(CategoryTheory): explicit argument versions of `epi_comp` and `mono_comp` (#22181) feat(Topology/Instances/EReal/Lemmas): add lemmas about limsup and multiplication (#21833) feat: basic structural lemmas about finite crystallographic root pairings. (#21932) Rename `Mem𝓛p` to `MemLp` (#22164) feat(Logic/Equiv): Upgrade arrowProdEquivProdArrow to dependent types (#21518) feat(CategoryTheory): Grothendieck abelian categories have enough injectives (#20079) chore: deprecate Finite.cast_card_eq_mk (#22161) feat(CategoryTheory/Limits/Fubini): relax `HasLimits` hypotheses (#20570) chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up (#22109)

fpvandoorn added 3 commits February 21, 2025 15:07

rename MemLp

a525878

deprecate theorems as well

9025db7

undo changes to aliases, undo some accidental newlines, add some miss…

fb346e8

…ing deprecations

fpvandoorn added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 21, 2025

fpvandoorn added 5 commits February 21, 2025 15:33

some aliases do need to be renamed...

2d16bca

fix

dbc15e3

fix

ca6b949

Oh, I used the wrong L, and a few more renames

aed438e

a few more renames

eedcedf

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 21, 2025

Parcly-Taxel approved these changes Feb 21, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 21, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 21, 2025

mathlib-bors bot changed the title ~~Rename Mem𝓛p to MemLp~~ [Merged by Bors] - Rename Mem𝓛p to MemLp Feb 21, 2025

mathlib-bors bot closed this Feb 21, 2025

mathlib-bors bot deleted the MemLp branch February 21, 2025 20:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - Rename `Mem𝓛p` to `MemLp`#22164

[Merged by Bors] - Rename `Mem𝓛p` to `MemLp`#22164
fpvandoorn wants to merge 8 commits intomasterfrom
MemLp

fpvandoorn commented Feb 21, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Feb 21, 2025 •

edited

Loading

Declarations diff

Uh oh!

EtienneC30 commented Feb 21, 2025

Uh oh!

github-actions bot commented Feb 21, 2025

Uh oh!

sgouezel commented Feb 21, 2025

Uh oh!

mathlib-bors bot commented Feb 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

fpvandoorn commented Feb 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary eedcedfe0d

Import changes for modified files

Declarations diff

Uh oh!

EtienneC30 commented Feb 21, 2025

Uh oh!

github-actions bot commented Feb 21, 2025

Uh oh!

sgouezel commented Feb 21, 2025

Uh oh!

mathlib-bors bot commented Feb 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

fpvandoorn commented Feb 21, 2025 •

edited

Loading

github-actions bot commented Feb 21, 2025 •

edited

Loading