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

41 declarations, 0 contain sorry, 0 declared as axioms

Minkowski's integral inequality

In this file, we prove Minkowski's integral inequality and apply it to truncations. We use this to deduce weak type estimates for truncations.

Upstreaming status:

Minkowski's integral inequality belongs into mathlib, and is mostly ready
applying it to truncations needs truncations upstreamed first
weak type estimates are also desirable

Lemma names often need to be improved a bit; perhaps the code can also be golfed.

Imports (1)

Carleson.ToMathlib.RealInterpolation.Misc

Imported by 2 files

def MeasureTheory.truncCut line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, MeasureTheory.SigmaFinite, Nat
Proof uses: Set.indicator, MeasureTheory.spanningSets, Min.min
6 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.truncCut_mono line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ENNReal, Monotone, Nat, MeasureTheory.truncCut
Proof uses: LE.le, id, dite, ite, Membership.mem, Set, MeasureTheory.spanningSets, Classical.decPred, Min.min, OfNat.ofNat, Classical.propDecidable, Eq.mpr, Eq, congrFun', congrArg, ite_eq_left, min_le_min_left, Iff.mpr, Nat.cast_le, Not and 7 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.truncCut_mono₀ line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ENNReal, Monotone, Nat, MeasureTheory.truncCut
Proof uses: LE.le, MeasureTheory.truncCut_mono
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.truncCut_sup line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ENNReal, Eq, iSup, Nat, MeasureTheory.truncCut
Proof uses: iSup_eq_of_forall_le_of_forall_lt_exists_gt, id, LE.le, Set.indicator, MeasureTheory.spanningSets, Min.min, dite, ite, Membership.mem, Set, Classical.decPred, OfNat.ofNat, Classical.propDecidable, Eq.mpr, congrFun', congrArg, ite_eq_left, min_le_left, Not, ite_eq_right and 25 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.representationLp Characterization of ∫⁻ x : α, f x ^ p ∂μ by a duality argument line 84 source
Source documentation
Characterization of ∫⁻ x : α, f x ^ p ∂μ by a duality argument.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SigmaFinite, ENNReal, AEMeasurable, Real, GT.gt, OfNat.ofNat, GE.ge, Eq, HAdd.hAdd, Inv.inv, HPow.hPow, MeasureTheory.lintegral, HDiv.hDiv, iSup, Membership.mem, Set, Set.ofPred, And and 2 more
Proof uses: Nat, MeasureTheory.spanningSets, MeasureTheory.truncCut, Real.HolderConjugate, Iff.mpr, LT.lt, Real.holderConjugate_iff, And.intro, HSub.hSub, Eq.mpr, ite, Classical.decPred, Min.min, id, congr, congrArg, congrFun', Set.indicator, MeasureTheory.truncCut.eq_1, dite and 161 more
217 instances, coercions and auxiliary constants left out.

Tactic trace: 155 steps
Open to load the checked before-and-after goal states.
```
lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) {p q : ℝ} (hp : p > 1) (hq : q ≥ 1)
    (hpq : p⁻¹ + q⁻¹ = 1) :
    (∫⁻ x : α, (f x) ^ p ∂μ) ^ (1 / p) =
    ⨆ g ∈ {g' : α → ℝ≥0∞ | AEMeasurable g' μ ∧ ∫⁻ x : α, (g' x) ^ q ∂μ ≤ 1},
    ∫⁻ x : α, (f x) * g x ∂μ := by
…
```
Mentions: g
lemma MeasureTheory.aemeasurability_prod₁ TODO: better name! line 233 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Prod, ENNReal, AEMeasurable, MeasureTheory.Measure.prod, Filter.Eventually, Function.comp, Prod.mk, MeasureTheory.ae
Proof uses: And, Measurable, Filter.EventuallyEq, Filter.mp_mem, Set.ofPred, Eq, MeasureTheory.Measure.ae_ae_of_ae_prod, And.right, Filter.univ_mem', Membership.mem, Set, id, Exists.intro, And.intro, Measurable.comp, And.left, measurable_prodMk_left
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma aemeasurability_prod₁ {α : Type u_1} {β : Type u_3}
    [MeasurableSpace α] [MeasurableSpace β]
    {μ : Measure α} {ν : Measure β} [SFinite ν]
    ⦃f : α × β → ENNReal⦄
    (hf : AEMeasurable f (μ.prod ν)) :
    ∀ᵐ x : α ∂μ, AEMeasurable (f ∘ (Prod.mk x)) ν := by
…
```
lemma MeasureTheory.aemeasurability_prod₂ TODO: better name! line 244 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Prod, ENNReal, AEMeasurable, MeasureTheory.Measure.prod, Filter.Eventually, Function.comp, Prod.mk, MeasureTheory.ae
Proof uses: Prod.swap, AEMeasurable.comp_measurable, Eq.mpr, MeasureTheory.Measure.map, id, Eq, congrArg, MeasureTheory.Measure.prod_swap, measurable_swap, eq_of_heq, Filter, HEq, Eq.refl, HEq.refl, Eq.symm, funext, autoParam, MeasureTheory.aemeasurability_prod₁
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma aemeasurability_prod₂ {α : Type u_1} {β : Type u_3}
    [MeasurableSpace α] [MeasurableSpace β]
    {μ : Measure α} {ν : Measure β} [SFinite ν]
    [SFinite μ] ⦃f : α × β → ENNReal⦄
    (hf : AEMeasurable f (μ.prod ν)) :
    ∀ᵐ y : β ∂ν, AEMeasurable (f ∘ (fun x ↦ Prod.mk x y)) μ := by
…
```
lemma MeasureTheory.aemeasurable_integral_component TODO: better name! line 258 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, Prod, ENNReal, AEMeasurable, MeasureTheory.Measure.prod, MeasureTheory.lintegral, Prod.mk
Proof uses: And, Measurable, Filter.EventuallyEq, MeasureTheory.ae, Exists.intro, And.intro, Measurable.lintegral_prod_right, And.left, Filter.mp_mem, Set.ofPred, Filter.Eventually, Eq, MeasureTheory.Measure.ae_ae_of_ae_prod, And.right, Filter.univ_mem', Membership.mem, Set, id, MeasureTheory.lintegral_congr_ae
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma aemeasurable_integral_component {α : Type u_1} {β : Type u_3}
    [MeasurableSpace α] [MeasurableSpace β]
    {μ : Measure α} {ν : Measure β} [SFinite ν]
    ⦃f : α × β → ENNReal⦄
    (hf : AEMeasurable f (μ.prod ν)) :
    AEMeasurable (fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ := by
…
```
lemma MeasureTheory.lintegral_lintegral_pow_swap Minkowsi's integral inequality: TODO describe what it does line 271 source
Source documentation
Minkowsi's integral inequality: TODO describe what it does

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, MeasureTheory.SigmaFinite, ENNReal, AEMeasurable, Prod, Function.uncurry, MeasureTheory.Measure.prod, HPow.hPow, MeasureTheory.lintegral, Inv.inv
Proof uses: LT.lt, Eq, Or, Decidable.lt_or_eq_of_le, Real.conjExponent, Real.HolderConjugate, Real.HolderConjugate.conjExponent, Real.HolderTriple.lt, Real.HolderConjugate.symm, Membership.mem, Set, Set.ofPred, And, HMul.hMul, Filter.Eventually, MeasureTheory.ae, MeasureTheory.aemeasurability_prod₁, Trans.trans, MeasureTheory.lintegral_congr_ae, Filter.mp_mem and 48 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_lintegral_pow_swap {α : Type u_1} {β : Type u_3} {p : ℝ} (hp : 1 ≤ p)
    [MeasurableSpace α] [MeasurableSpace β]
    {μ : Measure α} {ν : Measure β} [SFinite ν]
    [SigmaFinite μ] ⦃f : α → β → ENNReal⦄
    (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :
    (∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ) ^ p⁻¹ ≤
    ∫⁻ (y : β), (∫⁻ (x : α), (f x y) ^ p ∂μ) ^ p⁻¹ ∂ν := by
…
```
lemma MeasureTheory.lintegral_lintegral_pow_swap_rpow line 311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GE.ge, OfNat.ofNat, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, MeasureTheory.SigmaFinite, ENNReal, AEMeasurable, Prod, Function.uncurry, MeasureTheory.Measure.prod, LE.le, MeasureTheory.lintegral, HPow.hPow, Inv.inv
Proof uses: LT.lt, lt_of_lt_of_le, zero_lt_one, ENNReal.le_of_rpow_le, inv_pos_of_pos, Eq.mpr, id, Eq, congrArg, ENNReal.rpow_rpow_inv, LT.lt.ne', MeasureTheory.lintegral_lintegral_pow_swap
49 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.aemeasurable_ton line 327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ToneCouple, AEMeasurable, ENNReal, ToneCouple.ton, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat
Proof uses: ite, Eq, Bool, ToneCouple.mon, Bool.true, StrictMono, StrictAnti, ToneCouple.ton_is_ton, dite, aemeasurable_restrict_of_monotoneOn, measurableSet_Ioi, StrictMonoOn.monotoneOn, StrictMono.strictMonoOn, Eq.mp, ite_eq_left, Not, aemeasurable_restrict_of_antitoneOn, StrictAntiOn.antitoneOn, StrictAnti.strictAntiOn, ite_eq_right
27 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.indicator_ton_measurable TODO: better name! line 336 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ToneCouple, MeasureTheory.NullMeasurableSet, Prod, ENNReal, Set.ofPred, MeasureTheory.indicator_ton_measurable.match_1, LE.le, ENorm.enorm, ToneCouple.ton, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat
Proof uses: nullMeasurableSet_le, Prod.snd, Prod.fst, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.AEStronglyMeasurable.comp_snd, AEMeasurable.comp_fst, AEMeasurable.comp_aemeasurable, of_eq_true, AEMeasurable, MeasureTheory.Measure.map, Eq.trans, True, congrArg, MeasureTheory.Measure.map_id', aemeasurable_id'
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma indicator_ton_measurable {g : α → E₁}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    (hg : AEStronglyMeasurable g μ) (tc : ToneCouple) :
    NullMeasurableSet {(s, x) : ℝ≥0∞ × α | ‖g x‖ₑ ≤ tc.ton s } ((volume.restrict (Ioi 0)).prod μ) := by
…
```
Mentions: g, E₁, ToneCouple, s
lemma MeasureTheory.indicator_ton_measurable_lt TODO: better name! line 347 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ToneCouple, MeasureTheory.NullMeasurableSet, Prod, ENNReal, Set.ofPred, MeasureTheory.indicator_ton_measurable.match_1, LT.lt, ToneCouple.ton, ENorm.enorm, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat
Proof uses: nullMeasurableSet_lt, Prod.fst, Prod.snd, AEMeasurable.comp_fst, AEMeasurable.comp_aemeasurable, of_eq_true, AEMeasurable, MeasureTheory.Measure.map, Eq.trans, True, congrArg, MeasureTheory.Measure.map_id', aemeasurable_id', MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.AEStronglyMeasurable.comp_snd
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma indicator_ton_measurable_lt {g : α → E₁}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    (hg : AEStronglyMeasurable g μ) (tc : ToneCouple) :
    NullMeasurableSet {(s, x) : ℝ≥0∞ × α | tc.ton s < ‖g x‖ₑ }
      ((volume.restrict (Ioi 0)).prod μ) := by
…
```
Mentions: g, E₁, ToneCouple, s
lemma MeasureTheory.AEStronglyMeasurable.trunc_ton_norm line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ToneCouple, Prod, ENNReal, MeasureTheory.trunc, ToneCouple.ton, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, Function.support, ENorm.enorm
Proof uses: Set, Set.ofPred, MeasureTheory.indicator_ton_measurable.match_1, LE.le, Eq, Set.indicator, funext, of_eq_true, ite, Eq.trans, True, congrArg, ite_congr, Membership.mem, Classical.decPred, Eq.refl, Not, eq_self, Eq.mpr, id and 5 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.trunc_ton line 373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ToneCouple, Prod, ENNReal, MeasureTheory.trunc, ToneCouple.ton, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, Function.support
Proof uses: Set, Set.ofPred, MeasureTheory.indicator_ton_measurable.match_1, LE.le, ENorm.enorm, Eq, Set.indicator, funext, of_eq_true, ite, Eq.trans, True, congrArg, ite_congr, Membership.mem, Classical.decPred, Eq.refl, Not, eq_self, Eq.mpr and 6 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.truncCompl_ton line 387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ToneCouple, Prod, ENNReal, MeasureTheory.truncCompl, ToneCouple.ton, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, Function.support
Proof uses: Set, Set.ofPred, MeasureTheory.indicator_ton_measurable.match_1, LT.lt, ENorm.enorm, Eq, Set.indicator, funext, Eq.mpr, ite, id, congrArg, MeasureTheory.truncCompl_eq, of_eq_true, Eq.trans, True, ite_congr, Membership.mem, Classical.decPred, Eq.refl and 7 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.truncCompl_ton_norm line 401 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.AEStronglyMeasurable, ToneCouple, Prod, ENNReal, MeasureTheory.truncCompl, ToneCouple.ton, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, Function.support, ENorm.enorm
Proof uses: Set, Set.ofPred, MeasureTheory.indicator_ton_measurable.match_1, LT.lt, Eq, Set.indicator, funext, Eq.mpr, ite, id, congrArg, MeasureTheory.truncCompl_eq, of_eq_true, Eq.trans, True, ite_congr, Membership.mem, Classical.decPred, Eq.refl, Not and 6 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.restrict_to_support TODO: better name! line 415 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Real, LT.lt, OfNat.ofNat, TopologicalSpace, ESeminormedAddMonoid, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Function.support, HPow.hPow, ENorm.enorm, MeasureTheory.trunc
Proof uses: MeasureTheory.setLIntegral_eq_of_support_subset, id, LE.le, Set, Set.ofPred, Ne, Eq.mpr, ite, congrArg, propext, Set.ofPred_subset_ofPred, Mathlib.Tactic.Contrapose.contrapose₄, congrFun', ite_congr, Not, Eq.refl, of_eq_true, Eq.trans, True, ite_eq_left_of_eq_true and 3 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma restrict_to_support {p : ℝ} (hp : 0 < p) [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
  (f : α → E₁) :
    ∫⁻ x : α in f.support, ‖trunc f t x‖ₑ ^ p ∂ μ = ∫⁻ x : α, ‖trunc f t x‖ₑ ^ p ∂μ := by
…
```
Mentions: E₁, MeasureTheory.trunc
lemma MeasureTheory.restrict_to_support_truncCompl TODO: better name! line 427 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Real, TopologicalSpace, ESeminormedAddMonoid, LT.lt, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Function.support, HPow.hPow, ENorm.enorm, MeasureTheory.truncCompl
Proof uses: MeasureTheory.setLIntegral_eq_of_support_subset, id, LE.le, Set, Eq.mpr, Set.ofPred, Ne, ite, congrArg, MeasureTheory.truncCompl_eq, propext, Set.ofPred_subset_ofPred, Mathlib.Tactic.Contrapose.contrapose₄, of_eq_true, Eq.trans, True, congrFun', ite_eq_right_of_eq_false, False, enorm_zero and 2 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma restrict_to_support_truncCompl {p : ℝ} [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
  (hp : 0 < p) (f : α → E₁) :
    ∫⁻ x : α in f.support, ‖(truncCompl f t) x‖ₑ ^ p ∂μ =
    ∫⁻ x : α, ‖(truncCompl f t) x‖ₑ ^ p ∂μ := by
…
```
Mentions: E₁, MeasureTheory.truncCompl
lemma MeasureTheory.restrict_to_support_trnc TODO: better name! line 440 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Real, Bool, TopologicalSpace, ESeminormedAddMonoid, LT.lt, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Function.support, ENorm.enorm, HPow.hPow, MeasureTheory.trnc
Proof uses: MeasureTheory.setLIntegral_eq_of_support_subset, id, LE.le, Set, Eq.mpr, Set.ofPred, Ne, congrArg, propext, Set.ofPred_subset_ofPred, Mathlib.Tactic.Contrapose.contrapose₄, MeasureTheory.trnc_le_func, Iff.mpr, ENNReal.rpow_eq_zero_iff_of_pos, of_eq_true, Eq.trans, True, congrFun', Eq.mp, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma restrict_to_support_trnc {p : ℝ} {j : Bool} [TopologicalSpace E₁]
  [ESeminormedAddMonoid E₁] (hp : 0 < p) (f : α → E₁) :
    ∫⁻ x : α in (fun x ↦ ‖f x‖ₑ).support, ‖trnc j f t x‖ₑ ^ p ∂μ =
    ∫⁻ x : α, ‖trnc j f t x‖ₑ ^ p ∂μ := by
…
```
Mentions: E₁, MeasureTheory.trnc
theorem MeasureTheory.AEStronglyMeasurable.trnc_restrict line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Bool, MeasureTheory.AEStronglyMeasurable, ToneCouple, Prod, ENNReal, MeasureTheory.trnc, ToneCouple.ton, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, Function.support
Proof uses: dite, Eq, Bool.true, Eq.mpr, MeasureTheory.trunc, id, congrFun', congrArg, autoParam, funext, MeasureTheory.trnc.match_1, Unit, MeasureTheory.truncCompl, MeasureTheory.AEStronglyMeasurable.trunc_ton, Not, Bool.false, Bool.of_not_eq_true, MeasureTheory.AEStronglyMeasurable.truncCompl_ton
30 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.AEStronglyMeasurable.trnc_restrict_norm line 468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Bool, MeasureTheory.AEStronglyMeasurable, ToneCouple, Prod, ENNReal, MeasureTheory.trnc, ToneCouple.ton, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, Function.support, ENorm.enorm
Proof uses: dite, Eq, Bool.true, Eq.mpr, MeasureTheory.trunc, id, congrFun', congrArg, autoParam, funext, MeasureTheory.trnc.match_1, Unit, MeasureTheory.truncCompl, MeasureTheory.AEStronglyMeasurable.trunc_ton_norm, Not, Bool.false, Bool.of_not_eq_true, MeasureTheory.AEStronglyMeasurable.truncCompl_ton_norm
30 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_lintegral_pow_swap_truncCompl_old line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Real, TopologicalSpace, ESeminormedAddMonoid, Bool, MeasureTheory.SigmaFinite, MeasureTheory.Measure.restrict, Function.support, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.AEStronglyMeasurable, ToneCouple, ENNReal, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, Set.Ioi, HPow.hPow, HMul.hMul and 6 more
Proof uses: MeasureTheory.lintegral_lintegral_pow_swap_rpow, le_of_mul_le_mul_left, Eq.mpr, id, Eq, Mathlib.Tactic.FieldSimp.le_eq_cancel_le, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Eq.trans, congr_arg₂, rfl, Mathlib.Tactic.FieldSimp.NF.mul_eq_eval, Eq.refl, Mathlib.Tactic.FieldSimp.NF.atom_eq_eval, Mathlib.Tactic.FieldSimp.NF.one_eq_eval and 51 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_lintegral_pow_swap_truncCompl line 514 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Real, TopologicalSpace, ESeminormedAddMonoid, Bool, MeasureTheory.SigmaFinite, MeasureTheory.Measure.restrict, Function.support, ENNReal, ENorm.enorm, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.AEStronglyMeasurable, ToneCouple, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, Set.Ioi, HPow.hPow and 6 more
Proof uses: MeasureTheory.lintegral_lintegral_pow_swap_rpow, le_of_mul_le_mul_left, Eq.mpr, id, Eq, Mathlib.Tactic.FieldSimp.le_eq_cancel_le, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Eq.trans, congr_arg₂, rfl, Mathlib.Tactic.FieldSimp.NF.mul_eq_eval, Eq.refl, Mathlib.Tactic.FieldSimp.NF.atom_eq_eval, Mathlib.Tactic.FieldSimp.NF.one_eq_eval and 51 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_congr_support line 549 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Membership.mem, Set, Function.support, ENorm.enorm, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict
Proof uses: MeasureTheory.lintegral_congr_ae, Iff.mpr, Filter.Eventually, MeasureTheory.ae, Set.ofPred, Not, OfNat.ofNat, MeasureTheory.ae_iff, Eq.mpr, Inter.inter, id, congrArg, MeasureTheory.Measure.restrict_apply₀', MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_support, AEMeasurable, aestronglyMeasurable_iff_aemeasurable, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.measure_mono_null, EmptyCollection.emptyCollection, Set.mem_of_mem_inter_right and 3 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.estimate_trnc One of the key estimates for the real interpolation theorem, not yet using the particular choice of exponent and scale in the ScaledPowerFunction line 565 source
Source documentation
One of the key estimates for the real interpolation theorem, not yet using the particular choice of exponent and scale in the ScaledPowerFunction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Real, ScaledPowerFunction, Bool, TopologicalSpace, ESeminormedAddMonoid, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.AEStronglyMeasurable, MeasureTheory.SigmaFinite, MeasureTheory.Measure.restrict, Function.support, ENNReal, ENorm.enorm, ite, Eq, Bool.xor, ToneCouple.mon and 19 more
Proof uses: ScaledPowerFunction.hd, id, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', ENNReal.toReal, ToneCouple, Eq.mpr, congrArg, rfl, dite, congrFun', funext, ite_eq_left, Iff.mp, ENNReal.ofReal_eq_zero, Mathlib.Tactic.Contrapose.contrapose₁, Not, implies_congr, ite_eq_right and 195 more
209 instances, coercions and auxiliary constants left out.

Tactic trace: 102 steps
Open to load the checked before-and-after goal states.
```
lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₀q₀ : p₀ ≤ q₀)
    (hf : AEStronglyMeasurable f μ) (hf₂ : SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support))
    (hpowers : if xor j (spf_to_tc spf).mon = true then q₀ < q else q < q₀)
    (hpow_pos : 0 < q₀ + spf.σ⁻¹ * (q - q₀)) :
    ∫⁻ s : ℝ in Ioi 0,
    eLpNorm (trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s))) (ENNReal.ofReal p₀) μ ^ q₀ *
    ENNReal.ofReal (s ^ (q - q₀ - 1)) ≤
    (spf.d ^ (q - q₀)) * ENNReal.ofReal |q - q₀|⁻¹ *
    (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support,
    ‖f a‖ₑ ^ (p₀ + spf.σ⁻¹ * (q - q₀) * (p₀ / q₀)) ∂μ) ^ (p₀⁻¹ * q₀) := by
…
```
Mentions: ScaledPowerFunction, E₁, spf_to_tc, s, MeasureTheory.trnc
def MeasureTheory.sel TODO: add a doc-string, explaining the purpose of this definition line 692 source
Source comment
TODO: add a doc-string, explaining the purpose of this definition

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal
Proof uses: MeasureTheory.sel.match_1, Unit
```
def sel (j : Bool) (p₀ p₁ : ℝ≥0∞) := match j with | true => p₁ | false => p₀
```
lemma MeasureTheory.estimate_trnc₁ Documented declaration: estimate_trnc₁ line 697 source
Source documentation
One of the key estimates for the real interpolation theorem, now using the particular choice of exponent, but not yet using the particular choice of scale in the ScaledPowerFunction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ScaledPowerFunction, Bool, TopologicalSpace, ESeminormedAddMonoid, Membership.mem, Set, Set.Ioo, OfNat.ofNat, LT.lt, LE.le, MeasureTheory.sel, Ne, Top.top, Eq, Inv.inv, HAdd.hAdd, HMul.hMul and 22 more
Proof uses: ComputationsInterpolatedExponents.interp_exp_toReal_pos', Or.inl, LT.lt.ne_top, HDiv.hDiv, Bool.false, id, Eq.mpr, congrArg, ComputationsChoiceExponent.ζ_equality₅, LT.lt.ne, Bool.true, ComputationsChoiceExponent.ζ_equality₆, ENNReal.toReal_pos, LT.lt.ne', Trans.trans, Iff.mpr, ENNReal.ofReal_toReal_eq_iff, Eq.symm, MeasureTheory.estimate_trnc, Eq.refl and 56 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 109 steps
Open to load the checked before-and-after goal states.
```
lemma estimate_trnc₁ {spf : ScaledPowerFunction} {j : Bool}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] (ht : t ∈ Ioo 0 1)
    (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hpq : sel j p₀ p₁ ≤ sel j q₀ q₁)
    (hp' : sel j p₀ p₁ ≠ ⊤) (hq' : sel j q₀ q₁ ≠ ⊤) (hp₀p₁ : p₀ < p₁)
    (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - t) * p₀⁻¹ + t * p₁⁻¹)
    (hq : q⁻¹ = (1 - t) * q₀⁻¹ + t * q₁⁻¹)
    (hf : AEStronglyMeasurable f μ) (hf₂ : SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support))
    (hspf : spf.σ = ζ p₀ q₀ p₁ q₁ t.toReal) :
    ∫⁻ s : ℝ in Ioi 0,
    eLpNorm (trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s))) (sel j p₀ p₁) μ ^ (sel j q₀ q₁).toReal *
    ENNReal.ofReal (s ^ (q.toReal - (sel j q₀ q₁).toReal - 1)) ≤
    (spf.d ^ (q.toReal - (sel j q₀ q₁).toReal)) *
…
```
Mentions: ScaledPowerFunction, E₁, MeasureTheory.sel, s, MeasureTheory.trnc, spf_to_tc
lemma MeasureTheory.wnorm_eq_zero_iff line 813 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, ENNReal, Ne, OfNat.ofNat, Iff, Eq, MeasureTheory.wnorm, Filter.EventuallyEq, MeasureTheory.ae, ENorm.enorm
Proof uses: id, dite, ite, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.wnorm', ENNReal.toReal, Eq.mpr, congrFun', congrArg, ite_eq_left, MeasureTheory.eLpNorm, Eq.symm, MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNorm_enorm, MeasureTheory.eLpNormEssSup_eq_zero_iff, Not, ite_eq_right, Iff.trans, Iff.intro and 56 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.weaktype_estimate line 859 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, MeasureTheory.Measure, ENNReal, ENorm, NNReal, LT.lt, OfNat.ofNat, Top.top, MeasureTheory.MemLp, MeasureTheory.HasWeakType, LE.le, MeasureTheory.distribution, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, MeasureTheory.eLpNorm, Neg.neg
Proof uses: dite, Eq, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', MeasureTheory.distibution_top, Not, MeasureTheory.wnorm, And.right, MeasureTheory.AEStronglyMeasurable, ENNReal.toReal_pos, LT.lt.ne', LT.lt.ne_top, ENNReal.rpow_pos_of_nonneg, LT.lt.le, ENNReal.toNNReal, Inv.inv and 16 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.weaktype_estimate_top line 876 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, MeasureTheory.Measure, ENNReal, ENorm, NNReal, Eq, Top.top, MeasureTheory.MemLp, MeasureTheory.HasWeakType, LE.le, HMul.hMul, MeasureTheory.eLpNorm, MeasureTheory.distribution, OfNat.ofNat
Proof uses: MeasureTheory.wnorm, And.right, MeasureTheory.AEStronglyMeasurable, Iff.mp, nonpos_iff_eq_zero, Trans.trans, MeasureTheory.eLpNormEssSup, MeasureTheory.distribution_mono_right, le_trans, Eq.mp, ite, MeasureTheory.wnorm', ENNReal.toReal, congrFun', congrArg, ite_eq_left, meas_essSup_lt, ENorm.enorm, Filter.isBounded_le_of_top, Filter.map and 1 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_eq_zero_of_eLpNorm_eq_zero line 894 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Ne, OfNat.ofNat, Eq, MeasureTheory.eLpNorm
Proof uses: dite, of_eq_true, Eq.trans, True, congrFun', congrArg, autoParam, MeasureTheory.eLpNorm_exponent_zero, eq_self, Not, Eq.mpr, ENorm.enorm, id, Eq.symm, MeasureTheory.eLpNorm_enorm, Filter.EventuallyEq, MeasureTheory.ae, propext, MeasureTheory.eLpNorm_eq_zero_iff, Continuous.comp_aestronglyMeasurable and 2 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNormEssSup_eq_zero_of_eLpNorm_eq_zero line 901 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Ne, OfNat.ofNat, Eq, MeasureTheory.eLpNorm, MeasureTheory.eLpNormEssSup
Proof uses: Eq.mpr, Top.top, id, congrArg, Eq.symm, MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNorm_eq_zero_of_eLpNorm_eq_zero
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_eq_zero_of_eLpNormEssSup_eq_zero line 906 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Eq, MeasureTheory.eLpNormEssSup, OfNat.ofNat, MeasureTheory.eLpNorm
Proof uses: Eq.mpr, Top.top, id, congrArg, Eq.symm, MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNorm_eq_zero_of_eLpNorm_eq_zero, ENNReal.top_ne_zero
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_trnc_est line 915 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Bool, LE.le, MeasureTheory.eLpNorm, MeasureTheory.trnc
Proof uses: MeasureTheory.eLpNorm_mono_enorm, MeasureTheory.trnc_le_func
13 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.weaktype_aux₀ If T has weaktype p₀-p₁, f is AEStronglyMeasurable and the p-norm of f vanishes, then the q-norm of T f vanishes line 921 source
Source documentation
If T has weaktype p₀-p₁, f is AEStronglyMeasurable and the p-norm of f vanishes, then the q-norm of T f vanishes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, MeasureTheory.Measure, ESeminormedAddMonoid, ENorm, ENNReal, LT.lt, OfNat.ofNat, NNReal, MeasureTheory.HasWeakType, MeasureTheory.AEStronglyMeasurable, Eq, MeasureTheory.eLpNorm
Proof uses: MeasureTheory.eLpNorm_eq_zero_of_eLpNorm_eq_zero, LT.lt.ne', MeasureTheory.MemLp, And.intro, Top.top, Eq.mpr, id, congrArg, ENNReal.zero_lt_top, LE.le, MeasureTheory.wnorm, HMul.hMul, And.right, Iff.mp, nonpos_iff_eq_zero, Eq.mp, MulZeroClass.mul_zero, Filter.EventuallyEq, MeasureTheory.ae, ENorm.enorm and 4 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma weaktype_aux₀ {f : α → ε₁} {T : (α → ε₁) → (α' → ε₂)}
    {q₀ p : ℝ≥0∞} (p₀ q : ℝ≥0∞) (hq₀ : 0 < q₀) (hp : 0 < p)
    {C₀ : ℝ≥0} (h₀T : HasWeakType T p₀ q₀ μ ν C₀)
    (hf : AEStronglyMeasurable f μ) (hF : eLpNorm f p μ = 0) : eLpNorm (T f) q ν = 0 := by
…
```
Mentions: T, α', MeasureTheory.HasWeakType
lemma MeasureTheory.weaktype_estimate_truncCompl line 938 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ENorm, NNReal, LT.lt, OfNat.ofNat, Ne, Top.top, LE.le, MeasureTheory.MemLp, MeasureTheory.HasWeakType, MeasureTheory.distribution, MeasureTheory.truncCompl, HMul.hMul, HPow.hPow, Real, ENNReal.toReal and 2 more
Proof uses: MeasureTheory.weaktype_estimate, MeasureTheory.truncCompl_Lp_Lq_lower, And.intro
37 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.weaktype_estimate_trunc TODO: can we remove the hypothesis on a? line 948 source
Source comment
TODO: can we remove the hypothesis on a?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ENorm, NNReal, LT.lt, OfNat.ofNat, Top.top, LE.le, MeasureTheory.MemLp, MeasureTheory.HasWeakType, Ne, MeasureTheory.distribution, MeasureTheory.trunc, HMul.hMul, HPow.hPow, Real, ENNReal.toReal and 2 more
Proof uses: MeasureTheory.weaktype_estimate, MeasureTheory.trunc_Lp_Lq_higher, And.intro
37 instances, coercions and auxiliary constants left out.
```
lemma weaktype_estimate_trunc {C₁ : ℝ≥0} {p p₁ q₁ : ℝ≥0∞} {f : α → E₁'}
    (hp : 0 < p) (hq₁ : 0 < q₁) (hq₁' : q₁ < ⊤) (hp₁p : p ≤ p₁) (hf : MemLp f p μ)
    (h₁T : HasWeakType T' p₁ q₁ μ ν C₁) (ht : 0 < t) {a : ℝ≥0∞} (ha : a ≠ ⊤) :
    distribution (T' (trunc f a)) t ν ≤ C₁ ^ q₁.toReal *
      eLpNorm (trunc f a) p₁ μ ^ q₁.toReal * (t ^ (-q₁.toReal)) :=
…
```
Mentions: MeasureTheory.HasWeakType, MeasureTheory.distribution, MeasureTheory.trunc
lemma MeasureTheory.weaktype_estimate_trunc_top_top line 955 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ENorm, NNReal, LT.lt, OfNat.ofNat, Eq, Top.top, LE.le, MeasureTheory.MemLp, MeasureTheory.HasWeakType, HDiv.hDiv, MeasureTheory.distribution, MeasureTheory.trunc
Proof uses: dite, of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.distibution_top, eq_self, Not, Eq.mpr, id, MeasureTheory.trunc_Lp_Lq_higher, And.intro, ENNReal.div_ne_top, ne_of_gt, Iff.mpr, ENNReal.coe_pos, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm and 28 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.weaktype_estimate_truncCompl_top line 980 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ENorm, NNReal, LT.lt, OfNat.ofNat, Eq, Top.top, Ne, MeasureTheory.MemLp, MeasureTheory.HasWeakType, HPow.hPow, Real, HDiv.hDiv, ENNReal.toReal, HSub.hSub, HMul.hMul and 4 more
Proof uses: dite, of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.distibution_top, eq_self, Not, MeasureTheory.eLpNormEssSup, Or, eq_zero_or_pos, MeasureTheory.trnc, Bot.bot, Bool, Iff.mp, LE.le, nonpos_iff_eq_zero, Eq.mpr, id and 87 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.weaktype_estimate_trunc_top NB line 1042 source
Source comment
NB. The assumptions `hd` is necessary: if `t ≠ ∞` and `f` has eLpNorm 0, then `d = 0` as well (since p.toReal and p₁.toReal are positive), hence `a = ∞` and the statement becomes `distribution (T f) t ν = 0`, which is false in general.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ENorm, NNReal, LT.lt, OfNat.ofNat, Top.top, Eq, MeasureTheory.MemLp, MeasureTheory.HasWeakType, HPow.hPow, Real, HDiv.hDiv, ENNReal.toReal, HSub.hSub, HMul.hMul, MeasureTheory.eLpNorm and 3 more
Proof uses: MeasureTheory.AEStronglyMeasurable, And.left, dite, of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.distibution_top, eq_self, Not, Ne, MeasureTheory.MemLp.eLpNorm_lt_top, Eq.rec, ENNReal.rpow_ne_top_of_ne_zero, Eq.symm, Iff.mpr, And, ENNReal.div_ne_zero, And.intro and 80 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma weaktype_estimate_trunc_top {C₁ : ℝ≥0} (hC₁ : 0 < C₁) {p p₁ q₁ : ℝ≥0∞}
    (hp : 0 < p)
    (hp₁ : p₁ < ⊤) (hq₁ : q₁ = ⊤) (hp₁p : p < p₁) {f : α → E₁'} (hf : MemLp f p μ)
    (h₁T : HasWeakType T' p₁ q₁ μ ν C₁) (ht : 0 < t) {a : ℝ≥0∞} {d : ℝ≥0∞} (hd : 0 < d)
    (ha : a = (t / d) ^ (p₁.toReal / (p₁.toReal - p.toReal)))
    (hdeq : d = ((ENNReal.ofNNReal C₁) ^ p₁.toReal * eLpNorm f p μ ^ p.toReal) ^ p₁.toReal⁻¹) :
    distribution (T' (trunc f a)) t ν = 0 := by
…
```
Mentions: MeasureTheory.HasWeakType, d, MeasureTheory.distribution, MeasureTheory.trunc