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

62 declarations, 0 contain sorry, 0 declared as axioms

The Marcinkiewisz real interpolation theorem

This file contains a proof of the Marcinkiewisz real interpolation theorem. The proof roughly follows Folland, Real Analysis. Modern Techniques and Their Applications, section 6.4, theorem 6.28, but a different truncation is used, and some estimates instead follow the technique as e.g. described in [Duoandikoetxea, Fourier Analysis, 2000].

This file has the definitions for the main proof, and the final proof of the theorem. A few other files contain the necessary pre-requisites:

(in InterpolateExponents.lean) Convenience results for working with (interpolated) exponents
(in InterpolateExponents.lean) Results about the particular choice of exponent
(in Misc.lean) Interface for using cutoff functions
(in Misc.lean) Results about the particular choice of scale
(in Misc.lean) Some tools for measure theory computations
(in Misc.lean) Results about truncations of a function
(in Misc.lean) Measurability properties of truncations
(in Misc.lean) Truncations and Lp spaces
(in Misc.lean) Some results about the integrals of truncations
(in Minkowski.lean) Minkowski's integral inequality
(in Minkowski.lean) Apply Minkowski's integral inequality to truncations
(in Minkowski.lean) Weaktype estimates applied to truncations

Upstreaming status: the result is highly desirable; the ideal proof strategy is not yet clear. It may be nicer to generalise this to Lorentz spaces first, and then upstream the proof there. (Useful ingredients for this proof also belong into mathlib.) Prioritise other files first (e.g., about weak type or the prerequisites files).

Imports (1)

Carleson.ToMathlib.RealInterpolation.Minkowski

Imported by 3 files

def MeasureTheory.SubadditiveOn The operator is subadditive on functions satisfying P with constant A line 59 source
Source documentation
The operator is subadditive on functions satisfying P with constant A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENorm, ENNReal
Proof uses: LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul
12 instances, coercions and auxiliary constants left out.
```
def SubadditiveOn [ENorm ε] (T : (α → ε₁) → α' → ε) (P : (α → ε₁) → Prop) (A : ℝ≥0∞) : Prop :=
…
```
Mentions: T, α', A
def MeasureTheory.SubadditiveTrunc line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENorm, ENNReal, MeasureTheory.Measure
Proof uses: LT.lt, OfNat.ofNat, Filter.Eventually, LE.le, ENorm.enorm, HAdd.hAdd, MeasureTheory.trunc, MeasureTheory.truncCompl, HMul.hMul, MeasureTheory.ae
24 instances, coercions and auxiliary constants left out.
def MeasureTheory.AESubadditiveOn The operator is subadditive on functions satisfying P with constant A (this is almost vacuous if A = ⊤) line 69 source
Source documentation
The operator is subadditive on functions satisfying P with constant A (this is almost vacuous if A = ⊤).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENorm, ENNReal, MeasureTheory.Measure
Proof uses: Filter.Eventually, LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul, MeasureTheory.ae
14 instances, coercions and auxiliary constants left out.
```
def AESubadditiveOn [ENorm ε] (T : (α → ε₁) → α' → ε) (P : (α → ε₁) → Prop) (A : ℝ≥0∞)
    (ν : Measure α') : Prop :=
…
```
Mentions: T, α', A
lemma MeasureTheory.SubadditiveOn.aeSubadditiveOn line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, ENorm, MeasureTheory.SubadditiveOn, MeasureTheory.Measure, MeasureTheory.AESubadditiveOn
Proof uses: MeasureTheory.ae_of_all, LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul
14 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.SubadditiveOn.iSup line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.SubadditiveOn, iSup
Proof uses: id, LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul, iSup_le, LE.le.trans, mul_le_mul', le_refl, add_le_add, le_iSup
44 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.SubadditiveOn.iSup₂ line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.SubadditiveOn, iSup
Proof uses: Eq.mpr, PSigma, PSigma.fst, PSigma.snd, id, Eq, congrFun', congrArg, funext, iSup_psigma', MeasureTheory.SubadditiveOn.iSup
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.SubadditiveOn.indicator line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.SubadditiveOn, Set, Set.indicator
Proof uses: LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul, dite, Membership.mem, Classical.propDecidable, of_eq_true, Eq.trans, True, congr, congrArg, Set.indicator_of_mem, eq_true, Not, OfNat.ofNat, Set.indicator_of_notMem, False, eq_false, not_false_eq_true and 3 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.SubadditiveOn.const If T is constant in the second argument (but not necessarily the first) and satisfies a subadditivity criterion, then SubadditiveOn T P 1 line 107 source
Source comment
If `T` is constant in the second argument (but not necessarily the first) and satisfies a subadditivity criterion, then `SubadditiveOn T P 1`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, LE.le, HAdd.hAdd, MeasureTheory.SubadditiveOn, OfNat.ofNat
Proof uses: Eq.mpr, ENorm.enorm, HMul.hMul, id, Eq, congrArg, one_mul
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma const {T : (α → ε₁) → ℝ≥0∞} (h_add : ∀ {f g}, P f → P g → T (f + g) ≤ T f + T g) :
    SubadditiveOn (fun u (_ : α') ↦ T u) P 1 :=
…
```
Mentions: T, g, MeasureTheory.SubadditiveOn, α'
lemma MeasureTheory.SubadditiveOn.imp line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.SubadditiveOn
2 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.AESubadditiveOn.antitone line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.Measure, ENNReal, MeasureTheory.AESubadditiveOn
4 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.AESubadditiveOn.zero line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.Measure, HAdd.hAdd, ENNReal, Filter.EventuallyEq, MeasureTheory.ae, OfNat.ofNat, MeasureTheory.AESubadditiveOn
Proof uses: Filter.mp_mem, Set.ofPred, Eq, LE.le, ENorm.enorm, HMul.hMul, Membership.mem, Set, Filter.univ_mem', id, of_eq_true, Eq.trans, True, congr, congrArg, enorm_zero, add_zero, MulZeroClass.mul_zero
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AESubadditiveOn.forall_le line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.Measure, Set, Set.Countable, ENNReal, Membership.mem, MeasureTheory.AESubadditiveOn, Filter.Eventually, LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul, MeasureTheory.ae
Proof uses: Iff.mpr, eventually_countable_ball
35 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.AESubadditiveOn.biSup line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.Measure, Set, Set.Countable, ENNReal, Filter.Eventually, Ne, iSup, Membership.mem, Top.top, MeasureTheory.ae, HAdd.hAdd, MeasureTheory.AESubadditiveOn
Proof uses: Filter.mp_mem, Set.ofPred, Filter.univ_mem', id, Eq.mpr, Not, Eq, congrArg, ne_eq, LE.le, propext, eq_top_iff, Eq.mp, LE.le.trans, le_biSup, ENorm.enorm, HMul.hMul, Iff.mpr, MeasureTheory.ae_ball_iff, forall_congr and 8 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AESubadditiveOn.indicator line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.Measure, ENNReal, MeasureTheory.AESubadditiveOn, Set, Set.indicator
Proof uses: Filter.mp_mem, MeasureTheory.ae, Set.ofPred, LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul, Filter.univ_mem', Membership.mem, id, dite, Classical.propDecidable, of_eq_true, Eq.trans, True, congr, congrArg, Set.indicator_of_mem, eq_true, Not and 8 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AESubadditiveOn.const If T is constant in the second argument (but not necessarily the first) and satisfies a subadditivity criterion, then AESubadditiveOn T P 1 line 184 source
Source comment
If `T` is constant in the second argument (but not necessarily the first) and satisfies a subadditivity criterion, then `AESubadditiveOn T P 1`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.Measure, LE.le, ENNReal, ENorm.enorm, HAdd.hAdd, MeasureTheory.AESubadditiveOn, OfNat.ofNat
Proof uses: MeasureTheory.ae_of_all, HMul.hMul, Eq.mpr, id, Eq, congrArg, one_mul
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma const (T : (α → ε₁) → ε) (P : (α → ε₁) → Prop)
    (h_add : ∀ {f g}, P f → P g → ‖T (f + g)‖ₑ ≤ ‖T f‖ₑ + ‖T g‖ₑ) :
    AESubadditiveOn (fun u (_ : α') ↦ T u) P 1 ν :=
…
```
Mentions: T, g, MeasureTheory.AESubadditiveOn, α'
def MeasureTheory.SublinearOn The operator is sublinear on functions satisfying P with constant A line 196 source
Source documentation
The operator is sublinear on functions satisfying P with constant A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENNReal
Proof uses: And, MeasureTheory.SubadditiveOn, Eq, HSMul.hSMul
4 instances, coercions and auxiliary constants left out.
```
def SublinearOn (T : (α → ε₁) → α' → ε) (P : (α → ε₁) → Prop) (A : ℝ≥0∞) :
    Prop :=
…
```
Mentions: T, α', A
def MeasureTheory.AESublinearOn The operator is almost everywhere sublinear on functions satisfying P with constant A line 201 source
Source documentation
The operator is almost everywhere sublinear on functions satisfying P with constant A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENNReal, MeasureTheory.Measure
Proof uses: And, MeasureTheory.AESubadditiveOn, Filter.EventuallyEq, MeasureTheory.ae, HSMul.hSMul
6 instances, coercions and auxiliary constants left out.
```
def AESublinearOn (T : (α → ε₁) → α' → ε) (P : (α → ε₁) → Prop) (A : ℝ≥0∞) (ν : Measure α') :
    Prop :=
…
```
Mentions: T, α', A
lemma MeasureTheory.SublinearOn.aeSublinearOn line 209 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENNReal, MeasureTheory.SublinearOn, MeasureTheory.Measure, MeasureTheory.AESublinearOn
Proof uses: And.intro, MeasureTheory.AESubadditiveOn, Filter.EventuallyEq, MeasureTheory.ae, HSMul.hSMul, MeasureTheory.SubadditiveOn.aeSubadditiveOn, And.left, MeasureTheory.SubadditiveOn, Eq, MeasureTheory.ae_of_all, congrFun, And.right
24 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.SublinearOn.iSup line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENNReal, MeasureTheory.SublinearOn, iSup
Proof uses: And.intro, MeasureTheory.SubadditiveOn, Eq, HSMul.hSMul, MeasureTheory.SubadditiveOn.iSup, And.left, funext, Eq.mpr, id, congrArg, ENNReal.smul_iSup, eq_of_heq, SupSet, HEq, Eq.refl, HEq.refl, Eq.symm, Eq.rec, rfl, And.right
42 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.SublinearOn.iSup₂ line 224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENNReal, MeasureTheory.SublinearOn, iSup
Proof uses: Eq.mpr, PSigma, PSigma.fst, PSigma.snd, id, Eq, congrFun', congrArg, funext, iSup_psigma', MeasureTheory.SublinearOn.iSup
37 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.SublinearOn.indicator line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ESeminormedAddCommMonoid, Module, ENNReal, Set, MeasureTheory.SublinearOn, Set.indicator
Proof uses: And.intro, MeasureTheory.SubadditiveOn, Eq, HSMul.hSMul, MeasureTheory.SubadditiveOn.indicator, And.left, funext, dite, Membership.mem, Classical.propDecidable, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', congrFun, And.right, Set.indicator_of_mem, eq_self and 7 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.SublinearOn.const If T is constant in the second argument (but not necessarily the first) and satisfies certain requirements, then SublinearOn T P 1 line 241 source
Source comment
If `T` is constant in the second argument (but not necessarily the first) and satisfies certain requirements, then `SublinearOn T P 1`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, LE.le, ENNReal, ENorm.enorm, HAdd.hAdd, Eq, HSMul.hSMul, MeasureTheory.SublinearOn, OfNat.ofNat
Proof uses: And.intro, MeasureTheory.SubadditiveOn, MeasureTheory.SubadditiveOn.const, ENorm, funext, of_eq_true, Eq.trans, True, congrFun', congrArg, eq_self
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma const (T : (α → ε₁) → ε) (P : (α → ε₁) → Prop)
    (h_add : ∀ {f g}, P f → P g → ‖T (f + g)‖ₑ ≤ ‖T f‖ₑ + ‖T g‖ₑ)
    (h_smul : ∀ f {c : ℝ≥0}, P f → T (c • f) = c • T f) :
    SublinearOn (fun u (_ : α') ↦ T u) P 1 := by
…
```
Mentions: T, g, c, MeasureTheory.SublinearOn, α'
lemma MeasureTheory.SublinearOn.imp line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENNReal, MeasureTheory.SublinearOn
Proof uses: And.intro, MeasureTheory.SubadditiveOn, Eq, HSMul.hSMul, MeasureTheory.SubadditiveOn.imp, And.left, And.right
22 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.AESublinearOn.antitone line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, MeasureTheory.Measure, ENNReal, MeasureTheory.AESublinearOn
Proof uses: And.intro, MeasureTheory.AESubadditiveOn, Filter.EventuallyEq, MeasureTheory.ae, HSMul.hSMul, MeasureTheory.AESubadditiveOn.antitone, And.left, And.right
6 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.AESublinearOn.biSup line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, MeasureTheory.Measure, Set, Set.Countable, ENNReal, Filter.Eventually, Ne, iSup, Membership.mem, Top.top, MeasureTheory.ae, HAdd.hAdd, HSMul.hSMul, MeasureTheory.AESublinearOn
Proof uses: Filter.mp_mem, Set.ofPred, Filter.univ_mem', id, Eq.mpr, Not, Eq, congrArg, ne_eq, LE.le, propext, eq_top_iff, Eq.mp, LE.le.trans, le_biSup, And.intro, MeasureTheory.AESubadditiveOn, Filter.EventuallyEq, MeasureTheory.AESubadditiveOn.biSup, And.left and 10 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AESublinearOn.biSup2 line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddCommMonoid, Module, NNReal, Set, Set.Countable, ENNReal, Filter.Eventually, Ne, iSup, Membership.mem, Top.top, MeasureTheory.ae, OfNat.ofNat, HAdd.hAdd, HSMul.hSMul, MeasureTheory.AESublinearOn, Set.add and 2 more
Proof uses: Exists.intro, And, Exists, Eq, And.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, add_zero, eq_self, zero_add, MeasureTheory.AESublinearOn.antitone, Or.elim, MeasureTheory.AESublinearOn.biSup, Filter.mp_mem, LE.le, ENorm.enorm, HMul.hMul and 65 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AESublinearOn.indicator line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, MeasureTheory.Measure, ESeminormedAddCommMonoid, Module, ENNReal, Set, MeasureTheory.AESublinearOn, Set.indicator
Proof uses: And.intro, MeasureTheory.AESubadditiveOn, Filter.EventuallyEq, MeasureTheory.ae, HSMul.hSMul, MeasureTheory.AESubadditiveOn.indicator, And.left, Filter.mp_mem, Set.ofPred, Eq, And.right, Filter.univ_mem', Membership.mem, id, dite, Classical.propDecidable, of_eq_true, Eq.trans, True, congr and 10 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AESublinearOn.const If T is constant in the second argument (but not necessarily the first) and satisfies certain requirements, then AESublinearOn T P 1 line 335 source
Source comment
If `T` is constant in the second argument (but not necessarily the first) and satisfies certain requirements, then `AESublinearOn T P 1`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, MeasureTheory.Measure, LE.le, ENNReal, ENorm.enorm, HAdd.hAdd, Eq, HSMul.hSMul, MeasureTheory.AESublinearOn, OfNat.ofNat
Proof uses: And.intro, MeasureTheory.AESubadditiveOn, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.AESubadditiveOn.const, MeasureTheory.ae_of_all, id
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma const (T : (α → ε₁) → ε) (P : (α → ε₁) → Prop)
    (h_add : ∀ {f g}, P f → P g → ‖T (f + g)‖ₑ ≤ ‖T f‖ₑ + ‖T g‖ₑ)
    (h_smul : ∀ f {c : ℝ≥0}, P f → T (c • f) = c • T f) :
    AESublinearOn (fun u (_ : α') ↦ T u) P 1 ν := by
…
```
Mentions: T, g, c, MeasureTheory.AESublinearOn, α'
lemma MeasureTheory.AESublinearOn.toReal line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, MeasureTheory.Measure, ENNReal, MeasureTheory.AESublinearOn, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Real, ENNReal.toReal
Proof uses: And.intro, MeasureTheory.AESubadditiveOn, Filter.EventuallyEq, HSMul.hSMul, Filter.mp_mem, Set.ofPred, LE.le, ENorm.enorm, HAdd.hAdd, HMul.hMul, Membership.mem, Set, And.left, Filter.univ_mem', id, Eq.mpr, Eq, congrArg, congr, Real.enorm_toReal and 13 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.PreservesAEStrongMeasurability Proposition that expresses that the map T map between function spaces preserves AE strong measurability on L^p line 383 source
Source documentation
Proposition that expresses that the map T map between function spaces preserves AE strong measurability on L^p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal
Proof uses: MeasureTheory.MemLp, MeasureTheory.AEStronglyMeasurable
2 instances, coercions and auxiliary constants left out.
```
def PreservesAEStrongMeasurability (T : (α → ε₁) → α' → ε₂) (p : ℝ≥0∞) : Prop :=
…
```
Mentions: T, α'
lemma MeasureTheory.estimate_distribution_subadditiveTrunc line 386 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ENorm, LT.lt, OfNat.ofNat, MeasureTheory.SubadditiveTrunc, LE.le, MeasureTheory.distribution, HMul.hMul, Nat, HAdd.hAdd, MeasureTheory.trunc, MeasureTheory.truncCompl
Proof uses: Eq.mpr, id, Eq, congrArg, mul_comm, mul_assoc, two_mul, MeasureTheory.distribution_add_le_of_enorm, Filter.Eventually, ENorm.enorm, MeasureTheory.ae, Eq.symm, MeasureTheory.trunc_add_truncCompl
70 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.rewrite_norm_func line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Real, TopologicalSpace, ContinuousENorm, LT.lt, OfNat.ofNat, NNReal, MeasureTheory.AEStronglyMeasurable, Eq, ENNReal, MeasureTheory.lintegral, HPow.hPow, ENorm.enorm, HMul.hMul, ENNReal.ofReal, Nat, MeasureTheory.MeasureSpace.volume, MeasureTheory.distribution, HSub.hSub
Proof uses: Trans.trans, MeasureTheory.Measure.restrict, Set.Ioi, Eq.mpr, id, congrArg, MeasureTheory.lintegral_norm_pow_eq_distribution, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 76 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.estimate_norm_rpow_range_operator line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Real, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, LT.lt, OfNat.ofNat, StrictRangeToneCouple, NNReal, MeasureTheory.SubadditiveTrunc, MeasureTheory.AEStronglyMeasurable, LE.le, ENNReal, MeasureTheory.lintegral, HPow.hPow, ENorm.enorm, HMul.hMul, ENNReal.ofReal, Nat and 8 more
Proof uses: Eq.mpr, id, Eq, congrArg, MeasureTheory.rewrite_norm_func, mul_le_mul', le_refl, MeasureTheory.lintegral_mono_ae, Filter.mp_mem, MeasureTheory.ae, Set.ofPred, Membership.mem, Set, Set.Ioo, Top.top, ae_in_Ioo_zero_top, Filter.univ_mem', ENNReal.ofReal_mul, of_eq_true, Eq.symm and 18 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.ton_measurable_eLpNorm_trunc TODO: the infrastructure can perhaps be improved here line 443 source
Source comment
TODO: the infrastructure can perhaps be improved here

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ToneCouple, Measurable, MeasureTheory.eLpNorm, MeasureTheory.trunc, ToneCouple.ton
Proof uses: id, ite, Eq, Bool, ToneCouple.mon, Bool.true, StrictMono, StrictAnti, ToneCouple.ton_is_ton, dite, Function.comp, Monotone.measurable, Monotone.comp, MeasureTheory.eLpNorm_trunc_mono, StrictMono.monotone, Eq.mp, ite_eq_left, Not, Antitone.measurable, Monotone.comp_antitone and 2 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem ton_measurable_eLpNorm_trunc [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] (tc : ToneCouple) :
    Measurable (fun x ↦ eLpNorm (trunc f (tc.ton x)) p₁ μ) := by
…
```
Mentions: E₁, ToneCouple, MeasureTheory.trunc
lemma MeasureTheory.estimate_norm_rpow_range_operator' line 451 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, LT.lt, OfNat.ofNat, StrictRangeToneCouple, Eq, Top.top, GT.gt, MeasureTheory.distribution, MeasureTheory.truncCompl, ToneCouple.ton, StrictRangeToneCouple.toToneCouple, MeasureTheory.trunc, MeasureTheory.MemLp, MeasureTheory.HasWeakType and 11 more
Proof uses: Neg.neg, of_eq_true, Eq.trans, inferInstance, Ring, True, congr, congrArg, Int.rawCast, Int.negOfNat, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm, Eq.refl and 88 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor_rw_aux₀ line 513 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, HMul.hMul
Proof uses: Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_mul and 4 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor_rw_aux₁ line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Eq, HMul.hMul
Proof uses: of_eq_true, Eq.trans, True, congrArg, HAdd.hAdd, HPow.hPow, Nat, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right and 14 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor₀ line 518 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, MeasureTheory.eLpNorm and 5 more
Proof uses: And.left, LE.le, lt_of_lt_of_le, And.right, ne_top_of_le_ne_top, ComputationsInterpolatedExponents.interp_exp_in_Ioo_zero_top, Or.inl, ENNReal.toReal_pos_of_Ioo, Eq.mpr, id, congrArg, div_eq_mul_inv, ENNReal.mul_inv, Or.inr, ChoiceScale.d_ne_top_aux₂, ChoiceScale.d_ne_zero_aux₀, ENNReal.mul_rpow_of_ne_zero, ChoiceScale.d_ne_zero_aux₂, mul_ne_zero, Iff.mpr and 105 more
144 instances, coercions and auxiliary constants left out.

Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor₁ line 573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, MeasureTheory.eLpNorm and 5 more
Proof uses: And.left, LE.le, lt_of_lt_of_le, And.right, ne_top_of_le_ne_top, ComputationsInterpolatedExponents.interp_exp_in_Ioo_zero_top, Decidable.not_or_of_imp, ENNReal.toReal_pos_of_Ioo, Eq.mpr, id, congrArg, div_eq_mul_inv, ENNReal.mul_inv, Or.inr, ChoiceScale.d_ne_top_aux₂, ChoiceScale.d_ne_zero_aux₀, ENNReal.mul_rpow_of_ne_zero, ChoiceScale.d_ne_zero_aux₂, mul_ne_zero, Iff.mpr and 71 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.finite_spanning_sets_from_lintegrable line 629 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, AEMeasurable, LT.lt, MeasureTheory.lintegral, Top.top, MeasureTheory.Measure.FiniteSpanningSetsIn, MeasureTheory.Measure.restrict, Function.support, Set.univ, Set
Proof uses: MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Nat, ite, Eq, OfNat.ofNat, Set.ofPred, LE.le, HDiv.hDiv, HAdd.hAdd, trivial
29 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.support_sigma_finite_of_lintegrable line 674 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, AEMeasurable, LT.lt, MeasureTheory.lintegral, Top.top, MeasureTheory.SigmaFinite, MeasureTheory.Measure.restrict, Function.support
Proof uses: MeasureTheory.SigmaFinite.mk, Exists.nonempty, MeasureTheory.Measure.FiniteSpanningSetsIn, Set.univ, Set, HEq, MeasureTheory.finite_spanning_sets_from_lintegrable, Exists.intro, HEq.rfl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.support_sigma_finite_from_MemLp line 681 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.MemLp, Ne, Top.top, OfNat.ofNat, MeasureTheory.SigmaFinite, MeasureTheory.Measure.restrict, Function.support, ENorm.enorm
Proof uses: HPow.hPow, Real, ENNReal.toReal, Eq, Set, id, Set.ofPred, Set.ext, Eq.mpr, Iff, Membership.mem, LE.le, Not, congrFun', congrArg, funext, Eq.trans, And, LT.lt, Or and 29 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.combine_estimates₀ line 713 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, LT.lt, OfNat.ofNat, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, ScaledPowerFunction, Membership.mem, Set, Set.Ioc, Set.Ioo, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub and 22 more
Proof uses: ComputationsInterpolatedExponents.interpolated_pos', ENNReal.ne_top_of_Ioo, MeasureTheory.SigmaFinite, MeasureTheory.Measure.restrict, Function.support, MeasureTheory.support_sigma_finite_from_MemLp, ComputationsInterpolatedExponents.interp_exp_ne_top, LT.lt.ne', StrictRangeToneCouple, spf_to_tc, Trans.trans, HDiv.hDiv, ScaledPowerFunction.d, MeasureTheory.sel, Bool, Bot.bot, MeasureTheory.MeasureSpace.volume, MeasureTheory.trunc, ToneCouple.ton, StrictRangeToneCouple.toToneCouple and 102 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 151 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.combine_estimates₁ line 860 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, LT.lt, OfNat.ofNat, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, ScaledPowerFunction, Membership.mem, Set, Set.Ioc, Set.Ioo, Ne, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub and 20 more
Proof uses: LT.lt.ne', ComputationsInterpolatedExponents.interpolated_pos', ENNReal.ne_top_of_Ioo, ComputationsInterpolatedExponents.interp_exp_ne_top, ENNReal.toReal_pos, ENNReal.le_of_rpow_le, Trans.trans, MeasureTheory.lintegral, ENorm.enorm, id, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', dite, HDiv.hDiv, Eq.mpr, congrFun', congrArg, Eq.trans, ite_congr, Eq.refl and 25 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor₃ line 902 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, LT.lt, OfNat.ofNat, Ne, Top.top, Membership.mem, Set, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, HPow.hPow, Real and 3 more
Proof uses: Eq.mpr, id, congrArg, Eq.symm, ComputationsInterpolatedExponents.interp_exp_eq, ENNReal.mul_rpow_of_nonneg, ENNReal.toReal_nonneg, ENNReal.rpow_mul, mul_div_assoc, mul_div_cancel_left₀, LT.lt.ne', ENNReal.toReal_pos, Eq.refl
69 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor_aux₄ line 911 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, MeasureTheory.eLpNorm, HPow.hPow and 2 more
Proof uses: ComputationsInterpolatedExponents.interp_exp_eq, ne_top_of_le_ne_top, And.right, LT.lt, LE.le, ENNReal.toReal_pos, LT.lt.ne', And.left, Eq.mpr, id, congrArg, Eq.symm, Mathlib.Tactic.Ring.of_eq, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul and 87 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor₄ line 939 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, MeasureTheory.eLpNorm and 4 more
Proof uses: And.left, LE.le, ne_top_of_le_ne_top, And.right, Eq.mpr, HDiv.hDiv, id, congrArg, Eq.symm, MeasureTheory.simplify_factor₃, MeasureTheory.simplify_factor₀, Eq.refl
61 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.simplify_factor₅ line 955 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HMul.hMul, HSub.hSub, LT.lt, MeasureTheory.eLpNorm and 4 more
Proof uses: ne_top_of_le_ne_top, And.right, LE.le, Eq.mpr, HDiv.hDiv, id, congrArg, Eq.symm, MeasureTheory.simplify_factor₃, And.left, ENNReal.mem_sub_Ioo, ENNReal.one_ne_top, ComputationsInterpolatedExponents.switch_exponents, MeasureTheory.simplify_factor₁, Eq.refl
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.exists_hasStrongType_real_interpolation_aux₀ The trivial case for the estimate in the real interpolation theorem when the L^p norm of f vanishes line 972 source
Source documentation
The trivial case for the estimate in the real interpolation theorem when the L^p norm of f vanishes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Set.Ioo, NNReal, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.HasWeakType, MeasureTheory.PreservesAEStrongMeasurability, MeasureTheory.MemLp and 1 more
Proof uses: LT.lt, ComputationsInterpolatedExponents.interpolated_pos', And.left, LE.le, ENNReal.ne_top_of_Ioo, ENNReal.pos_of_rb_Ioc, MeasureTheory.eLpNorm_eq_zero_of_eLpNorm_eq_zero, MeasureTheory.AEStronglyMeasurable, Top.top, LT.lt.ne', And.intro, Eq.mpr, id, congrArg, ENNReal.zero_lt_top, MeasureTheory.wnorm, HMul.hMul, And.right, Iff.mp, nonpos_iff_eq_zero and 13 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma exists_hasStrongType_real_interpolation_aux₀ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] [TopologicalSpace E₂] [ContinuousENorm E₂]
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (ht : t ∈ Ioo 0 1)
    {C₀ : ℝ≥0}
    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
    (h₀T : HasWeakType T p₀ q₀ μ ν C₀)
    (h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p) (hf : MemLp f p μ)
…
```
Mentions: E₁, E₂, MeasureTheory.HasWeakType, T, MeasureTheory.PreservesAEStrongMeasurability
lemma MeasureTheory.exists_hasStrongType_real_interpolation_aux The estimate for the real interpolation theorem in case p₀ < p₁ line 996 source
Source documentation
The estimate for the real interpolation theorem in case p₀ < p₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, NNReal, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioc, Ne, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.SubadditiveTrunc and 14 more
Proof uses: ENNReal.pos_of_rb_Ioc, Or, eq_zero_or_pos, le_of_eq_of_le, MeasureTheory.exists_hasStrongType_real_interpolation_aux₀, zero_le, ScaledPowerFunction, ChoiceScale.spf_ch, ENNReal.toReal_mem_Ioo, And.left, LT.lt.ne, And.intro, And.right, MeasureTheory.AEStronglyMeasurable, MeasureTheory.combine_estimates₁, id, lt_of_lt_of_le, Eq.refl
94 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma exists_hasStrongType_real_interpolation_aux {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} {A : ℝ≥0}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    [TopologicalSpace E₂] [ContinuousENorm E₂] (hA : 0 < A)
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁)
    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
    (hT : SubadditiveTrunc T A f ν) (h₀T : HasWeakType T p₀ q₀ μ ν C₀)
    (h₁T : HasWeakType T p₁ q₁ μ ν C₁)
    (h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p) (hf : MemLp f p μ) :
…
```
Mentions: A, E₁, E₂, MeasureTheory.SubadditiveTrunc, T, MeasureTheory.HasWeakType, MeasureTheory.PreservesAEStrongMeasurability
lemma MeasureTheory.exists_hasStrongType_real_interpolation_aux₁ TODO: the below lemmas were split because otherwise the lean server would crash (seems to be related to the linter?) (after the merge) line 1023 source
Source comment
TODO: the below lemmas were split because otherwise the lean server would crash (seems to be related to the linter?) (after the merge)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Eq, LT.lt, NNReal, Set.Ioo, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, Top.top, MeasureTheory.eLpNorm, HPow.hPow and 11 more
Proof uses: Ne, LT.lt.ne, ENNReal.pos_of_rb_Ioc, ComputationsChoiceExponent.preservation_inequality_of_lt₀, LT.lt.ne', ComputationsInterpolatedExponents.interp_exp_toReal_pos', Or.inl, LT.lt.ne_top, ChoiceScale.d_pos, ChoiceScale.d_ne_top, ENNReal.toReal_pos, Eq.mpr, id, congrArg, ENNReal.ofReal_toReal, Eq.refl, Iff.mpr, ENNReal.ofReal_toReal_eq_iff, ComputationsInterpolatedExponents.interp_exp_ne_top, HPow and 95 more
175 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma exists_hasStrongType_real_interpolation_aux₁ {f : α → E₁}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ < q₁)
    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤) :
    (ENNReal.ofReal q.toReal *
        ((C₀ * eLpNorm f p μ)^ q₀.toReal *
        (∫⁻ (t : ℝ) in Ioo 0 (@d _ E₁ _ p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f).toReal,
        ENNReal.ofReal (t ^ (q.toReal - q₀.toReal - 1))) * (if q₀ = ⊤ then 0 else 1) +
        ((C₁ * eLpNorm f p μ) ^ q₁.toReal *
…
```
Mentions: E₁, d
lemma MeasureTheory.exists_hasStrongType_real_interpolation_aux₂ The main estimate in the real interpolation theorem for p₀ = p₁, before taking roots, for the case q₀ < q₁ line 1102 source
Source documentation
The main estimate in the real interpolation theorem for p₀ = p₁, before taking roots, for the case q₀ < q₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Eq, LT.lt, NNReal, Set.Ioo, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.HasWeakType, MeasureTheory.PreservesAEStrongMeasurability and 11 more
Proof uses: ChoiceScale.d, ENNReal.pos_of_rb_Ioc, Ne, ne_top_of_le_ne_top, LT.lt.ne_top, And.right, LT.lt.ne', ComputationsInterpolatedExponents.interp_exp_toReal_pos', Or.inl, Eq.symm, ComputationsInterpolatedExponents.interp_exp_eq, Or, eq_zero_or_pos, le_of_eq_of_le, MeasureTheory.exists_hasStrongType_real_interpolation_aux₀, zero_le, And.intro, MeasureTheory.AEStronglyMeasurable, ENNReal.toReal_pos, ChoiceScale.d_pos and 120 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 137 steps
Open to load the checked before-and-after goal states.
```
lemma exists_hasStrongType_real_interpolation_aux₂ {f : α → E₁}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    [TopologicalSpace E₂] [ContinuousENorm E₂]
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ < q₁)
    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
    (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁)
    (h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p)
…
```
Mentions: E₁, E₂, MeasureTheory.HasWeakType, T, MeasureTheory.PreservesAEStrongMeasurability
lemma MeasureTheory.exists_hasStrongType_real_interpolation_aux₃ The main estimate for the real interpolation theorem for p₀ = p₁, requiring q₀ ≠ q₁, before taking roots line 1231 source
Source documentation
The main estimate for the real interpolation theorem for p₀ = p₁, requiring q₀ ≠ q₁, before taking roots.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Eq, Ne, NNReal, Set.Ioo, LT.lt, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.HasWeakType and 12 more
Proof uses: Or, lt_or_gt_of_ne, MeasureTheory.exists_hasStrongType_real_interpolation_aux₂, Mathlib.Tactic.Ring.of_eq, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_left, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_mul and 9 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma exists_hasStrongType_real_interpolation_aux₃ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    [TopologicalSpace E₂] [ContinuousENorm E₂]
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ ≠ q₁)
    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
    (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁)
    (h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p)
…
```
Mentions: E₁, E₂, MeasureTheory.HasWeakType, T, MeasureTheory.PreservesAEStrongMeasurability
lemma MeasureTheory.exists_hasStrongType_real_interpolation_aux₄ The main estimate for the real interpolation theorem, before taking roots, combining the cases p₀ ≠ p₁ and p₀ = p₁ line 1257 source
Source documentation
The main estimate for the real interpolation theorem, before taking roots, combining the cases p₀ ≠ p₁ and p₀ = p₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, NNReal, LT.lt, OfNat.ofNat, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, Membership.mem, Set, Set.Ioc, Ne, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.SubadditiveTrunc and 14 more
Proof uses: rfl, Eq.mpr, id, congrArg, Eq.symm, dite, Eq.mp, ite_eq_left, one_mul, ComputationsInterpolatedExponents.interp_exp_eq, Trans.trans, MeasureTheory.exists_hasStrongType_real_interpolation_aux₃, HMul, Eq.rec, Eq.refl, ENNReal.toReal_inv, add_comm, HPow, HAdd, mul_comm and 31 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma exists_hasStrongType_real_interpolation_aux₄ {p₀ p₁ q₀ q₁ p q : ℝ≥0∞} {A : ℝ≥0} (hA : 0 < A)
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    [TopologicalSpace E₂] [ContinuousENorm E₂]
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁)
    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁)
    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
    (hT : SubadditiveTrunc T A f ν) (h₀T : HasWeakType T p₀ q₀ μ ν C₀)
    (h₁T : HasWeakType T p₁ q₁ μ ν C₁)
    (h₂T : PreservesAEStrongMeasurability (μ := μ) (ν := ν) T p) (hf : MemLp f p μ) :
…
```
Mentions: A, E₁, E₂, MeasureTheory.SubadditiveTrunc, T, MeasureTheory.HasWeakType, MeasureTheory.PreservesAEStrongMeasurability
def MeasureTheory.C_realInterpolation_ENNReal The definition of the constant in the real interpolation theorem, when viewed as an element of ℝ≥0∞ line 1309 source
Source documentation
The definition of the constant in the real interpolation theorem, when viewed as an element of ℝ≥0∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, NNReal
Proof uses: HMul.hMul, ite, Eq, OfNat.ofNat, ENNReal.ofReal, Real, HPow.hPow, ENNReal.toReal, Inv.inv, HAdd.hAdd, LT.lt, Top.top, abs, HSub.hSub
33 instances, coercions and auxiliary constants left out.
```
def C_realInterpolation_ENNReal (p₀ p₁ q₀ q₁ q : ℝ≥0∞) (C₀ C₁ : ℝ≥0) (A : ℝ≥0) (t : ℝ≥0∞) :=
…
```
Mentions: A
lemma MeasureTheory.C_realInterpolation_ENNReal_ne_top line 1315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, NNReal, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Ne, Set.Ioo, LT.lt, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.C_realInterpolation_ENNReal, Top.top
Proof uses: ENNReal.pos_of_rb_Ioc, id, ENNReal.mul_ne_top, HMul.hMul, ite, ENNReal.ofReal, Real, HPow.hPow, ENNReal.toReal, abs, LT.lt.ne', ComputationsInterpolatedExponents.interpolated_pos', ENNReal.ne_top_of_Ioo, ComputationsInterpolatedExponents.interp_exp_ne_top, ite_ne_top, ENNReal.one_ne_top, Not, ENNReal.ofReal_ne_top, ENNReal.rpow_ne_top_of_nonneg', lt_of_le_of_ne' and 40 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.C_realInterpolation_ENNReal_pos line 1342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, NNReal, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioc, Ne, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.C_realInterpolation_ENNReal
Proof uses: ENNReal.pos_of_rb_Ioc, id, ENNReal.mul_pos, HMul.hMul, ite, ENNReal.ofReal, Real, HPow.hPow, ENNReal.toReal, Top.top, abs, mul_ne_zero, dite, Eq.mpr, congrFun', congrArg, ite_eq_left, ne_of_gt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat and 48 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.C_realInterpolation The constant occurring in the real interpolation theorem line 1374 source
Source documentation
The constant occurring in the real interpolation theorem

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, NNReal
Proof uses: ENNReal.toNNReal, MeasureTheory.C_realInterpolation_ENNReal
```
def C_realInterpolation (p₀ p₁ q₀ q₁ q : ℝ≥0∞) (C₀ C₁ A : ℝ≥0) (t : ℝ≥0∞) : ℝ≥0 :=
…
```
Mentions: A
lemma MeasureTheory.C_realInterpolation_pos line 1377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, NNReal, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioc, Ne, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.C_realInterpolation
Proof uses: id, ENNReal.toNNReal_pos, MeasureTheory.C_realInterpolation_ENNReal, ne_of_gt, MeasureTheory.C_realInterpolation_ENNReal_pos, MeasureTheory.C_realInterpolation_ENNReal_ne_top
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.coe_C_realInterpolation line 1388 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, NNReal, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Ne, Set.Ioo, LT.lt, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.C_realInterpolation, MeasureTheory.C_realInterpolation_ENNReal
Proof uses: ENNReal.coe_toNNReal, MeasureTheory.C_realInterpolation_ENNReal_ne_top
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.Subadditive_trunc_from_SubadditiveOn_Lp₀p₁ line 1397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, LT.lt, OfNat.ofNat, NNReal, LE.le, Membership.mem, Set, Set.Ioo, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub, MeasureTheory.AESubadditiveOn, Or and 2 more
Proof uses: dite, Filter.Eventually, ENorm.enorm, MeasureTheory.trunc, MeasureTheory.truncCompl, HMul.hMul, MeasureTheory.ae, Top.top, Eq.mpr, id, congrArg, congrFun', Filter, funext, congr, MeasureTheory.trunc_top, MeasureTheory.truncCompl_top, Filter.univ_mem', Set.ofPred, Eq.symm and 37 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.exists_hasStrongType_real_interpolation Marcinkiewicz real interpolation theorem line 1439 source
Source documentation
Marcinkiewicz real interpolation theorem

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Ne, NNReal, LE.le, Set.Ioo, LT.lt, Eq, Inv.inv, HAdd.hAdd, HDiv.hDiv, HSub.hSub and 7 more
Proof uses: And.intro, MeasureTheory.eLpNorm, HMul.hMul, Eq.mpr, id, congrArg, HAdd, Eq.rec, Eq.refl, HDiv, MeasureTheory.SubadditiveTrunc, MeasureTheory.Subadditive_trunc_from_SubadditiveOn_Lp₀p₁, And.left, MeasureTheory.C_realInterpolation_ENNReal, MeasureTheory.coe_C_realInterpolation, lt_of_lt_of_le, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Nat.cast_one and 3 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem exists_hasStrongType_real_interpolation {p₀ p₁ q₀ q₁ p q : ℝ≥0∞}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]
    [TopologicalSpace E₂] [ContinuousENorm E₂]
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁)
    {C₀ C₁ A : ℝ≥0} (hA : 1 ≤ A) (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hp : p⁻¹ = (1 - t) / p₀ + t / p₁) (hq : q⁻¹ = (1 - t) / q₀ + t / q₁)
    (hmT : ∀ f, MemLp f p μ → AEStronglyMeasurable (T f) ν)
    (hT : AESubadditiveOn T (fun f ↦ MemLp f p₀ μ ∨ MemLp f p₁ μ) A ν)
    (h₀T : HasWeakType T p₀ q₀ μ ν C₀) (h₁T : HasWeakType T p₁ q₁ μ ν C₁) :
    HasStrongType T p q μ ν (C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t) := by
…
```
Mentions: E₁, E₂, A, T, MeasureTheory.AESubadditiveOn, MeasureTheory.HasWeakType, MeasureTheory.HasStrongType, MeasureTheory.C_realInterpolation