Rearrangement.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

52 declarations, 0 contain sorry, 0 declared as axioms

Decreasing rearrangements `f^#`

Imports (3)

Imported by 2 files

def MeasureTheory.rearrangement The decreasing rearrangement function f^# line 30 source
Source documentation
The decreasing rearrangement function f^#. It equals μ univ for t = 0. Note that unlike the notes, we also define this for t = ∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, ENNReal, MeasureTheory.Measure
Proof uses: InfSet.sInf, Set.ofPred, LE.le, MeasureTheory.distribution
8 instances, coercions and auxiliary constants left out.
```
def rearrangement (f : α → ε) (t : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ :=
…
```
lemma MeasureTheory.rearrangement_top line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Eq, ENNReal, MeasureTheory.rearrangement, Top.top, OfNat.ofNat
Proof uses: id, of_eq_true, InfSet.sInf, Set.ofPred, LE.le, MeasureTheory.distribution, Eq.trans, True, congrFun', congrArg, Bot.bot, Set.univ, Set, funext, sInf_univ, bot_eq_zero', eq_self
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_eq_zero_of_ae_zero_enorm line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Filter.EventuallyEq, MeasureTheory.ae, Function.comp, ENorm.enorm, OfNat.ofNat, Eq, MeasureTheory.rearrangement
Proof uses: id, Eq.mpr, InfSet.sInf, Set.ofPred, LE.le, MeasureTheory.distribution, congrFun', congrArg, Set, funext, MeasureTheory.distribution_eq_zero_of_ae_zero_enorm, of_eq_true, Eq.trans, True, Bot.bot, Set.univ, sInf_univ, bot_eq_zero', eq_self
39 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_eq_zero_of_ae_zero line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Filter.EventuallyEq, MeasureTheory.ae, OfNat.ofNat, Eq, MeasureTheory.rearrangement
Proof uses: MeasureTheory.rearrangement_eq_zero_of_ae_zero_enorm, Filter.mp_mem, Set.ofPred, Function.comp, ENorm.enorm, Filter.univ_mem', Membership.mem, Set, id, of_eq_true, Eq.trans, True, congrFun', congrArg, enorm_zero, eq_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_zero line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ENormedAddMonoid, Eq, MeasureTheory.rearrangement, OfNat.ofNat
Proof uses: MeasureTheory.rearrangement_eq_zero_of_ae_zero, MeasureTheory.ae_eq_rfl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_antitone' line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.rearrangement
Proof uses: sInf_le_sInf, Set.ofPred, MeasureTheory.distribution, Membership.mem, Set, LE.le.trans, Membership.mem.out
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_antitone line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Antitone, ENNReal, MeasureTheory.rearrangement
Proof uses: LE.le, MeasureTheory.rearrangement_antitone'
5 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.rearrangement_mono_fun line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Filter.Eventually, LE.le, ENorm.enorm, MeasureTheory.ae, MeasureTheory.rearrangement
Proof uses: sInf_le_sInf, Set.ofPred, MeasureTheory.distribution, Membership.mem, Set, LE.le.trans, MeasureTheory.distribution_mono_left
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_le_rearrangement line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Filter.Eventually, LE.le, ENorm.enorm, MeasureTheory.ae, MeasureTheory.rearrangement
Proof uses: le_trans, MeasureTheory.rearrangement_antitone', MeasureTheory.rearrangement_mono_fun
8 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.rearrangment_eq_rearrangement_of_distribution_eq_distribution line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Eq, MeasureTheory.distribution, MeasureTheory.rearrangement
Proof uses: id, of_eq_true, InfSet.sInf, Set.ofPred, LE.le, Eq.trans, True, congrFun', congrArg, Set, funext, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_measurable₀ line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Measurable, ENNReal, MeasureTheory.rearrangement
Proof uses: Antitone.measurable, MeasureTheory.rearrangement_antitone
8 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.rearrangement_measurable line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Measurable, MeasureTheory.rearrangement
Proof uses: Measurable.fun_comp, MeasureTheory.rearrangement_measurable₀
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_distribution_le line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.rearrangement, MeasureTheory.distribution
Proof uses: sInf_le, Set.ofPred, of_eq_true
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_rearrangement_le line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.distribution, MeasureTheory.rearrangement
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, OfNat.ofNat, True, congrFun', congrArg, MeasureTheory.distibution_top, Not, GT.gt, HAdd.hAdd, Exists, And, Membership.mem, Set, Set.ofPred, LT.lt, InfSet.sInf and 46 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lt_rearrangement_iff_lt_distribution Lemma 1.1.22 of [Ian Tice] line 118 source
Source comment
Lemma 1.1.22 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Iff, LT.lt, MeasureTheory.rearrangement, MeasureTheory.distribution
Proof uses: Iff.intro, id, InfSet.sInf, Set.ofPred, LE.le, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, Eq, implies_congr, sInf_le, Membership.mem, Set, Trans.trans, rfl, MeasureTheory.distribution_mono_right, MeasureTheory.distribution_rearrangement_le
24 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma lt_rearrangement_iff_lt_distribution {f : α → ε} {μ : Measure α} {t : ℝ≥0∞} {y : ℝ≥0∞} :
    y < rearrangement f t μ ↔ t < distribution f y μ := by
…
```
Mentions: MeasureTheory.rearrangement, MeasureTheory.distribution
lemma MeasureTheory.rearrangement_le_iff_distribution_le line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Iff, LE.le, MeasureTheory.rearrangement, MeasureTheory.distribution
Proof uses: Mathlib.Tactic.Contrapose.contrapose_iff₁, Eq.mpr, Not, LT.lt, id, Eq, congr, congrArg, MeasureTheory.lt_rearrangement_iff_lt_distribution
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_rearrangement_eq_distribution line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Eq, MeasureTheory.distribution, MeasureTheory.rearrangement, MeasureTheory.MeasureSpace.volume
Proof uses: id, Set, Set.ofPred, LT.lt, ENorm.enorm, Set.Iio, Set.ext, Eq.mpr, Iff, Membership.mem, congrArg, MeasureTheory.lt_rearrangement_iff_lt_distribution, ENNReal.volume_Iio, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.support_rearrangement_eq line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, Eq, Set, ENNReal, Function.support, MeasureTheory.rearrangement, Set.Iio
Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Not, OfNat.ofNat, LT.lt, id, congr, congrArg, MeasureTheory.distribution, Eq.symm, MeasureTheory.distribution_zero_eq_measure_support, propext, MeasureTheory.lt_rearrangement_iff_lt_distribution, of_eq_true, Ne, Eq.trans, LE.le, True
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ae_eq_zero_of_rearrangement_ae_eq_zero line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement, OfNat.ofNat
Proof uses: id, Eq, Set, Function.support, Eq.mp, Set.Iio, congrArg, ENNReal.volume_Iio, MeasureTheory.support_rearrangement_eq
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.continuousWithinAt_rearrangement Lemma 1.1.22 of [Ian Tice] line 165 source
Source comment
Lemma 1.1.22 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, ContinuousWithinAt, MeasureTheory.rearrangement, Set.Ici
Proof uses: Iff.mpr, Filter.Tendsto, nhdsWithin, nhds, And, LT.lt, Filter.Eventually, GT.gt, tendsto_order, And.intro, MeasureTheory.distribution, Iff.mp, MeasureTheory.lt_rearrangement_iff_lt_distribution, Eq.mpr, Membership.mem, Set, id, Eq, congrArg, propext and 9 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma continuousWithinAt_rearrangement :
    ContinuousWithinAt (rearrangement f · μ) (Set.Ici x) x := by
…
```
Mentions: MeasureTheory.rearrangement
lemma MeasureTheory.rearrangement_eq_rearrangement_prod line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, ENNReal, MeasureTheory.IsProbabilityMeasure, Eq, MeasureTheory.rearrangement, Prod, Prod.fst, MeasureTheory.Measure.prod
Proof uses: MeasureTheory.rearrangment_eq_rearrangement_of_distribution_eq_distribution, MeasureTheory.distribution_eq_distribution_prod
2 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_indicator_le Lemma 1.1.24 of [Ian Tice] line 186 source
Source comment
Lemma 1.1.24 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Set, LE.le, MeasureTheory.rearrangement, Set.indicator, Set.Iio
Proof uses: Eq.mpr, MeasureTheory.distribution, id, Eq, congrArg, propext, MeasureTheory.rearrangement_le_iff_distribution_le, ite, Membership.mem, OfNat.ofNat, Set.indicator_apply, dite, congrFun', ite_eq_left, LE.le.trans, MeasureTheory.distribution_mono_left, Filter.univ_mem', MeasureTheory.ae, Set.ofPred, ENorm.enorm and 12 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma rearrangement_indicator_le {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε}
  {X : Set α} :
    rearrangement (X.indicator f) x μ ≤
      Set.indicator (Set.Iio (μ X)) (rearrangement f · μ) x := by
…
```
Mentions: MeasureTheory.rearrangement
lemma MeasureTheory.rearrangement_indicator_const line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Set, Eq, MeasureTheory.rearrangement, Set.indicator, Function.const, Set.Iio, ENorm.enorm
Proof uses: id, Eq.mpr, InfSet.sInf, Set.ofPred, LE.le, MeasureTheory.distribution, congrFun', congrArg, funext, MeasureTheory.distribution_indicator_const, ite, Membership.mem, Classical.decPred, OfNat.ofNat, LT.lt, congr, ite_congr, Eq.refl, Not, ite.congr_simp and 22 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_const_smul line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Eq, MeasureTheory.rearrangement, HSMul.hSMul, HMul.hMul
Proof uses: dite, OfNat.ofNat, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congr, congrFun', zero_smul, MeasureTheory.rearrangement_zero, MulZeroClass.zero_mul, eq_self, Not, Top.top, Set.indicator, Function.support, Function.const, funext and 41 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_indicator_superlevelSet line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ENormedAddMonoid, Eq, MeasureTheory.rearrangement, Set.indicator, MeasureTheory.superlevelSet
Proof uses: Eq.mpr, InfSet.sInf, Set.ofPred, LE.le, MeasureTheory.distribution, id, congrArg, MeasureTheory.rearrangement.eq_1, Min.min, congrFun', Set, funext, MeasureTheory.distribution_indicator_superlevelSet, Or, ite, Membership.mem, Classical.decPred, OfNat.ofNat, LT.lt, ENorm.enorm and 24 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_indicator_superlevelSet_compl line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Ne, MeasureTheory.distribution, Top.top, Eq, MeasureTheory.rearrangement, Set.indicator, Compl.compl, Set, MeasureTheory.superlevelSet, HAdd.hAdd
Proof uses: Eq.mpr, InfSet.sInf, Set.ofPred, LE.le, id, congrArg, MeasureTheory.rearrangement.eq_1, HSub.hSub, congrFun', funext, MeasureTheory.distribution_indicator_superlevelSet_compl, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite' line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, LT.lt, ENNReal, Set, Function.support, Top.top, MeasurableSet, Eq, Set.ofPred, Membership.mem, SDiff.sdiff, Singleton.singleton, OfNat.ofNat, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: MeasurableSpace.induction_on_inter, borel, Set.range, Set.Ioi, borel_eq_generateFrom_Ioi, isPiSystem_Ioi, of_eq_true, EmptyCollection.emptyCollection, Eq.trans, True, congr, congrArg, False, funext, congrFun', Set.sdiff_singleton_eq_self, Not, not_false_eq_true, MeasureTheory.measure_empty, eq_self and 64 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 100 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite line 395 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, LT.lt, ENNReal, Set, Function.support, Top.top, MeasurableSet, Not, Membership.mem, OfNat.ofNat, Eq, Set.ofPred, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: SDiff.sdiff, Singleton.singleton, of_eq_true, Eq.trans, True, congrArg, Set.sdiff_singleton_eq_self, False, eq_false, not_false_eq_true, eq_self, Eq.mpr, id, MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite'
40 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem' line 404 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Set, ENNReal, MeasurableSet, Not, Membership.mem, OfNat.ofNat, Exists, And, LT.lt, MeasureTheory.distribution, Top.top, Eq, Set.ofPred, ENorm.enorm, MeasureTheory.MeasureSpace.volume and 1 more
Proof uses: Set.indicator, MeasureTheory.superlevelSet, Set.ext, id, Iff, ite, Classical.decPred, Iff.intro, of_eq_true, Eq.trans, True, congrArg, ite_eq_left_of_eq_true, eq_true, Decidable, False.elim, Eq.mp, False, enorm_zero, eq_false and 26 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_enorm_eq_eq_volume_rearrangement_eq line 426 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ENNReal, Ne, MeasureTheory.distribution, Top.top, Eq, Set, Set.ofPred, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: Eq.mpr, LE.le, id, congrArg, Eq.symm, propext, top_le_iff, Trans.trans, MeasureTheory.Measure.map, HAdd.hAdd, rfl, Set.indicator, Compl.compl, MeasureTheory.superlevelSet, funext, congrFun', MeasureTheory.rearrangement_indicator_superlevelSet_compl, Set.Iio, ENNReal.volume_Iio, MeasureTheory.measure_mono and 51 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem line 474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Set, ENNReal, MeasurableSet, Not, Membership.mem, OfNat.ofNat, InfSet.sInf, LT.lt, MeasureTheory.distribution, Top.top, Eq, Set.ofPred, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: dite, EmptyCollection.emptyCollection, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congr, False, funext, MeasureTheory.measure_empty, eq_self, BddBelow, Nat, And, Antitone, Filter.Tendsto, Filter.atTop, nhds and 60 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 95 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement' line 556 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ENNReal, Measurable, Eq, OfNat.ofNat, Exists, And, LE.le, LT.lt, MeasureTheory.distribution, Top.top, ENorm.enorm, Function.comp, MeasureTheory.rearrangement, MeasureTheory.MeasureSpace.volume
Proof uses: id, Set, Set.ofPred, Trans.trans, Membership.mem, Set.preimage, Set.Ioi, rfl, Eq.refl, MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem', MeasurableSet, measurableSet_preimage, measurableSet_Ioi, of_eq_true, Not, Eq.trans, False, True, congrArg, not_false_eq_true and 8 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement line 573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ENNReal, GT.gt, OfNat.ofNat, LT.lt, MeasureTheory.distribution, Top.top, Measurable, Eq, ENorm.enorm, Function.comp, MeasureTheory.rearrangement, MeasureTheory.MeasureSpace.volume
Proof uses: dite, Ne, InfSet.sInf, Set.preimage, Set.Ioi, MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement', And, Exists, LE.le, exists_between, Eq.mp, Bot.bot, congrArg, ENNReal.bot_eq_zero, Eq.symm, propext, bot_lt_iff_ne_bot, Exists.intro, Eq.mpr, id and 26 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_comp_rearrangement' line 602 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ENNReal, Measurable, Eq, OfNat.ofNat, GT.gt, MeasureTheory.distribution, Top.top, Exists, And, LT.lt, MeasureTheory.lintegral, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: InfSet.sInf, Set.ofPred, Eq.mpr, id, congrArg, MeasureTheory.lintegral_eq_lintegral_distribution, Measurable.comp_aemeasurable', MeasureTheory.AEStronglyMeasurable.enorm, Eq.symm, Measurable.aemeasurable, MeasureTheory.rearrangement_measurable, measurable_id', dite, Eq.rec, Eq.refl, funext, MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement, Membership.mem, Set, Eq.mp and 45 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_comp_rearrangement_of_distribution_finite line 679 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ENNReal, GT.gt, OfNat.ofNat, Ne, MeasureTheory.distribution, Top.top, Measurable, Eq, MeasureTheory.lintegral, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: MeasureTheory.lintegral_comp_rearrangement', False.elim, Exists, And, LT.lt
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_comp_rearrangement line 688 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ENNReal, Measurable, Eq, OfNat.ofNat, GT.gt, Exists, And, LT.lt, MeasureTheory.lintegral, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: MeasureTheory.lintegral_comp_rearrangement', MeasureTheory.distribution, Top.top
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_comp_rearrangement_of_strictmono line 696 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ENNReal, Measurable, Eq, OfNat.ofNat, StrictMono, MeasureTheory.lintegral, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement
Proof uses: MeasureTheory.lintegral_comp_rearrangement, GT.gt, Exists.intro, And, LT.lt, Eq.mpr, id, congrArg, Eq.symm, And.intro
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_rearrangement_pow Lemma 1.1.22 of [Ian Tice] line 709 source
Source comment
Lemma 1.1.22 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Real, LT.lt, OfNat.ofNat, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, HPow.hPow, MeasureTheory.rearrangement, ENorm.enorm
Proof uses: Eq.symm, MeasureTheory.lintegral_comp_rearrangement_of_strictmono, Measurable.pow_const, measurable_id', Eq.mpr, id, Eq.trans, Or, And, Top.top, False, congr, congrArg, True, congrFun', eq_self, true_and, false_and, or_false, ENNReal.strictMono_rpow_of_pos
27 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_rearrangement_pow {ε} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε}
  (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 0 < p) :
    ∫⁻ t, (rearrangement f t μ) ^ p = ∫⁻ x, ‖f x‖ₑ ^ p ∂μ := by
…
```
Mentions: MeasureTheory.rearrangement
lemma MeasureTheory.lintegral_rearrangement line 716 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, MeasureTheory.rearrangement, ENorm.enorm
Proof uses: HPow.hPow, Real, OfNat.ofNat, MeasureTheory.lintegral_rearrangement_pow, zero_lt_one, Eq.mp, congr, congrArg, funext, ENNReal.rpow_one
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rearrangement_add_le line 725 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, LE.le, MeasureTheory.rearrangement, HAdd.hAdd
Proof uses: csInf_le', Set.ofPred, MeasureTheory.distribution, le_trans, MeasureTheory.distribution_add_le, add_le_add, MeasureTheory.distribution_rearrangement_le
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.sSup_rearrangement Lemma 1.1.22 of [Ian Tice] line 732 source
Source comment
Lemma 1.1.22 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Eq, ENNReal, iSup, GT.gt, OfNat.ofNat, MeasureTheory.rearrangement
Proof uses: ContinuousWithinAt, Set.Ici, MeasureTheory.continuousWithinAt_rearrangement, Eq.mpr, id, congrArg, iSup_eq_of_forall_le_of_forall_lt_exists_gt, LE.le, LT.lt, Eq.trans, congrFun', iSup_congr_Prop, Iff.of_eq, Eq.refl, MeasureTheory.rearrangement_antitone', LT.lt.le, Filter.Eventually, And, nhdsWithin, Set.Ioi and 16 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma sSup_rearrangement :
    ⨆ t > 0, rearrangement f t μ = rearrangement f 0 μ := by
…
```
Mentions: MeasureTheory.rearrangement
lemma MeasureTheory.rearrangement_zero_eq_eLpNormEssSup Lemma 1.1.22 of [Ian Tice] line 750 source
Source comment
Lemma 1.1.22 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Eq, ENNReal, MeasureTheory.rearrangement, OfNat.ofNat, MeasureTheory.eLpNormEssSup
Proof uses: id, essSup, ENorm.enorm, Filter.limsup, MeasureTheory.ae, InfSet.sInf, Set.ofPred, LE.le, MeasureTheory.distribution, of_eq_true, Set, LT.lt, Eq.trans, True, congr, congrArg, funext, Filter.Eventually, Not, congrFun' and 1 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma rearrangement_zero_eq_eLpNormEssSup :
    rearrangement f 0 μ = eLpNormEssSup f μ  := by
…
```
Mentions: MeasureTheory.rearrangement
lemma MeasureTheory.eLpNorm'_rearrangement line 767 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Real, LT.lt, OfNat.ofNat, Eq, ENNReal, MeasureTheory.eLpNorm', MeasureTheory.rearrangement, MeasureTheory.MeasureSpace.volume
Proof uses: id, Eq.mpr, HPow.hPow, MeasureTheory.lintegral, ENorm.enorm, HDiv.hDiv, Inv.inv, congr, congrArg, one_div, MeasureTheory.lintegral_rearrangement_pow, Eq.refl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.setLIntegral_enorm_le_lintegral_rearrangement Lemma 1.1.24 of [Ian Tice] line 815 source
Source comment
Lemma 1.1.24 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Set, MeasurableSet, LE.le, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, ENorm.enorm, MeasureTheory.MeasureSpace.volume, Set.Iio, MeasureTheory.rearrangement
Proof uses: Eq.mpr, Set.indicator, id, Eq, congrArg, Eq.symm, MeasureTheory.lintegral_indicator, measurableSet_Iio, Function.comp, funext, of_eq_true, eq_self, Set.indicator_comp_of_zero, enorm_zero, MeasureTheory.lintegral_rearrangement, MeasureTheory.AEStronglyMeasurable.indicator₀, MeasureTheory.NullMeasurableSet, MeasureTheory.lintegral_mono_fn', le_refl, MeasureTheory.rearrangement_indicator_le
38 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma setLIntegral_enorm_le_lintegral_rearrangement {ε} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε}
  (hf : AEStronglyMeasurable f μ) {X : Set α} (hX : MeasurableSet X) :
    ∫⁻ x in X, ‖f x‖ₑ ∂μ ≤
      ∫⁻ t in (Set.Iio (μ X)), rearrangement f t μ := by
…
```
Mentions: MeasureTheory.rearrangement
lemma MeasureTheory.setLIntegral_enorm_eq line 829 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Set, MeasureTheory.NullMeasurableSet, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, ENorm.enorm, MeasureTheory.MeasureSpace.volume, Inter.inter, Set.ofPred, LT.lt
Proof uses: Eq.mpr, Set.indicator, id, congrArg, Eq.symm, MeasureTheory.lintegral_indicator₀, MeasureTheory.distribution, MeasureTheory.lintegral_eq_lintegral_distribution, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.indicator₀, Continuous.comp_aestronglyMeasurable, Continuous.enorm, continuous_id', Eq.rec, Eq.refl, funext, eq_of_heq, HEq, DFunLike, HEq.refl and 25 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.setLIntegral_eq line 843 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, AEMeasurable, Set, MeasureTheory.NullMeasurableSet, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Inter.inter, Set.ofPred, LT.lt
Proof uses: Eq.mpr, ENorm.enorm, id, congrFun', congrArg, funext, Eq.trans, Eq.symm, enorm_eq_self, Eq.refl, MeasureTheory.setLIntegral_enorm_eq, AEMeasurable.aestronglyMeasurable, of_eq_true, eq_self
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_rearrangement_eq' line 851 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Iio, MeasureTheory.rearrangement, Min.min, MeasureTheory.distribution
Proof uses: Eq.mpr, id, congrArg, MeasureTheory.lintegral_eq_lintegral_distribution, Measurable.aemeasurable, MeasureTheory.rearrangement_measurable, measurable_id', Eq.rec, Eq.refl, funext, Set, Set.ofPred, LT.lt, ENorm.enorm, Inter.inter, congrFun', MeasureTheory.Measure.restrict_apply', of_eq_true, MeasurableSet, Set.Iio_inter_Iio and 1 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_rearrangement_eq'' line 861 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Iio, MeasureTheory.distribution, MeasureTheory.rearrangement, Set.ofPred, LT.lt, ENorm.enorm
Proof uses: Eq.mpr, Min.min, id, congrArg, MeasureTheory.lintegral_rearrangement_eq', Set, Inter.inter, MeasureTheory.setLIntegral_eq, MeasureTheory.AEStronglyMeasurable.enorm, nullMeasurableSet_lt, Measurable.aemeasurable, measurable_const, Eq.rec, Eq.refl, funext, Max.max, Eq.symm, Antitone.map_max, MeasureTheory.distribution_mono_right', eq_of_heq and 16 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_rearrangement_eq Theorem 4.17 in https://doi.org/10.1007/978-3-319-30034-4 line 874 source
Source comment
Theorem 4.17 in https://doi.org/10.1007/978-3-319-30034-4

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.NoAtoms', MeasureTheory.AEStronglyMeasurable, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Iio, MeasureTheory.rearrangement, iSup, Set, MeasureTheory.NullMeasurableSet, LE.le, ENorm.enorm
Proof uses: Eq.mpr, Min.min, MeasureTheory.distribution, id, congrArg, MeasureTheory.lintegral_rearrangement_eq', le_antisymm, dite, OfNat.ofNat, le_iSup_of_le, MeasureTheory.superlevelSet, MeasureTheory.nullMeasurableSet_superlevelSet, Eq.mp, Bot.bot, ENNReal.bot_eq_zero, propext, MeasureTheory.rearrangement_le_iff_distribution_le, Eq.symm, le_bot_iff, Inter.inter and 99 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 113 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_rearrangement_eq {ε} [TopologicalSpace ε] [ContinuousENorm ε] [NoAtoms' μ] {f : α → ε}
  (hf : AEStronglyMeasurable f μ) {t : ℝ≥0∞} :
    ∫⁻ s in Set.Iio t, rearrangement f s μ
      = ⨆ (E : Set α) (_ : NullMeasurableSet E μ) (_ : μ E ≤ t), ∫⁻ x in E, ‖f x‖ₑ ∂μ := by
…
```
Mentions: MeasureTheory.NoAtoms', s, MeasureTheory.rearrangement, E
lemma MeasureTheory.lintegral_rearrangement_eq_and line 987 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.NoAtoms', MeasureTheory.AEStronglyMeasurable, ENNReal, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Iio, MeasureTheory.rearrangement, iSup, Set, And, MeasureTheory.NullMeasurableSet, LE.le, ENorm.enorm
Proof uses: Eq.mpr, id, congrArg, MeasureTheory.lintegral_rearrangement_eq, SupSet, Eq.rec, Eq.refl, funext, iSup_and'
34 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Antitone.lintegral_withDensity_le line 994 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Antitone, AEMeasurable, MeasureTheory.MeasureSpace.volume, LE.le, OfNat.ofNat, MeasureTheory.lintegral, MeasureTheory.Measure.withDensity, MeasureTheory.Measure.restrict, Set.Iio
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, dite, Top.top, HMul.hMul, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀', MeasureTheory.AEMeasurable.withDensity, Trans.trans, HAdd.hAdd, Singleton.singleton, Set, Set.univ, of_eq_true, Eq.trans, True, congrFun', MeasureTheory.Measure and 90 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 118 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_rearrangement_add_rearrangement_le_add_lintegral Remark 4.18 in https://doi.org/10.1007/978-3-319-30034-4 line 1147 source
Source comment
Remark 4.18 in https://doi.org/10.1007/978-3-319-30034-4

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, TopologicalSpace, ESeminormedAddMonoid, ContinuousAdd, MeasureTheory.AEStronglyMeasurable, ENNReal, LE.le, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Iio, MeasureTheory.rearrangement, HAdd.hAdd
Proof uses: MeasureTheory.NoAtoms', Not, Or, Classical.em, Eq.mpr, iSup, Set, And, MeasureTheory.NullMeasurableSet, ENorm.enorm, id, Eq, congrArg, MeasureTheory.lintegral_rearrangement_eq_and, MeasureTheory.AEStronglyMeasurable.add, Trans.trans, rfl, iSup_mono, MeasureTheory.lintegral_mono_fn', le_refl and 22 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_rearrangement_add_rearrangement_le_add_lintegral [SigmaFinite μ] {ε}
  [TopologicalSpace ε] [ESeminormedAddMonoid ε] [ContinuousAdd ε] {f g : α → ε}
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) {t : ℝ≥0∞} :
      ∫⁻ (s : ℝ≥0∞) in Set.Iio t, rearrangement (f + g) s μ
        ≤ (∫⁻ (s : ℝ≥0∞) in Set.Iio t, rearrangement f s μ)
          + ∫⁻ (s : ℝ≥0∞) in Set.Iio t, rearrangement g s μ := by
…
```
Mentions: g, s, MeasureTheory.rearrangement

Carleson/ToMathlib/Rearrangement.lean

Decreasing rearrangements f^#

`Carleson/ToMathlib/Rearrangement.lean`

Decreasing rearrangements `f^#`