Basic.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

26 declarations, 0 contain sorry, 0 declared as axioms

Imports (5)

Imported by 2 files

lemma MeasureTheory.eLorentzNorm'_mono_enorm_ae line 25 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Filter.Eventually, LE.le, ENorm.enorm, MeasureTheory.ae, MeasureTheory.eLorentzNorm'
Proof uses: id, mul_le_mul', HPow.hPow, Real, ENNReal.toReal, Inv.inv, MeasureTheory.eLpNorm, NNReal, HMul.hMul, MeasureTheory.distribution, MeasureTheory.Measure.withDensity, MeasureTheory.MeasureSpace.volume, le_refl, MeasureTheory.eLpNorm_mono_enorm, Eq.mpr, Eq, congr, congrArg, ENNReal.toReal_inv, ENNReal.rpow_le_rpow and 3 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_mono_enorm_ae line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Filter.Eventually, LE.le, ENorm.enorm, MeasureTheory.ae, MeasureTheory.eLorentzNorm
Proof uses: id, dite, ite, Eq, OfNat.ofNat, Top.top, MeasureTheory.eLpNormEssSup, HMul.hMul, MeasureTheory.eLorentzNorm', Eq.mpr, congr, congrArg, ite_eq_left, le_refl, Not, ite_eq_right, essSup_mono_ae, Filter.isCobounded_le_of_bot, Filter.map, Filter.isBounded_le_of_top and 2 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.eLorentzNorm_congr_enorm_ae Proof analogous to eLpNorm_congr_enorm_ae line 46 source
Source comment
Proof analogous to eLpNorm_congr_enorm_ae

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Filter.Eventually, Eq, ENorm.enorm, MeasureTheory.ae, MeasureTheory.eLorentzNorm
Proof uses: le_antisymm, MeasureTheory.eLorentzNorm_mono_enorm_ae, Filter.EventuallyEq.le, Filter.EventuallyEq.symm
6 instances, coercions and auxiliary constants left out.
```
theorem eLorentzNorm_congr_enorm_ae {f : α → ε'} {g : α → ε} (hfg : ∀ᵐ x ∂μ, ‖f x‖ₑ = ‖g x‖ₑ) :
    eLorentzNorm f p q μ = eLorentzNorm g p q μ :=
…
```
Mentions: g, MeasureTheory.eLorentzNorm
theorem MeasureTheory.eLorentzNorm_congr_ae Proof analogous to eLpNorm_congr_ae line 52 source
Source comment
Proof analogous to eLpNorm_congr_ae

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Filter.EventuallyEq, MeasureTheory.ae, Eq, MeasureTheory.eLorentzNorm
Proof uses: MeasureTheory.eLorentzNorm_congr_enorm_ae, Filter.Eventually.mono, ENorm.enorm, Eq.rec, rfl
4 instances, coercions and auxiliary constants left out.
```
theorem eLorentzNorm_congr_ae {f g : α → ε'} (hfg : f =ᵐ[μ] g) :
    eLorentzNorm f p q μ = eLorentzNorm g p q μ :=
…
```
Mentions: g, MeasureTheory.eLorentzNorm
theorem MeasureTheory.eLorentzNorm_enorm line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Eq, MeasureTheory.eLorentzNorm, ENorm.enorm
Proof uses: MeasureTheory.eLorentzNorm_congr_enorm_ae, Filter.Eventually.of_forall, MeasureTheory.ae, enorm_enorm
4 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.eLorentzNorm'_eq_zero_of_ae_enorm_zero line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Filter.EventuallyEq, MeasureTheory.ae, Function.comp, ENorm.enorm, OfNat.ofNat, Ne, Top.top, Eq, MeasureTheory.eLorentzNorm'
Proof uses: id, Eq.mpr, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, Inv.inv, MeasureTheory.eLpNorm, NNReal, MeasureTheory.distribution, MeasureTheory.Measure.withDensity, MeasureTheory.MeasureSpace.volume, congrFun', congrArg, autoParam, funext, Eq.trans, MeasureTheory.distribution_eq_zero_of_ae_zero_enorm, ENNReal.zero_rpow_of_pos, LT.lt and 9 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_eq_zero_of_ae_enorm_zero line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Filter.EventuallyEq, MeasureTheory.ae, Function.comp, ENorm.enorm, OfNat.ofNat, Eq, MeasureTheory.eLorentzNorm
Proof uses: Eq.mpr, Not, ite, Top.top, MeasureTheory.eLpNormEssSup, HMul.hMul, MeasureTheory.eLorentzNorm', id, MeasureTheory.eLpNorm, congrArg, Eq.symm, MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNorm_zero_of_ae_zero', Eq.trans, congrFun', ite_congr, Eq.refl, MulZeroClass.mul_zero, ite_self, MeasureTheory.eLorentzNorm'_eq_zero_of_ae_enorm_zero
25 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm'_eq_zero_of_ae_zero line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, OfNat.ofNat, Top.top, Filter.EventuallyEq, MeasureTheory.ae, Eq, MeasureTheory.eLorentzNorm'
Proof uses: MeasureTheory.eLorentzNorm'_eq_zero_of_ae_enorm_zero, Filter.mp_mem, Set.ofPred, Function.comp, ENorm.enorm, Filter.univ_mem', Membership.mem, Set, id, of_eq_true, Eq.trans, True, forall_congr, implies_congr_ctx, Eq.refl, congrFun', congrArg, enorm_zero, eq_self, implies_true
25 instances, coercions and auxiliary constants left out.

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

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_zero line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Eq, MeasureTheory.eLorentzNorm, OfNat.ofNat
Proof uses: MeasureTheory.eLorentzNorm_eq_zero_of_ae_enorm_zero, of_eq_true, Filter.EventuallyEq, MeasureTheory.ae, Function.comp, ENorm.enorm, Eq.trans, True, congrFun', congrArg, Function.const, enorm_zero
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_zero' line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Eq, MeasureTheory.eLorentzNorm, OfNat.ofNat
Proof uses: MeasureTheory.eLorentzNorm_zero
8 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.ae_eq_zero_of_eLorentzNorm'_eq_zero line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, Ne, OfNat.ofNat, Top.top, Eq, MeasureTheory.eLorentzNorm', Filter.EventuallyEq, MeasureTheory.ae
Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, Or, HPow.hPow, Real, ENNReal.toReal, Inv.inv, NNReal, MeasureTheory.Measure.withDensity, MeasureTheory.MeasureSpace.volume, HMul.hMul, MeasureTheory.distribution, Eq.mpr, Not, And, id, implies_congr, Eq.refl, And.intro, of_eq_true, Eq.trans and 79 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.eLorentzNorm'_eq_zero_iff line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, Ne, OfNat.ofNat, Top.top, Iff, Eq, MeasureTheory.eLorentzNorm', Filter.EventuallyEq, MeasureTheory.ae
Proof uses: Iff.intro, MeasureTheory.ae_eq_zero_of_eLorentzNorm'_eq_zero, MeasureTheory.eLorentzNorm'_eq_zero_of_ae_zero
26 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.eLorentzNorm_eq_zero_iff line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, Ne, OfNat.ofNat, Iff, Eq, MeasureTheory.eLorentzNorm, Filter.EventuallyEq, MeasureTheory.ae
Proof uses: id, dite, ite, Top.top, MeasureTheory.eLpNormEssSup, HMul.hMul, MeasureTheory.eLorentzNorm', Eq.mpr, congrFun', congrArg, Eq.trans, ite_congr, Eq.refl, Not, ite_eq_right, ite_eq_left, False.elim, MeasureTheory.eLpNormEssSup_eq_zero_iff, of_eq_true, True and 6 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_eq_eLpNorm line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Eq, MeasureTheory.eLorentzNorm, MeasureTheory.eLpNorm
Proof uses: dite, OfNat.ofNat, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', MeasureTheory.eLorentzNorm_exponent_zero', autoParam, MeasureTheory.eLpNorm_exponent_zero, eq_self, Not, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLorentzNorm_exponent_top_top, MeasureTheory.eLpNorm_exponent_top, ENNReal.ofReal, ENNReal.toReal, ENNReal.ofReal_toReal and 80 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm'_eq_wnorm line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, ENorm, Ne, Top.top, MeasureTheory.Measure, Eq, MeasureTheory.eLorentzNorm', MeasureTheory.wnorm
Proof uses: Eq.mpr, MeasureTheory.wnorm', ENNReal.toReal, id, congrArg, MeasureTheory.wnorm_ne_top, HMul.hMul, HPow.hPow, Real, Inv.inv, MeasureTheory.eLpNorm, NNReal, MeasureTheory.distribution, MeasureTheory.Measure.withDensity, MeasureTheory.MeasureSpace.volume, iSup, MeasureTheory.eLpNormEssSup, congrFun', Eq.trans, OfNat.ofNat and 38 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_eq_wnorm line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, ENorm, Ne, OfNat.ofNat, MeasureTheory.Measure, Eq, MeasureTheory.eLorentzNorm, Top.top, MeasureTheory.wnorm
Proof uses: dite, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, MeasureTheory.eLpNormEssSup, True, congr, MeasureTheory.eLorentzNorm_exponent_top_top, MeasureTheory.wnorm_top, eq_self, Not, MeasureTheory.eLorentzNorm', MeasureTheory.eLorentzNorm_eq_eLorentzNorm', MeasureTheory.eLorentzNorm'_eq_wnorm, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm'_eq Theorem 6.6 in https://doi.org/10.1007/978-3-319-30034-4 line 229 source
Source comment
Theorem 6.6 in https://doi.org/10.1007/978-3-319-30034-4

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, ENorm, Ne, OfNat.ofNat, Top.top, MeasureTheory.Measure, Eq, MeasureTheory.eLorentzNorm', MeasureTheory.eLpNorm, NNReal, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, Inv.inv, MeasureTheory.rearrangement, MeasureTheory.Measure.withDensity, MeasureTheory.MeasureSpace.volume
Proof uses: dite, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congr, MeasureTheory.eLorentzNorm'_exponent_zero', congrFun', autoParam, funext, ENNReal.toReal_inv, MeasureTheory.eLpNorm_exponent_zero, eq_self, Not, MeasureTheory.wnorm, MeasureTheory.eLorentzNorm'_eq_wnorm, iSup, MeasureTheory.wnorm_eq_iSup_rpow_mul_rearrangement and 180 more
242 instances, coercions and auxiliary constants left out.

Tactic trace: 115 steps
Open to load the checked before-and-after goal states.
```
lemma eLorentzNorm'_eq (p_nonzero : p ≠ 0) (p_ne_top : p ≠ ⊤) {f : α → ε} {μ : Measure α} :
  eLorentzNorm' f p q μ
    = eLpNorm (fun (t : ℝ≥0) ↦ t ^ p⁻¹.toReal * rearrangement f t μ) q
        (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹)) := by
…
```
Mentions: MeasureTheory.eLorentzNorm', MeasureTheory.rearrangement
lemma MeasureTheory.eLorentzNorm'_eq' line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, ENorm, Ne, OfNat.ofNat, Top.top, MeasureTheory.Measure, Eq, MeasureTheory.eLorentzNorm', MeasureTheory.eLpNorm, NNReal, HMul.hMul, HPow.hPow, Real, HSub.hSub, ENNReal.toReal, Inv.inv, MeasureTheory.rearrangement, MeasureTheory.MeasureSpace.volume
Proof uses: dite, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congr, MeasureTheory.eLorentzNorm'_exponent_zero', congrFun', autoParam, funext, ENNReal.toReal_inv, ENNReal.inv_zero, sub_zero, MeasureTheory.eLpNorm_exponent_zero, eq_self, Not, MeasureTheory.Measure.withDensity, MeasureTheory.eLorentzNorm'_eq and 59 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_eq TODO: remove this? line 387 source
Source comment
TODO: remove this?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Ne, OfNat.ofNat, Top.top, Eq, MeasureTheory.eLorentzNorm, MeasureTheory.eLpNorm, NNReal, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, Inv.inv, MeasureTheory.rearrangement, MeasureTheory.Measure.withDensity, MeasureTheory.MeasureSpace.volume
Proof uses: id, dite, ite, MeasureTheory.eLpNormEssSup, MeasureTheory.eLorentzNorm', Eq.mpr, congrFun', congrArg, Eq.trans, ite_congr, Eq.refl, Not, ite_eq_right, ite_eq_left, False.elim, MeasureTheory.eLorentzNorm'_eq
32 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma eLorentzNorm_eq (p_nonzero : p ≠ 0) (p_ne_top : p ≠ ⊤) {f : α → ε} :
  eLorentzNorm f p q μ
    = eLpNorm (fun (t : ℝ≥0) ↦ t ^ p⁻¹.toReal * rearrangement f t μ) q
        (volume.withDensity (fun (t : ℝ≥0) ↦ t⁻¹)) := by
…
```
Mentions: MeasureTheory.eLorentzNorm, MeasureTheory.rearrangement
lemma MeasureTheory.MemLorentz_iff_MemLp line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, Iff, MeasureTheory.MemLorentz, MeasureTheory.MemLp
Proof uses: id, And, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLorentzNorm, Top.top, Iff.intro, MeasureTheory.eLpNorm, Eq.mpr, Eq, congrArg, Eq.symm, MeasureTheory.eLorentzNorm_eq_eLpNorm, And.left
6 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.MemLorentz_of_MemLorentz_ge TODO: could maybe be strengthened to ↔ line 406 source
Source comment
TODO: could maybe be strengthened to ↔

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, TopologicalSpace, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.MemLorentz
Proof uses: id, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLorentzNorm, Top.top, And, And.intro, dite, ite, Eq, MeasureTheory.eLpNormEssSup, HMul.hMul, MeasureTheory.eLorentzNorm', Eq.mpr, congrFun', congrArg, ite_eq_left, ENNReal.zero_lt_top, Not, ite_eq_right, False.elim and 187 more
204 instances, coercions and auxiliary constants left out.

Tactic trace: 153 steps
Open to load the checked before-and-after goal states.
```
lemma MemLorentz_of_MemLorentz_ge [TopologicalSpace ε]
    {r₁ r₂ : ℝ≥0∞} (r₁_pos : 0 < r₁) (r₁_le_r₂ : r₁ ≤ r₂) {f : α → ε} (hf : MemLorentz f p r₁ μ) :
    MemLorentz f p r₂ μ := by
…
```
Mentions: MeasureTheory.MemLorentz
lemma MeasureTheory.eLorentzNorm'_indicator_const line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, ENorm.enorm, Top.top, Set, OfNat.ofNat, Eq, MeasureTheory.eLorentzNorm', Set.indicator, Function.const, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, Inv.inv
Proof uses: Eq.mpr, MeasureTheory.lintegral, NNReal, MeasureTheory.MeasureSpace.volume, MeasureTheory.distribution, id, congrArg, MeasureTheory.eLorentzNorm'_eq_integral_distribution_rpow, HMul, Eq.rec, Eq.refl, Set.Iio, congrFun', funext, MeasureTheory.distribution_indicator_const, ite, Membership.mem, Classical.decPred, congr, Eq.trans and 21 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm'_indicator_const' line 562 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Set, Ne, OfNat.ofNat, Top.top, Eq, MeasureTheory.eLorentzNorm', Set.indicator, Function.const, HMul.hMul, HPow.hPow, Real, HDiv.hDiv, Inv.inv, ENNReal.toReal, ENorm.enorm
Proof uses: Eq.mpr, MeasureTheory.eLpNorm, NNReal, MeasureTheory.rearrangement, MeasureTheory.Measure.withDensity, MeasureTheory.MeasureSpace.volume, id, congrArg, MeasureTheory.eLorentzNorm'_eq, Set.Iio, congrFun', autoParam, funext, MeasureTheory.rearrangement_indicator_const, MeasureTheory.lintegral, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, congr, ENNReal.toReal_inv, one_div, Set.preimage and 145 more
205 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLorentzNorm_indicator_const line 634 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Set, Eq, MeasureTheory.eLorentzNorm, Set.indicator, Function.const, ite, OfNat.ofNat, Top.top, ENorm.enorm, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, HDiv.hDiv
Proof uses: id, dite, MeasureTheory.eLpNormEssSup, MeasureTheory.eLorentzNorm', Eq.mpr, congr, congrArg, ite_eq_left, Eq.refl, Not, ite_eq_right, ite_congr, MeasureTheory.eLpNormEssSup_indicator_const_eq', MeasureTheory.eLpNormEssSup_indicator_const_eq, CommMonoidWithZero.mul_zero, HMul, Eq.rec, of_eq_true, Eq.trans, True and 9 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.MemLorentz.memLp line 660 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.MemLorentz, Membership.mem, Set, Set.Ioc, OfNat.ofNat, MeasureTheory.MemLp
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, propext, MeasureTheory.MemLorentz_iff_MemLp, MeasureTheory.MemLorentz_of_MemLorentz_ge, And.left, LT.lt, LE.le, And.right
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.