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

67 declarations, 0 contain sorry, 0 declared as axioms

Lemmas about `HasWeakType`

Imports (6)

Imported by 3 files

def MeasureTheory.wnorm' The weak L^p norm of a function, for p < ∞ line 37 source
Source documentation
The weak L^p norm of a function, for p < ∞

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, Real, MeasureTheory.Measure, ENNReal
Proof uses: iSup, NNReal, HMul.hMul, HPow.hPow, MeasureTheory.distribution, Inv.inv
16 instances, coercions and auxiliary constants left out.
```
def wnorm' (f : α → ε) (p : ℝ) (μ : Measure α) : ℝ≥0∞ :=
…
```
lemma MeasureTheory.wnorm'_zero line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Eq, ENNReal, MeasureTheory.wnorm', OfNat.ofNat, Real, Top.top
Proof uses: Eq.mpr, LT.lt, Exists, NNReal, id, Eq.trans, iSup, congrFun', congrArg, HMul.hMul, HPow.hPow, MeasureTheory.distribution, Inv.inv, funext, MonoidWithZero.toZero, GroupWithZero.inv_zero, ENNReal.rpow_zero, mul_one, Exists.intro, HAdd.hAdd and 7 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm'_toReal_le line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Real, LE.le, OfNat.ofNat, MeasureTheory.wnorm', Function.comp, ENNReal.toReal
Proof uses: iSup_mono, NNReal, HMul.hMul, HPow.hPow, MeasureTheory.distribution, Inv.inv, mul_le_mul', le_refl, ENNReal.rpow_le_rpow, MeasureTheory.distribution_mono_left, of_eq_true, Filter.Eventually, ENorm.enorm, MeasureTheory.ae, Eq.trans, True, congrFun', Filter, congrArg, funext and 1 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm'_toReal_eq line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Real, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Eq, MeasureTheory.wnorm', Function.comp, ENNReal.toReal
Proof uses: id, of_eq_true, iSup, NNReal, HMul.hMul, HPow.hPow, MeasureTheory.distribution, Inv.inv, Eq.trans, True, congrFun', congrArg, funext, MeasureTheory.distribution_toReal_eq, eq_self
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.wnorm'_eq_iSup_rpow_mul_rearrangement line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, Real, LT.lt, OfNat.ofNat, MeasureTheory.Measure, Eq, ENNReal, MeasureTheory.wnorm', iSup, NNReal, HMul.hMul, HPow.hPow, Inv.inv, MeasureTheory.rearrangement
Proof uses: Eq.mpr, id, Trans.trans, MeasureTheory.distribution, rfl, Max.max, Top.top, congrArg, ENNReal.iSup_ennreal, LE.le, Eq.trans, congrFun', MeasureTheory.distibution_top, ENNReal.zero_rpow_of_pos, MulZeroClass.mul_zero, zero_le, Eq.symm, of_eq_true, True, MeasureTheory.rearrangement_top and 56 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 102 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.wnorm The weak L^p norm of a function line 141 source
Source documentation
The weak L^p norm of a function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, ENNReal, MeasureTheory.Measure
Proof uses: ite, Eq, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.wnorm', ENNReal.toReal
3 instances, coercions and auxiliary constants left out.
```
def wnorm (f : α → ε) (p : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ :=
…
```
lemma MeasureTheory.wnorm_zero line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Eq, ENNReal, MeasureTheory.wnorm, OfNat.ofNat, Top.top
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite, MeasureTheory.eLpNormEssSup, MeasureTheory.wnorm', ENNReal.toReal, ite_eq_right_of_eq_false, MeasureTheory.wnorm'_zero, eq_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_top line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Eq, ENNReal, MeasureTheory.wnorm, Top.top, MeasureTheory.eLpNormEssSup
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, MeasureTheory.wnorm', ENNReal.toReal, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_ne_top line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Ne, Top.top, Eq, MeasureTheory.wnorm, MeasureTheory.wnorm', ENNReal.toReal
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_right_of_eq_false, MeasureTheory.eLpNormEssSup, eq_false, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_coe line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, NNReal, Eq, ENNReal, MeasureTheory.wnorm, MeasureTheory.wnorm'
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_right_of_eq_false, Top.top, MeasureTheory.eLpNormEssSup, ENNReal.toReal, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_ofReal line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Real, LE.le, OfNat.ofNat, Eq, ENNReal, MeasureTheory.wnorm, ENNReal.ofReal, MeasureTheory.wnorm'
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite, Top.top, MeasureTheory.eLpNormEssSup, ENNReal.toReal, ite_eq_right_of_eq_false, ENNReal.toReal_ofReal, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_toReal_le line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.wnorm, Real, Function.comp, ENNReal.toReal
Proof uses: ENNReal.recTopCoe, of_eq_true, Top.top, Eq.trans, MeasureTheory.eLpNormEssSup, True, congr, congrArg, MeasureTheory.wnorm_top, NNReal, MeasureTheory.wnorm'_toReal_le, ENNReal.toReal_nonneg
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_toReal_eq line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Eq, MeasureTheory.wnorm, Real, Function.comp, ENNReal.toReal
Proof uses: id, Eq.mpr, ite, MeasureTheory.eLpNormEssSup, MeasureTheory.wnorm', congrFun', congrArg, ite_congr, Eq.refl, MeasureTheory.eLpNormEssSup_toReal_eq, Not, of_eq_true, Eq.trans, True, MeasureTheory.wnorm'_toReal_eq, eq_self
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.wnorm_eq_iSup_rpow_mul_rearrangement line 168 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, ENNReal, Ne, OfNat.ofNat, Top.top, MeasureTheory.Measure, Eq, MeasureTheory.wnorm, iSup, NNReal, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, MeasureTheory.rearrangement
Proof uses: Eq.mpr, MeasureTheory.wnorm', id, congrArg, MeasureTheory.wnorm_ne_top, MeasureTheory.wnorm'_eq_iSup_rpow_mul_rearrangement, ENNReal.toReal_pos
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm'_mono_enorm_ae line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Real, LE.le, OfNat.ofNat, Filter.Eventually, ENNReal, ENorm.enorm, MeasureTheory.ae, MeasureTheory.wnorm'
Proof uses: id, iSup_le, NNReal, HMul.hMul, HPow.hPow, MeasureTheory.distribution, Inv.inv, iSup, Trans.trans, Eq, rfl, mul_le_mul', le_refl, ENNReal.rpow_le_rpow, MeasureTheory.distribution_mono_left, inv_nonneg_of_nonneg, le_iSup
57 instances, coercions and auxiliary constants left out.

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

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem MeasureTheory.wnorm_indicator_const line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Set, ENNReal, Not, Eq, OfNat.ofNat, Top.top, MeasureTheory.wnorm, Set.indicator, Function.const, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, ENorm.enorm
Proof uses: LT.lt, Eq.mpr, id, ENNReal.toReal_pos, MeasureTheory.wnorm', congrArg, MeasureTheory.wnorm_ne_top, iSup, NNReal, MeasureTheory.distribution, Set.Iio, congrFun', funext, MeasureTheory.distribution_indicator_const, le_antisymm, iSup_le, LE.le, dite, ite, Membership.mem and 78 more
164 instances, coercions and auxiliary constants left out.

Tactic trace: 84 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_iSup_of_monotone line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, Ne, OfNat.ofNat, Nat, Monotone, MeasureTheory.Measure, Eq, MeasureTheory.wnorm, iSup
Proof uses: id, ite, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.wnorm', ENNReal.toReal, NNReal, HMul.hMul, HPow.hPow, Real, MeasureTheory.distribution, Inv.inv, dite, Set, Set.ofPred, LT.lt, ENorm.enorm, Eq.mpr, congr, congrArg and 31 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.MemWLp A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm line 285 source
Source documentation
A function is in weak-L^p if it is (strongly a.e.)-measurable and has finite weak L^p norm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, TopologicalSpace, ENNReal, MeasureTheory.Measure
Proof uses: And, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.wnorm, Top.top
4 instances, coercions and auxiliary constants left out.
```
def MemWLp [TopologicalSpace ε] (f : α → ε) (p : ℝ≥0∞) (μ : Measure α) : Prop :=
…
```
lemma MeasureTheory.MemWLp_zero line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, TopologicalSpace, Not, MeasureTheory.MemWLp, OfNat.ofNat, ENNReal
Proof uses: of_eq_true, Eq.trans, False, True, congrArg, And, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.wnorm, Top.top, congrFun', MeasureTheory.wnorm_zero, and_false, not_false_eq_true
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.MemWLp.aeStronglyMeasurable line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, TopologicalSpace, MeasureTheory.MemWLp, MeasureTheory.AEStronglyMeasurable
Proof uses: And.left, LT.lt, MeasureTheory.wnorm, Top.top
4 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.MemWLp.wnorm_lt_top line 293 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, TopologicalSpace, MeasureTheory.MemWLp, LT.lt, MeasureTheory.wnorm, Top.top
Proof uses: And.right, MeasureTheory.AEStronglyMeasurable
8 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.MemWLp.ennreal_toReal line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, MeasureTheory.MemWLp, Real, Function.comp, ENNReal.toReal
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.wnorm, Top.top, MeasureTheory.AEStronglyMeasurable.ennreal_toReal, MeasureTheory.MemWLp.aeStronglyMeasurable, LE.le.trans_lt, MeasureTheory.wnorm_toReal_le, And.right
32 instances, coercions and auxiliary constants left out.
theorem MeasureTheory.MemWLp.ae_ne_top If a function f is MemWLp, then its norm is almost everywhere finite line 302 source
Source documentation
If a function f is MemWLp, then its norm is almost everywhere finite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, TopologicalSpace, MeasureTheory.MemWLp, Filter.Eventually, Ne, ENorm.enorm, Top.top, MeasureTheory.ae
Proof uses: dite, Eq, Eq.mpr, LT.lt, id, congrFun', Filter, congrArg, funext, ae_lt_of_essSup_lt, And.right, MeasureTheory.AEStronglyMeasurable, MeasureTheory.wnorm, Eq.mp, Filter.isBounded_le_of_top, Filter.map, Not, OfNat.ofNat, False.elim, MeasureTheory.MemWLp_zero and 92 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
theorem MemWLp.ae_ne_top [TopologicalSpace ε] (hf : MemWLp f p μ) : ∀ᵐ x ∂μ, ‖f x‖ₑ ≠ ∞ := by
…
```
Mentions: MeasureTheory.MemWLp
lemma MeasureTheory.distribution_le line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ContinuousENorm, OpensMeasurableSpace, ENNReal, Ne, OfNat.ofNat, MeasureTheory.Measure, AEMeasurable, LE.le, MeasureTheory.distribution, HMul.hMul, Inv.inv, MeasureTheory.lintegral, ENorm.enorm
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', MeasureTheory.distibution_top, ENNReal.inv_top, MulZeroClass.zero_mul, Not, Iff.mp, ENNReal.mul_le_iff_le_inv, id, Eq.mpr, Set, Set.ofPred, LT.lt and 16 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm'_le_eLpNorm' line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Real, LT.lt, OfNat.ofNat, LE.le, ENNReal, MeasureTheory.wnorm', MeasureTheory.eLpNorm'
Proof uses: iSup_le, NNReal, HMul.hMul, HPow.hPow, MeasureTheory.distribution, Inv.inv, id, Set, Set.ofPred, ENorm.enorm, HDiv.hDiv, LT.lt.le, div_pos, one_pos, Eq, of_eq_true, Eq.trans, True, congrArg, funext and 25 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_lt_top line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.MemLp, LT.lt, OfNat.ofNat, Ne, Top.top, NNReal, MeasureTheory.distribution
Proof uses: LE.le, MeasureTheory.wnorm', ENNReal.toReal, MeasureTheory.eLpNorm', MeasureTheory.wnorm'_le_eLpNorm', And.left, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm, ENNReal.toReal_pos, LT.lt.ne', LE.le.trans_lt, Eq.mp, congrArg, Eq.symm, MeasureTheory.eLpNorm_eq_eLpNorm', And.right, And, HMul.hMul, HPow.hPow, Real and 16 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_le_eLpNorm line 399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, ENNReal, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.wnorm, MeasureTheory.eLpNorm
Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, MeasureTheory.eLpNormEssSup, True, congr, congrArg, ite_eq_left_of_eq_true, MeasureTheory.wnorm', ENNReal.toReal, congrFun', eq_self, ite, MeasureTheory.eLpNorm', ite_eq_right_of_eq_false, False, Not, Eq.mpr and 5 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.MemLp.memWLp line 405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, LT.lt, OfNat.ofNat, MeasureTheory.MemLp, MeasureTheory.MemWLp
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.wnorm, Top.top, And.left, MeasureTheory.eLpNorm, LE.le.trans_lt, MeasureTheory.wnorm_le_eLpNorm, And.right
13 instances, coercions and auxiliary constants left out.
def MeasureTheory.HasWeakType An operator has weak type (p, q) if it is bounded as a map from L^p to weak L^q line 418 source
Source documentation
An operator has weak type (p, q) if it is bounded as a map from L^p to weak L^q. HasWeakType T p p' μ ν c means that T has weak type (p, p') w.r.t. measures μ, ν and constant c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, TopologicalSpace, ENNReal, MeasureTheory.Measure
Proof uses: MeasureTheory.MemLp, And, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm
6 instances, coercions and auxiliary constants left out.
```
def HasWeakType (T : (α → ε₁) → (α' → ε₂)) (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α')
    (c : ℝ≥0∞) : Prop :=
…
```
Mentions: T, α', c
def MeasureTheory.HasBoundedWeakType A weaker version of HasWeakType line 423 source
Source documentation
A weaker version of HasWeakType.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, TopologicalSpace, Zero, MeasurableSpace, ENNReal, MeasureTheory.Measure
Proof uses: BoundedFiniteSupport, And, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm
6 instances, coercions and auxiliary constants left out.
```
def HasBoundedWeakType {α α' : Type*} [Zero ε₁]
    {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → ε₁) → (α' → ε₂))
    (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0∞) : Prop :=
…
```
Mentions: α', T, c
def MeasureTheory.HasStrongType An operator has strong type (p, q) if it is bounded as an operator on L^p → L^q line 432 source
Source documentation
An operator has strong type (p, q) if it is bounded as an operator on L^p → L^q. HasStrongType T p p' μ ν c means that T has strong type (p, p') w.r.t. measures μ, ν and constant c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, TopologicalSpace, MeasurableSpace, ENNReal, MeasureTheory.Measure
Proof uses: MeasureTheory.MemLp, And, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul
6 instances, coercions and auxiliary constants left out.
```
def HasStrongType {α α' : Type*}
    {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → ε₁) → (α' → ε₂))
    (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0∞) : Prop :=
…
```
Mentions: α', T, c
lemma MeasureTheory.HasWeakType.memWLp line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.HasWeakType, MeasureTheory.MemLp, autoParam, LT.lt, Top.top, MeasureTheory.MemWLp
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.wnorm, And.left, LE.le, HMul.hMul, MeasureTheory.eLpNorm, LE.le.trans_lt, And.right, ENNReal.mul_lt_top
17 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasWeakType.toReal line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.HasWeakType, Real, ENNReal.toReal
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm, MeasureTheory.AEStronglyMeasurable.ennreal_toReal, And.left, LE.le.trans, Function.comp, MeasureTheory.wnorm_toReal_le, And.right
36 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.toReal_ofReal_preimage' line 458 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, Eq, Set.preimage, Real, ENNReal.toReal, ENNReal.ofReal, ite, Iff, Membership.mem, Top.top, OfNat.ofNat, Classical.propDecidable, Union.union, Singleton.singleton, SDiff.sdiff
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Set.ext, NNReal, of_eq_true, Option.none, Eq.trans, True, congr, ENNReal.ofReal_of_nonpos, LE.le, propext, iff_self, Option.some, congrFun', ENNReal.ofReal_coe_nnreal, Not and 19 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.toReal_ofReal_preimage line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, ENNReal, Eq, ite, Iff, Membership.mem, Top.top, OfNat.ofNat, Classical.propDecidable, Set.preimage, Real, ENNReal.toReal, ENNReal.ofReal, SDiff.sdiff, Singleton.singleton, Union.union
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Set.ext, NNReal, of_eq_true, Option.none, Eq.trans, True, congr, propext, ENNReal.ofReal_of_nonpos, LE.le, iff_self, Option.some, ENNReal.ofReal_coe_nnreal, Not, ite_eq_right and 19 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff move line 469 source
Source comment
move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, MeasureTheory.NullMeasurableSet, Set.preimage, Singleton.singleton, Set, Top.top, Iff, MeasureTheory.AEStronglyMeasurable, Real, Function.comp, ENNReal.toReal
Proof uses: Iff.intro, AEMeasurable.aestronglyMeasurable, MeasureTheory.NullMeasurable.aemeasurable, MeasurableSet, ENNReal.ofReal, AEMeasurable.nullMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasurableSet.preimage, ENNReal.measurable_ofReal, Eq.mpr, ite, Membership.mem, OfNat.ofNat, Classical.propDecidable, SDiff.sdiff, Union.union, id, Eq, congrArg, MeasureTheory.toReal_ofReal_preimage and 9 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma aestronglyMeasurable_ennreal_toReal_iff {f : α → ℝ≥0∞}
    (hf : NullMeasurableSet (f ⁻¹' {∞}) μ) :
    AEStronglyMeasurable (ENNReal.toReal ∘ f) μ ↔ AEStronglyMeasurable f μ := by
…
```
lemma MeasureTheory.hasWeakType_toReal_iff line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.MemLp, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Iff, MeasureTheory.HasWeakType, Real, ENNReal.toReal
Proof uses: Iff.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm, And, And.intro, Eq.mpr, Function.comp, id, Eq, congrArg, Eq.symm, propext, MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff, MeasureTheory.NullMeasurableSet.of_null, Set.preimage, Singleton.singleton, Set and 16 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.hasWeakType_iSup_of_monotone line 495 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, Nat, Monotone, Ne, OfNat.ofNat, MeasureTheory.HasWeakType, iSup
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm, AEMeasurable.aestronglyMeasurable, AEMeasurable.iSup, MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Eq.mpr, id, Eq, congrArg, MeasureTheory.wnorm_iSup_of_monotone, Monotone.apply₂, iSup_le, And.right
48 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.HasBoundedWeakType.memWLp line 523 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENorm, MeasureTheory.HasBoundedWeakType, BoundedFiniteSupport, autoParam, LT.lt, Top.top, MeasureTheory.MemWLp
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.wnorm, And.left, LE.le, HMul.hMul, MeasureTheory.eLpNorm, LE.le.trans_lt, And.right, ENNReal.mul_lt_top, BoundedFiniteSupport.memLp
27 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasWeakType.hasBoundedWeakType line 528 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENorm, MeasureTheory.HasWeakType, MeasureTheory.HasBoundedWeakType
Proof uses: BoundedFiniteSupport, BoundedFiniteSupport.memLp
12 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasStrongType.memLp line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.HasStrongType, MeasureTheory.MemLp, autoParam, LT.lt, Top.top
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm, And.left, LE.le, HMul.hMul, LE.le.trans_lt, And.right, ENNReal.mul_lt_top
17 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasStrongType.hasWeakType line 545 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, LT.lt, OfNat.ofNat, MeasureTheory.HasStrongType, MeasureTheory.HasWeakType
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm, And.left, LE.le.trans, MeasureTheory.wnorm_le_eLpNorm, And.right
18 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasStrongType.toReal line 549 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.HasStrongType, Real, ENNReal.toReal
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul, MeasureTheory.AEStronglyMeasurable.ennreal_toReal, And.left, LE.le.trans, Function.comp, MeasureTheory.eLpNorm_toReal_le, And.right
36 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.hasStrongType_toReal_iff line 553 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.MemLp, Filter.Eventually, Ne, Top.top, MeasureTheory.ae, Iff, MeasureTheory.HasStrongType, Real, ENNReal.toReal
Proof uses: Iff.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul, And, And.intro, Eq.mpr, Function.comp, id, Eq, congrArg, Eq.symm, propext, MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff, MeasureTheory.NullMeasurableSet.of_null, Set.preimage, Singleton.singleton, Set, Iff.mpr and 15 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.hasStrongType_iSup_of_monotone line 564 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, Nat, Monotone, MeasureTheory.HasStrongType, iSup
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul, AEMeasurable.aestronglyMeasurable, AEMeasurable.iSup, MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Eq.mpr, id, Eq, congrArg, MeasureTheory.eLpNorm_iSup', MeasureTheory.ae_of_all, Monotone.apply₂, iSup_le, And.right
46 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.HasBoundedStrongType.memLp line 589 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, MeasureTheory.HasBoundedStrongType, BoundedFiniteSupport, autoParam, LT.lt, Top.top, MeasureTheory.MemLp
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm, And.left, LE.le, HMul.hMul, LE.le.trans_lt, And.right, ENNReal.mul_lt_top, BoundedFiniteSupport.memLp
27 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasStrongType.hasBoundedStrongType line 594 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, MeasureTheory.HasStrongType, MeasureTheory.HasBoundedStrongType
Proof uses: BoundedFiniteSupport, BoundedFiniteSupport.memLp
12 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasBoundedStrongType.hasBoundedWeakType line 598 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ContinuousENorm, LT.lt, OfNat.ofNat, MeasureTheory.HasBoundedStrongType, MeasureTheory.HasBoundedWeakType
Proof uses: BoundedFiniteSupport, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm, And.left, LE.le.trans, MeasureTheory.wnorm_le_eLpNorm, And.right
28 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasBoundedStrongType.const_smul line 605 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.HasBoundedStrongType, NNReal, HSMul.hSMul
Proof uses: BoundedFiniteSupport, Eq.mpr, And, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul, id, Eq, congrArg, Pi.smul_apply, ENorm.enorm, MeasureTheory.eLpNorm_const_smul', And.intro, MeasureTheory.AEStronglyMeasurable.const_smul, And.left, le_of_le_of_eq, mul_le_mul_right, And.right, congr and 4 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_smul_left Documented declaration: distribution_smul_left line 625 source
Source comment
TODO: this lemma and its primed version could be unified using a `NormedSemifield` typeclass (which includes NNReal and normed fields like ℝ and ℂ), i.e. assuming 𝕜 is a normed semifield. Investigate if this is worthwhile when upstreaming this to mathlib.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddCommMonoid, SMul, NNReal, ENormSMulClass, Ne, OfNat.ofNat, Eq, MeasureTheory.distribution, HSMul.hSMul, HDiv.hDiv, ENorm.enorm
Proof uses: rfl, Eq.mpr, id, congrArg, propext, enorm_ne_zero, Iff.mpr, ENNReal.coe_ne_zero, eq_of_heq, Set, Set.ofPred, LT.lt, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Eq.rec, funext, Iff and 9 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma distribution_smul_left {f : α → ε'} {c : ℝ≥0} (hc : c ≠ 0) :
    distribution (c • f) t μ = distribution f (t / ‖c‖ₑ) μ := by
…
```
Mentions: c, MeasureTheory.distribution
lemma MeasureTheory.distribution_smul_left' line 640 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NontriviallyNormedField, ENNReal, NormedAddCommGroup, MulActionWithZero, NormSMulClass, Ne, OfNat.ofNat, Eq, MeasureTheory.distribution, HSMul.hSMul, HDiv.hDiv, ENorm.enorm
Proof uses: Iff.mpr, enorm_ne_zero, id, eq_of_heq, Set, Set.ofPred, LT.lt, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Eq.rec, funext, propext, Iff, Eq.mpr, HMul.hMul, congrArg, Eq.symm and 7 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.HasStrongType.const_smul line 649 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENorm, ESeminormedAddCommMonoid, SMul, NNReal, ENormSMulClass, ContinuousConstSMul, MeasureTheory.HasStrongType, HSMul.hSMul, HMul.hMul, ENorm.enorm
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, MeasureTheory.AEStronglyMeasurable.const_smul, And.left, LE.le.trans, MeasureTheory.eLpNorm_const_nnreal_smul_le, Eq.mpr, id, Eq, congrArg, mul_assoc, mul_le_mul', le_refl, And.right
38 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.HasStrongType.const_smul' line 661 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENorm, NormedRing, NormedAddCommGroup, MulActionWithZero, IsBoundedSMul, MeasureTheory.HasStrongType, HSMul.hSMul, HMul.hMul, ENorm.enorm
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, MeasureTheory.AEStronglyMeasurable.const_smul, And.left, LE.le.trans, MeasureTheory.eLpNorm_const_smul_le, Eq.mpr, id, Eq, congrArg, mul_assoc, mul_le_mul', le_refl, And.right
88 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.HasStrongType.const_mul line 669 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENorm, MeasureTheory.HasStrongType, NNReal, HMul.hMul, ENorm.enorm
Proof uses: MeasureTheory.HasStrongType.const_smul
22 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasStrongType.const_mul' line 677 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENorm, NormedRing, MeasureTheory.HasStrongType, HMul.hMul, ENorm.enorm
Proof uses: MeasureTheory.HasStrongType.const_smul'
35 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.wnorm_const_smul_le line 684 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddCommMonoid, Module, NNReal, ENormSMulClass, Ne, OfNat.ofNat, LE.le, MeasureTheory.wnorm, HSMul.hSMul, HMul.hMul, ENorm.enorm
Proof uses: dite, Eq, Top.top, Eq.mpr, MeasureTheory.eLpNormEssSup, id, congr, congrArg, Eq.trans, congrFun', MeasureTheory.wnorm_top, MeasureTheory.eLpNormEssSup_const_nnreal_smul_le, Not, HPow.hPow, Real, MeasureTheory.distribution, Inv.inv, ENNReal.toReal, iSup, ite_eq_right_of_eq_false and 36 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.wnorm_const_smul_le' line 706 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, NontriviallyNormedField, NormedAddCommGroup, MulActionWithZero, NormSMulClass, IsBoundedSMul, Ne, OfNat.ofNat, LE.le, MeasureTheory.wnorm, HSMul.hSMul, HMul.hMul, ENorm.enorm
Proof uses: dite, Eq, Top.top, Eq.mpr, MeasureTheory.eLpNormEssSup, id, congr, congrArg, Eq.trans, congrFun', MeasureTheory.wnorm_top, MeasureTheory.eLpNormEssSup_const_smul_le, Not, NNReal, HPow.hPow, Real, MeasureTheory.distribution, Inv.inv, ENNReal.toReal, iSup and 39 more
175 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.HasWeakType.const_smul line 731 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENorm, ESeminormedAddCommMonoid, Module, NNReal, ENormSMulClass, ContinuousConstSMul, Ne, OfNat.ofNat, MeasureTheory.HasWeakType, HSMul.hSMul, HMul.hMul
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, MeasureTheory.eLpNorm, MeasureTheory.AEStronglyMeasurable.const_smul, And.left, Trans.trans, Eq, rfl, id, Eq.mp, ENorm.enorm, congrArg, congrFun', enorm_NNReal, MeasureTheory.wnorm_const_smul_le, mul_le_mul', le_refl and 4 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.HasWeakType.const_smul' TODO: do we want to unify this lemma with its unprimed version, perhaps using an ENormedSemiring class? line 745 source
Source comment
TODO: do we want to unify this lemma with its unprimed version, perhaps using an `ENormedSemiring` class?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, NontriviallyNormedField, TopologicalSpace, ENorm, NormedAddCommGroup, MulActionWithZero, NormSMulClass, IsBoundedSMul, Ne, OfNat.ofNat, MeasureTheory.HasWeakType, HSMul.hSMul, HMul.hMul, ENorm.enorm
Proof uses: MeasureTheory.MemLp, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.wnorm, MeasureTheory.eLpNorm, MeasureTheory.AEStronglyMeasurable.smul, MeasureTheory.aestronglyMeasurable_const, And.left, Trans.trans, Eq, rfl, of_eq_true, eq_true, MeasureTheory.wnorm_const_smul_le', mul_le_mul', le_refl, And.right, Eq.mpr, id and 3 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma HasWeakType.const_smul' [IsBoundedSMul 𝕜 E'] {T : (α → ε) → (α' → E')} (hp' : p' ≠ 0)
    {c : ℝ≥0∞} (h : HasWeakType T p p' μ ν c) (k : 𝕜) :
    HasWeakType (k • T) p p' μ ν (‖k‖ₑ * c) := by
…
```
Mentions: T, α', c, MeasureTheory.HasWeakType, k
lemma MeasureTheory.HasWeakType.const_mul line 757 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENorm, Ne, OfNat.ofNat, MeasureTheory.HasWeakType, NNReal, HMul.hMul
Proof uses: MeasureTheory.HasWeakType.const_smul
23 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.HasWeakType.const_mul' TODO: do we want to unify this lemma with its unprimed version, perhaps using an ENormedSemiring class? line 764 source
Source comment
TODO: do we want to unify this lemma with its unprimed version, perhaps using an `ENormedSemiring` class?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, NontriviallyNormedField, TopologicalSpace, ENorm, Ne, OfNat.ofNat, MeasureTheory.HasWeakType, HMul.hMul, ENorm.enorm
Proof uses: MeasureTheory.HasWeakType.const_smul'
53 instances, coercions and auxiliary constants left out.
```
lemma HasWeakType.const_mul' {T : (α → ε) → (α' → 𝕜)} (hp' : p' ≠ 0)
    {c : ℝ≥0∞} (h : HasWeakType T p p' μ ν c) (e : 𝕜) :
    HasWeakType (fun f x ↦ e * T f x) p p' μ ν (‖e‖ₑ * c) :=
…
```
Mentions: T, α', c, MeasureTheory.HasWeakType
lemma MeasureTheory._root_.ContinuousLinearMap.distribution_le line 776 source
lemma MeasureTheory.lintegral_norm_pow_eq_distribution The layer-cake theorem, or Cavalieri's principle for functions into a space with a continuous enorm line 801 source
Source documentation
The layer-cake theorem, or Cavalieri's principle for functions into a space with a continuous enorm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Real, LT.lt, OfNat.ofNat, Eq, ENNReal, MeasureTheory.lintegral, HPow.hPow, ENorm.enorm, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HMul.hMul, ENNReal.ofReal, HSub.hSub, MeasureTheory.distribution
Proof uses: ENNReal.toReal, Set, Set.ofPred, MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul, Filter.Eventually.of_forall, LE.le, MeasureTheory.ae, ENNReal.toReal_nonneg, AEMeasurable.ennreal_toReal, MeasureTheory.AEStronglyMeasurable.enorm, Eq.mpr, id, congrArg, funext, congrFun', ENNReal.ofReal_mul, LT.lt.le, dite, Top.top, eq_of_heq and 113 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_norm_pow_eq_distribution {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 0 < p) :
    ∫⁻ x, ‖f x‖ₑ ^ p ∂μ =
    ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (.ofReal t) μ := by
…
```
Mentions: MeasureTheory.distribution
lemma MeasureTheory.eLpNorm_pow_eq_distribution The layer-cake theorem, or Cavalieri's principle, written using eLpNorm line 868 source
Source documentation
The layer-cake theorem, or Cavalieri's principle, written using eLpNorm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, NNReal, LT.lt, OfNat.ofNat, Eq, ENNReal, HPow.hPow, Real, MeasureTheory.eLpNorm, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HMul.hMul, ENNReal.ofReal, HSub.hSub and 1 more
Proof uses: Eq.mpr, MeasureTheory.eLpNorm', id, congrFun', congrArg, ENorm, MeasureTheory.eLpNorm_nnreal_eq_eLpNorm', LT.lt.ne', ENorm.enorm, HDiv.hDiv, Inv.inv, one_div, inv_mul_cancel₀, ENNReal.rpow_one, MeasureTheory.lintegral_norm_pow_eq_distribution, funext, ENNReal.ofReal_mul, NNReal.zero_le_coe, of_eq_true, Eq.trans and 3 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_pow_eq_distribution {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ≥0} (hp : 0 < p) :
    eLpNorm f p μ ^ (p : ℝ) =
    ∫⁻ t in Ioi (0 : ℝ), p * ENNReal.ofReal (t ^ ((p : ℝ) - 1)) * distribution f (.ofReal t) μ := by
…
```
Mentions: MeasureTheory.distribution
lemma MeasureTheory.eLpNorm_eq_distribution The layer-cake theorem, or Cavalieri's principle, written using eLpNorm, without taking powers line 878 source
Source documentation
The layer-cake theorem, or Cavalieri's principle, written using eLpNorm, without taking powers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Real, LT.lt, OfNat.ofNat, Eq, ENNReal, MeasureTheory.eLpNorm, ENNReal.ofReal, HPow.hPow, HMul.hMul, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, MeasureTheory.distribution, HSub.hSub and 1 more
Proof uses: id, dite, ite, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', ENNReal.toReal, Eq.mpr, congrFun', congrArg, ite_eq_left, False.elim, not_le_of_gt, Iff.mp, LE.le, ENNReal.ofReal_eq_zero, Not, ite_eq_right, ENNReal.coe_ne_top, Real.toNNReal and 31 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_eq_distribution {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 0 < p) :
    eLpNorm f (.ofReal p) μ =
    (ENNReal.ofReal p  * ∫⁻ t in Ioi (0 : ℝ), distribution f (.ofReal t) μ *
        ENNReal.ofReal (t ^ (p - 1)) ) ^ p⁻¹ := by
…
```
Mentions: MeasureTheory.distribution
lemma MeasureTheory.lintegral_pow_mul_distribution line 892 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, Real, LT.lt, Neg.neg, OfNat.ofNat, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HMul.hMul, ENNReal.ofReal, HPow.hPow, MeasureTheory.distribution, Inv.inv and 2 more
Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add and 50 more
111 instances, coercions and auxiliary constants left out.

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

Carleson/ToMathlib/WeakType.lean

Lemmas about HasWeakType

`Carleson/ToMathlib/WeakType.lean`

Lemmas about `HasWeakType`