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

90 declarations, 0 contain sorry, 0 declared as axioms

This file contains some miscellaneous prerequisites for proving the Marcinkiewisz real interpolation theorem. There are the following sections:

Interface for using cutoff functions
Results about the particular choice of scale
Some tools for measure theory computations
Results about truncations of a function
Measurability properties of truncations
Truncations and Lp spaces

Upstreaming status:

measure theory computations are basically ready
truncations and their properties definitely belong into mathlib
the details about cutoff functions and a particular scale function will depend on the particular proof chosen: design on the overall proof approach first
except for using distribution_lt_top, this file does not use WeakType; it does use helper lemmas in InterpolatedExponents, though.

Imports (2)

Imported by 4 files

structure ScaledPowerFunction A ScaledPowerFunction is meant to represent a function of the form t ↦ (t / d)^σ, where d is strictly positive and either σ > 0 or σ < 0 line 40 source
Source documentation
A ScaledPowerFunction is meant to represent a function of the form t ↦ (t / d)^σ, where d is strictly positive and either σ > 0 or σ < 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure ScaledPowerFunction where
…
```
structure ToneCouple A ToneCouple is a couple of two monotone functions that are practically inverses of each other line 54 source
Source documentation
A ToneCouple is a couple of two monotone functions that are practically inverses of each other. It is used in the proof of the real interpolation theorem.
Note: originally it seemed useful to make the possible choice of this function general in the proof of the real inteprolation theorem. However, in the end really only one function works for all the different cases. This infrastructure, however, could potentially still be useful, if one would like to try to improve the constant.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure ToneCouple where
…
```
structure StrictRangeToneCouple A StrictRangeToneCouple is a ToneCouple for which the functions in the couple, when restricted to Ioo 0 ∞, map to Ioo 0 ∞ line 67 source
Source documentation
A StrictRangeToneCouple is a ToneCouple for which the functions in the couple, when restricted to Ioo 0 ∞, map to Ioo 0 ∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure StrictRangeToneCouple extends ToneCouple where
…
```
Mentions: ToneCouple
def spf_to_tc A scaled power function gives rise to a ToneCouple line 74 source
Source documentation
A scaled power function gives rise to a ToneCouple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ScaledPowerFunction, StrictRangeToneCouple
Proof uses: StrictRangeToneCouple.mk, ToneCouple.mk, ENNReal, HPow.hPow, Real, HDiv.hDiv, ScaledPowerFunction.d, ScaledPowerFunction.σ, HMul.hMul, Inv.inv, ite, Bool, LT.lt, OfNat.ofNat, Bool.true, Bool.false
19 instances, coercions and auxiliary constants left out.

Tactic trace: 82 steps
Open to load the checked before-and-after goal states.
```
def spf_to_tc (spf : ScaledPowerFunction) : StrictRangeToneCouple where
…
```
Mentions: ScaledPowerFunction, StrictRangeToneCouple
def ChoiceScale.d line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm
Proof uses: HDiv.hDiv, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, Inv.inv, HSub.hSub, MeasureTheory.eLpNorm
16 instances, coercions and auxiliary constants left out.
lemma ChoiceScale.d_pos_aux₀ line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Top.top, MeasureTheory.eLpNorm, LT.lt, HPow.hPow, Real, ENNReal.toReal
Proof uses: ENNReal.rpow_pos, pos_of_gt, And.left, ENNReal.ne_top_of_Ioo
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_ne_top_aux₀ line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Top.top, Ne, HPow.hPow
Proof uses: LT.lt, And.left, And.right, ENNReal.rpow_ne_top_of_ne_zero, ne_of_gt, ENNReal.ne_top_of_Ioo
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_ne_zero_aux₀ line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Top.top, MeasureTheory.eLpNorm, Ne, HPow.hPow, ENNReal.toReal
Proof uses: LT.lt.ne', ENNReal.rpow_pos, ChoiceScale.d_pos_aux₀, ChoiceScale.d_ne_top_aux₀
16 instances, coercions and auxiliary constants left out.
lemma ChoiceScale.d_ne_zero_aux₂ line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, NNReal, Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Top.top, MeasureTheory.eLpNorm, Ne, HMul.hMul, HPow.hPow, ENNReal.toReal
Proof uses: LT.lt.ne', ENNReal.mul_pos, ne_of_gt, ENNReal.rpow_pos, Iff.mpr, ENNReal.coe_pos, ENNReal.coe_ne_top, ChoiceScale.d_ne_zero_aux₀
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_ne_top_aux₂ line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Top.top, MeasureTheory.eLpNorm, Ne, HPow.hPow, ENNReal.toReal
Proof uses: ENNReal.rpow_ne_top', LT.lt.ne', ChoiceScale.d_pos_aux₀, ChoiceScale.d_ne_top_aux₀
16 instances, coercions and auxiliary constants left out.
lemma ChoiceScale.d_ne_top_aux₃ line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, ENorm, NNReal, Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Top.top, MeasureTheory.eLpNorm, Ne, HMul.hMul, HPow.hPow, ENNReal.toReal
Proof uses: ENNReal.mul_ne_top, ENNReal.rpow_ne_top_of_ne_zero, ne_of_gt, Iff.mpr, ENNReal.coe_pos, ENNReal.coe_ne_top, ChoiceScale.d_ne_top_aux₂
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_ne_zero_aux₃ line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Top.top, MeasureTheory.eLpNorm, Ne, HDiv.hDiv, HMul.hMul, HPow.hPow, ENNReal.toReal
Proof uses: Iff.mpr, And, ENNReal.div_ne_zero, And.intro, ChoiceScale.d_ne_zero_aux₂, ChoiceScale.d_ne_top_aux₃
40 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_ne_top_aux₄ line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Top.top, MeasureTheory.eLpNorm, Ne, HDiv.hDiv, HMul.hMul, HPow.hPow, ENNReal.toReal
Proof uses: LT.lt.ne, ENNReal.div_lt_top, ChoiceScale.d_ne_top_aux₃, ChoiceScale.d_ne_zero_aux₂
40 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_pos If the p-norm of f is positive and finite, then d is positive line 207 source
Source comment
If the `p`-norm of `f` is positive and finite, then `d` is positive

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Top.top, MeasureTheory.eLpNorm, GT.gt, ChoiceScale.d
Proof uses: pos_of_ne_zero, ChoiceScale.d_ne_zero_aux₃, HDiv.hDiv, Real, HMul.hMul, ENNReal.toReal, Inv.inv, HSub.hSub
33 instances, coercions and auxiliary constants left out.
```
lemma d_pos (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hF : eLpNorm f p μ ∈ Ioo 0 ⊤) :
    @d α ε m p p₀ q₀ p₁ q₁ C₀ C₁ μ _ f > 0 :=
…
```
Mentions: ChoiceScale.d
lemma ChoiceScale.d_ne_top line 212 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, Top.top, MeasureTheory.eLpNorm, Ne, ChoiceScale.d
Proof uses: Eq.mpr, HDiv.hDiv, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, Inv.inv, HSub.hSub, id, Eq, congrArg, ChoiceScale.d.eq_1, ChoiceScale.d_ne_top_aux₄
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_eq_top₀ line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, LT.lt, OfNat.ofNat, Ne, Top.top, Eq, ChoiceScale.d, HPow.hPow, Real, HMul.hMul, ENNReal.toReal, MeasureTheory.eLpNorm, Inv.inv
Proof uses: id, Eq.mpr, HDiv.hDiv, HSub.hSub, congrArg, congrFun', Eq.trans, congr, ENNReal.inv_top, sub_zero, zero_div, ENNReal.rpow_zero, MulZeroClass.mul_zero, mul_one, div_one, mul_div_cancel_right₀, LT.lt.ne', ComputationsInterpolatedExponents.inv_toReal_pos_of_ne_top, Ne.symm, Eq.rec and 10 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_eq_top₁ line 231 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, LT.lt, OfNat.ofNat, Ne, Top.top, Eq, ChoiceScale.d, HPow.hPow, Real, HMul.hMul, ENNReal.toReal, MeasureTheory.eLpNorm, Inv.inv
Proof uses: id, Eq.mpr, HDiv.hDiv, HSub.hSub, congrArg, Neg.neg, congrFun', Eq.trans, congr, ENNReal.inv_top, zero_sub, zero_div, ENNReal.rpow_zero, MulZeroClass.mul_zero, mul_one, one_div, div_neg, mul_div_cancel_right₀, LT.lt.ne', ComputationsInterpolatedExponents.inv_toReal_pos_of_ne_top and 24 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_eq_top_of_eq line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, LT.lt, OfNat.ofNat, Ne, Top.top, Eq, ChoiceScale.d, HMul.hMul, MeasureTheory.eLpNorm
Proof uses: Eq.mpr, HPow.hPow, Real, ENNReal.toReal, Inv.inv, id, congrArg, ChoiceScale.d_eq_top₁, Eq.rec, Eq.symm, ENNReal.mul_rpow_of_nonneg, inv_nonneg_of_nonneg, ENNReal.toReal_nonneg, ENNReal.rpow_rpow_inv, LT.lt.ne', ENNReal.toReal_pos, Eq.refl
47 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma ChoiceScale.d_eq_top_top line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, LT.lt, OfNat.ofNat, Ne, Eq, Top.top, ChoiceScale.d
Proof uses: id, Eq.mpr, HDiv.hDiv, HMul.hMul, HPow.hPow, Real, ENNReal.toReal, Inv.inv, HSub.hSub, MeasureTheory.eLpNorm, congrArg, Neg.neg, congrFun', Eq.trans, congr, ENNReal.inv_top, zero_sub, zero_div, ENNReal.rpow_zero, MulZeroClass.mul_zero and 17 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def ChoiceScale.spf_ch The particular choice of scaled power function that works in the proof of the real interpolation theorem line 275 source
Source documentation
The particular choice of scaled power function that works in the proof of the real interpolation theorem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, NNReal, MeasureTheory.Measure, ENorm, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Ne, LT.lt, Top.top, MeasureTheory.eLpNorm, ScaledPowerFunction
Proof uses: ScaledPowerFunction.mk, ComputationsChoiceExponent.ζ, ChoiceScale.d, ChoiceScale.d_pos
28 instances, coercions and auxiliary constants left out.
```
def spf_ch {t : ℝ} (ht : t ∈ Ioo 0 1) (hq₀q₁ : q₀ ≠ q₁) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀)
    (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hF : eLpNorm f p μ ∈ Ioo 0 ⊤) :
    ScaledPowerFunction where
…
```
Mentions: ScaledPowerFunction
lemma MeasureTheory.lintegral_double_restrict_set TODO: change lhs and rhs? line 304 source
Source comment
TODO: change lhs and rhs? TODO: rewrite the condition in filter form?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Set, ENNReal, MeasurableSet, Filter.Eventually, Membership.mem, SDiff.sdiff, LE.le, OfNat.ofNat, MeasureTheory.ae, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Inter.inter
Proof uses: MeasureTheory.setLIntegral_mono_ae', MeasurableSet.diff, Eq.mpr, HAdd.hAdd, id, congrArg, Eq.symm, MeasureTheory.lintegral_inter_add_sdiff, Iff.mp, nonpos_iff_eq_zero, Eq.mp, MeasureTheory.lintegral_zero, add_zero, Eq.refl
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_double_restrict_set {A B : Set α} {f : α → ℝ≥0∞} (hA : MeasurableSet A)
  (hB : MeasurableSet B) (hf : ∀ᵐ (x : α) ∂μ, x ∈ A \ B → f x ≤ 0) :
    ∫⁻ x in A, f x ∂μ = ∫⁻ x in A ∩ B, f x ∂μ := by
…
```
Mentions: A
lemma MeasureTheory.lintegral_rw_aux local convenience function line 311 source
Source comment
local convenience function

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, Set, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Eq, MeasureTheory.lintegral, HMul.hMul
Proof uses: MeasureTheory.lintegral_rw₂, Filter.EventuallyEq.refl
18 instances, coercions and auxiliary constants left out.
```
lemma lintegral_rw_aux {g : ℝ → ℝ≥0∞} {f₁ f₂ : ℝ → ℝ≥0∞} {A : Set ℝ}
    (heq : f₁ =ᶠ[ae (volume.restrict A)] f₂) :
    ∫⁻ s in A, g s * f₁ s = ∫⁻ s in A, g s * f₂ s :=
…
```
Mentions: g, A, s
lemma MeasureTheory.power_aux line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, HPow.hPow, ENNReal.ofReal, HAdd.hAdd, HMul.hMul
Proof uses: Filter.mp_mem, Set.ofPred, Eq, MeasureTheory.self_mem_ae_restrict, measurableSet_Ioi, Filter.univ_mem', Membership.mem, Set, id, Eq.mpr, congrArg, ENNReal.ofReal_rpow_of_pos, Eq.symm, ENNReal.ofReal_mul, le_of_lt, Real.rpow_pos_of_pos, Real.rpow_add, Eq.refl
53 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.power_aux_2 line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, ENNReal.ofReal, HPow.hPow, HAdd.hAdd, HMul.hMul
Proof uses: Filter.mp_mem, Set.ofPred, Eq, MeasureTheory.self_mem_ae_restrict, measurableSet_Ioi, Filter.univ_mem', Membership.mem, Set, id, Eq.mpr, congrArg, Eq.symm, ENNReal.ofReal_mul, le_of_lt, Real.rpow_pos_of_pos, Real.rpow_add, Eq.refl
52 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.power_aux_3 line 329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, HPow.hPow, HAdd.hAdd, HMul.hMul
Proof uses: Filter.mp_mem, Set.ofPred, Eq, Set.Ioo, OfNat.ofNat, Top.top, Set.univ, Ioo_zero_top_ae_eq_univ, Filter.univ_mem', Membership.mem, Set, id, ENNReal.rpow_add, Ne, Not, And.left, LT.lt, Iff.mpr, And, Eq.mp and 9 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.power_aux_4 line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, ENNReal.ofReal, HPow.hPow
Proof uses: Filter.mp_mem, Set.ofPred, Eq, MeasureTheory.self_mem_ae_restrict, measurableSet_Ioi, Filter.univ_mem', Membership.mem, Set, id, Eq.mpr, congrArg, Eq.symm, ENNReal.ofReal_rpow_of_pos, Eq.refl
38 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ofReal_rpow_of_pos_aux line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, HPow.hPow, ENNReal.ofReal
Proof uses: Filter.mp_mem, Set.ofPred, Eq, MeasureTheory.self_mem_ae_restrict, measurableSet_Ioi, Filter.univ_mem', Membership.mem, Set, id, ENNReal.ofReal_rpow_of_pos
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.extract_constant_double_integral_rpow line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, ENNReal, GE.ge, OfNat.ofNat, Ne, Top.top, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HPow.hPow, HMul.hMul
Proof uses: Eq.mpr, id, congrArg, MeasurableSpace, MeasureTheory.Measure, Eq.symm, MeasureTheory.lintegral_const_mul', ENNReal.rpow_ne_top_of_nonneg, funext, ENNReal.mul_rpow_of_nonneg, of_eq_true, Eq.trans, True, congrFun', eq_self
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ofReal_rpow_rpow_aux line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Filter.EventuallyEq, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, HPow.hPow, ENNReal.ofReal
Proof uses: Filter.mp_mem, Set.ofPred, Eq, MeasureTheory.self_mem_ae_restrict, measurableSet_Ioi, Filter.univ_mem', Membership.mem, Set, id, ENNReal.ofReal_rpow_of_pos
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_rpow_of_gt line 362 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, Neg.neg, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioo, ENNReal.ofReal, HPow.hPow, HDiv.hDiv, HAdd.hAdd
Proof uses: lt_of_not_ge, 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, HMul.hMul, 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 61 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.trunc The t-truncation of a function f line 399 source
Source documentation
The t-truncation of a function f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, Zero, ENNReal
Proof uses: ite, LE.le, ENorm.enorm, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def trunc (f : α → ε') (t : ℝ≥0∞) (x : α) : ε' := if ‖f x‖ₑ ≤ t then f x else 0
```
lemma MeasureTheory.trunc_eq_indicator line 401 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, ENorm, Zero, Eq, MeasureTheory.trunc, Set.indicator, Set.ofPred, LE.le, ENorm.enorm
Proof uses: funext, id, ite, OfNat.ofNat, Membership.mem, Set, Classical.decPred, of_eq_true
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.trunc_top line 405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, Zero, Eq, MeasureTheory.trunc, Top.top, ENNReal
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.indicator, Set.ofPred, LE.le, ENorm.enorm, MeasureTheory.trunc_eq_indicator, Set.univ, Set, funext, Set.indicator_univ, eq_self
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.truncCompl The complement of a t-truncation of a function f line 408 source
Source documentation
The complement of a t-truncation of a function f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, Zero, ENNReal
Proof uses: ite, LE.le, ENorm.enorm, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def truncCompl (f : α → ε') (t : ℝ≥0∞) (x : α) : ε' := if ‖f x‖ₑ ≤ t then 0 else f x
```
lemma MeasureTheory.truncCompl_eq_indicator line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, ENorm, Zero, Eq, MeasureTheory.truncCompl, Set.indicator, Compl.compl, Set, Set.ofPred, LE.le, ENorm.enorm
Proof uses: funext, of_eq_true, ite, OfNat.ofNat, Eq.trans, True, congrArg, Membership.mem, Classical.decPred, Not, ite_congr, Eq.refl, ite_not, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.truncCompl_top line 415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, Zero, Eq, MeasureTheory.truncCompl, Top.top, ENNReal, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.indicator, Compl.compl, Set, Set.ofPred, LE.le, ENorm.enorm, MeasureTheory.truncCompl_eq_indicator, EmptyCollection.emptyCollection, Set.univ, funext, Set.compl_univ, Set.indicator_empty, 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.truncCompl_eq line 417 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, ENorm, Zero, Eq, MeasureTheory.truncCompl, ite, LT.lt, ENorm.enorm, OfNat.ofNat
Proof uses: funext, Eq.mpr, Not, id, congrArg, Eq.symm, ite_not, of_eq_true, LE.le, Eq.trans, True, ite_congr, Eq.refl, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.trnc A function to deal with truncations and complement of truncations in one go line 424 source
Source documentation
A function to deal with truncations and complement of truncations in one go.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, Zero, Bool, ENNReal
Proof uses: MeasureTheory.trnc.match_1, Unit, MeasureTheory.truncCompl, MeasureTheory.trunc
```
def trnc (j : Bool) (f : α → ε') (t : ℝ≥0∞) : α → ε' :=
…
```
lemma MeasureTheory.trnc_false line 430 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, ENorm, Zero, Eq, MeasureTheory.trnc, Bool.false, MeasureTheory.truncCompl
Proof uses: rfl
lemma MeasureTheory.trnc_true line 433 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, ENorm, Zero, Eq, MeasureTheory.trnc, Bool.true, MeasureTheory.trunc
Proof uses: rfl
lemma MeasureTheory.trunc_add_truncCompl A function is the complement if its truncation and the complement of the truncation line 439 source
Source documentation
A function is the complement if its truncation and the complement of the truncation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, Eq, HAdd.hAdd, MeasureTheory.trunc, MeasureTheory.truncCompl
Proof uses: funext, id, ite, LE.le, ENorm.enorm, OfNat.ofNat, dite, Eq.mpr, congrFun', congrArg, congr, ite_eq_left, of_eq_true, Eq.trans, True, add_zero, eq_self, Not, ite_eq_right, zero_add
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma trunc_add_truncCompl {t : ℝ≥0∞} : trunc f t + truncCompl f t = f := by
…
```
Mentions: MeasureTheory.trunc, MeasureTheory.truncCompl
lemma MeasureTheory.StronglyMeasurable.trunc line 488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.StronglyMeasurable, MeasureTheory.trunc
Proof uses: MeasureTheory.StronglyMeasurable.ite, OfNat.ofNat, LE.le, ENorm.enorm, MeasureTheory.StronglyMeasurable.measurableSet_le, Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.enorm, MeasureTheory.stronglyMeasurable_const
27 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.StronglyMeasurable.truncCompl line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.StronglyMeasurable, MeasureTheory.truncCompl
Proof uses: Eq.mpr, ite, LT.lt, ENorm.enorm, OfNat.ofNat, id, Eq, congrArg, MeasureTheory.truncCompl_eq, MeasureTheory.StronglyMeasurable.ite, MeasureTheory.StronglyMeasurable.measurableSet_lt, MeasureTheory.stronglyMeasurable_const, Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.enorm
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.trunc line 531 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.AEStronglyMeasurable, MeasureTheory.trunc
Proof uses: And, MeasureTheory.StronglyMeasurable, Filter.EventuallyEq, MeasureTheory.ae, Exists.intro, And.intro, Eq.mpr, Set.indicator, Set.ofPred, LE.le, ENorm.enorm, id, Eq, congrArg, MeasureTheory.trunc_eq_indicator, MeasureTheory.StronglyMeasurable.indicator, measurableSet_le, MeasureTheory.StronglyMeasurable.enorm, measurable_const, MeasureTheory.measure_mono_null and 19 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.truncCompl line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.AEStronglyMeasurable, MeasureTheory.truncCompl
Proof uses: And, MeasureTheory.StronglyMeasurable, Filter.EventuallyEq, MeasureTheory.ae, Exists.intro, And.intro, Eq.mpr, Set.indicator, Compl.compl, Set, Set.ofPred, LE.le, ENorm.enorm, id, Eq, congrArg, MeasureTheory.truncCompl_eq_indicator, MeasureTheory.StronglyMeasurable.indicator, MeasurableSet, measurableSet_le and 20 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.aestronglyMeasurable_trnc line 553 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, Bool, MeasureTheory.AEStronglyMeasurable, MeasureTheory.trnc
Proof uses: Bool.rec, MeasureTheory.AEStronglyMeasurable.truncCompl, MeasureTheory.AEStronglyMeasurable.trunc
12 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.trunc_le line 557 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, LE.le, ENorm.enorm, MeasureTheory.trunc, Max.max, OfNat.ofNat
Proof uses: id, dite, ite, Eq.mpr, Eq, congrFun', congrArg, ite_eq_left, LT.lt, Or, lt_or_ge, Trans.trans, LT.lt.le, le_max_left, le_max_right, Not, ite_eq_right, of_eq_true, Eq.trans, True and 3 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.coe_coe_eq_ofReal A small lemma that is helpful for rewriting line 566 source
Source documentation
A small lemma that is helpful for rewriting

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, ENNReal, Real.toNNReal, ENNReal.ofReal
Proof uses: Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma coe_coe_eq_ofReal (a : ℝ) : ofNNReal a.toNNReal = ENNReal.ofReal a := by rfl
```
lemma MeasureTheory.trunc_eLpNormEssSup_le line 568 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, LE.le, MeasureTheory.eLpNormEssSup, MeasureTheory.trunc, Max.max, OfNat.ofNat
Proof uses: essSup_le_of_ae_le, ENorm.enorm, MeasureTheory.ae_of_all, MeasureTheory.trunc_le, Filter.isCobounded_le_of_bot, Filter.map, MeasureTheory.ae
31 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.trunc_mono line 572 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, LE.le, ENorm.enorm, MeasureTheory.trunc
Proof uses: id, dite, ite, OfNat.ofNat, Eq.mpr, Eq, congrFun', congrArg, ite_eq_left, le_refl, Not, ite_eq_right, Decidable.byContradiction, ne_of_not_le, le_antisymm, le_trans, le_of_not_ge, enorm_zero, zero_le, le_rfl
26 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_trunc_mono The norm of the truncation is monotone in the truncation parameter line 581 source
Source documentation
The norm of the truncation is monotone in the truncation parameter

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Monotone, MeasureTheory.eLpNorm, MeasureTheory.trunc
Proof uses: LE.le, MeasureTheory.eLpNorm_mono_enorm, MeasureTheory.trunc_mono
17 instances, coercions and auxiliary constants left out.
```
lemma eLpNorm_trunc_mono :
    Monotone fun s ↦ eLpNorm (trunc f s) p μ :=
…
```
Mentions: s, MeasureTheory.trunc
lemma MeasureTheory.trunc_buildup_enorm line 585 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, Eq, HAdd.hAdd, ENorm.enorm, MeasureTheory.trunc, MeasureTheory.truncCompl
Proof uses: id, dite, ite, LE.le, OfNat.ofNat, Eq.mpr, congrFun', congrArg, congr, ite_eq_left, of_eq_true, Eq.trans, True, enorm_zero, add_zero, eq_self, Not, ite_eq_right, zero_add
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.trunc_le_func line 589 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, LE.le, ENorm.enorm, MeasureTheory.trunc
Proof uses: id, dite, ite, OfNat.ofNat, Eq.mpr, Eq, congrFun', congrArg, ite_eq_left, of_eq_true, Not, ite_eq_right, Eq.trans, True, enorm_zero
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.truncCompl_le_func line 592 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, LE.le, ENorm.enorm, MeasureTheory.truncCompl
Proof uses: Eq.mpr, ite, LT.lt, OfNat.ofNat, id, Eq, congrArg, MeasureTheory.truncCompl_eq, dite, congrFun', ite_eq_left, of_eq_true, Not, ite_eq_right, Eq.trans, True, enorm_zero
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.foo line 596 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Ne, Top.top, LE.le, Eq, HAdd.hAdd
Proof uses: LT.lt, Or, le_or_gt, ENNReal.add_lt_add_of_le_of_lt, False.elim, Decidable.byContradiction, False, Not, ne_of_lt, le_antisymm, le_trans, le_of_eq, le_refl, ge_of_eq
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.truncCompl_anti line 602 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, ENNReal, LE.le, Ne, ENorm.enorm, MeasureTheory.trunc, Top.top, MeasureTheory.truncCompl
Proof uses: Eq, HAdd.hAdd, of_eq_true, Eq.trans, True, congr, congrArg, MeasureTheory.trunc_buildup_enorm, eq_self, MeasureTheory.foo, MeasureTheory.trunc_mono
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_truncCompl_anti The norm of the complement of the truncation is antitone in the truncation parameter line 610 source
Source documentation
The norm of the complement of the truncation is antitone in the truncation parameter

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, MeasureTheory.eLpNorm, OfNat.ofNat, Top.top, MeasureTheory.AEStronglyMeasurable, Antitone, MeasureTheory.truncCompl
Proof uses: LE.le, Filter.Eventually, ENorm.enorm, MeasureTheory.ae, Eq.mpr, Eq, Set, Set.ofPred, Not, id, congrFun', congrArg, funext, MeasureTheory.measure_eq_top_of_lintegral_ne_top, MeasureTheory.AEStronglyMeasurable.enorm, Eq.mp, MeasureTheory.lintegral, MeasureTheory.eLpNorm_one_eq_lintegral_enorm, MeasureTheory.trunc, Filter.Eventually.mono and 13 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_truncCompl_anti (hf : eLpNorm f 1 μ ≠ ⊤) (mf : AEStronglyMeasurable f μ) :
    Antitone (fun s ↦ eLpNorm (truncCompl f s) p μ) := by
…
```
Mentions: mf, s, MeasureTheory.truncCompl
lemma MeasureTheory.eLpNorm_trunc_measurable The norm of the truncation is meaurable in the truncation parameter line 624 source
Source documentation
The norm of the truncation is meaurable in the truncation parameter

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Measurable, MeasureTheory.eLpNorm, MeasureTheory.trunc
Proof uses: Monotone.measurable, MeasureTheory.eLpNorm_trunc_mono
20 instances, coercions and auxiliary constants left out.
```
lemma eLpNorm_trunc_measurable :
    Measurable (fun s ↦ eLpNorm (trunc f s) p μ) :=
…
```
Mentions: s, MeasureTheory.trunc
lemma MeasureTheory.eLpNorm_truncCompl_measurable The norm of the complement of the truncation is measurable in the truncation parameter line 630 source
Source documentation
The norm of the complement of the truncation is measurable in the truncation parameter

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, MeasureTheory.eLpNorm, OfNat.ofNat, Top.top, MeasureTheory.AEStronglyMeasurable, Measurable, MeasureTheory.truncCompl
Proof uses: Antitone.measurable, MeasureTheory.eLpNorm_truncCompl_anti
26 instances, coercions and auxiliary constants left out.
```
lemma eLpNorm_truncCompl_measurable (hf : eLpNorm f 1 μ ≠ ⊤) (mf : AEStronglyMeasurable f μ) :
    Measurable (fun s ↦ eLpNorm (truncCompl f s) p μ) :=
…
```
Mentions: mf, s, MeasureTheory.truncCompl
lemma MeasureTheory.trnc_le_func line 634 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, Bool, ENNReal, LE.le, ENorm.enorm, MeasureTheory.trnc
Proof uses: id, MeasureTheory.trnc.match_1, Unit, MeasureTheory.truncCompl, MeasureTheory.trunc, ite, OfNat.ofNat, Bool.false, dite, Eq.mpr, Eq, congrFun', congrArg, ite_eq_left, of_eq_true, Eq.trans, True, enorm_zero, Not, ite_eq_right and 1 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.MemLp.trunc line 655 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.MemLp, MeasureTheory.trunc
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLpNorm, Top.top, MeasureTheory.AEStronglyMeasurable.trunc, And.left, lt_of_le_of_lt, MeasureTheory.eLpNorm_mono_enorm_ae, MeasureTheory.ae_of_all, LE.le, ENorm.enorm, id, dite, ite, OfNat.ofNat, Eq.mpr, Eq, congrFun', congrArg and 8 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.MemLp.truncCompl line 665 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, MeasureTheory.MemLp, MeasureTheory.truncCompl
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLpNorm, Top.top, MeasureTheory.AEStronglyMeasurable.truncCompl, And.left, lt_of_le_of_lt, MeasureTheory.eLpNorm_mono_enorm_ae, MeasureTheory.ae_of_all, LE.le, ENorm.enorm, id, dite, ite, OfNat.ofNat, Eq.mpr, Eq, congrFun', congrArg and 8 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.eLpNorm_truncCompl_le line 672 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, Not, Eq, OfNat.ofNat, Ne, Top.top, LE.le, HPow.hPow, Real, MeasureTheory.eLpNorm, MeasureTheory.truncCompl, ENNReal.toReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.ofPred, LT.lt and 1 more
Proof uses: id, ite, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', ENNReal.toReal_pos, Eq.mpr, HDiv.hDiv, congrFun', congrArg, Eq.trans, ite_congr, Eq.refl, ite_eq_right, Trans.trans, Inv.inv, one_div, ENNReal.rpow_inv_rpow, LT.lt.ne', Eq.symm, MeasureTheory.setLIntegral_eq_of_support_subset and 26 more
56 instances, coercions and auxiliary constants left out.

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

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, LT.lt, LE.le, HPow.hPow, Real, MeasureTheory.eLpNorm, MeasureTheory.truncCompl, ENNReal.toReal, HMul.hMul and 1 more
Proof uses: ne_top_of_le_ne_top, And.right, LT.lt.ne', LT.lt.trans_le, And.left, le_trans, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.ofPred, ENorm.enorm, MeasureTheory.eLpNorm_truncCompl_le, Trans.trans, Eq, Eq.mpr, id, congrArg, Eq.symm, MeasureTheory.lintegral_const_mul', dite, of_eq_true and 44 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma estimate_eLpNorm_truncCompl {p q : ℝ≥0∞}
    (p_ne_top : p ≠ ⊤) (hpq : q ∈ Ioc 0 p) (hf : AEStronglyMeasurable f μ) (ht : 0 < t) :
    eLpNorm (truncCompl f t) q μ ^ q.toReal ≤
    (t ^ (q.toReal - p.toReal)) * eLpNorm f p μ ^ p.toReal := by
…
```
Mentions: MeasureTheory.truncCompl
lemma MeasureTheory.estimate_eLpNorm_trunc TODO: better name! line 723 source
Source comment
TODO: better name!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ENNReal, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, LE.le, HPow.hPow, Real, MeasureTheory.eLpNorm, MeasureTheory.trunc, ENNReal.toReal, HMul.hMul, HSub.hSub
Proof uses: LT.lt, LT.lt.trans_le, And.left, And.right, LT.lt.ne, LE.le.trans_lt, Iff.mpr, lt_top_iff_ne_top, dite, Eq, Filter.EventuallyEq, MeasureTheory.ae, ENorm.enorm, Eq.mpr, id, congrArg, Eq.symm, propext, MeasureTheory.eLpNorm_eq_zero_iff, Continuous.comp_aestronglyMeasurable and 88 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 76 steps
Open to load the checked before-and-after goal states.
```
lemma estimate_eLpNorm_trunc {p q : ℝ≥0∞}
    (hq : q ≠ ⊤) (hpq : p ∈ Ioc 0 q) {f : α → ε} (hf : AEStronglyMeasurable f μ) :
    eLpNorm (trunc f t) q μ ^ q.toReal ≤
    (t ^ (q.toReal - p.toReal)) * eLpNorm f p μ ^ p.toReal := by
…
```
Mentions: MeasureTheory.trunc
lemma MeasureTheory.trunc_Lp_Lq_higher If f is in Lp, the truncation is element of Lq for q ≥ p line 790 source
Source documentation
If f is in Lp, the truncation is element of Lq for q ≥ p.

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, MeasureTheory.MemLp, Ne, Top.top, MeasureTheory.trnc, Bool
Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLpNorm, MeasureTheory.aestronglyMeasurable_trnc, And.left, Eq, Or, eq_or_ne, Eq.mpr, id, congrArg, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm_exponent_top, Trans.trans, LE.le, MeasureTheory.trunc, Max.max, rfl, MeasureTheory.trunc_eLpNormEssSup_le and 25 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma trunc_Lp_Lq_higher (hpq : p ∈ Ioc 0 q) {f : α → ε} (hf : MemLp f p μ) (ht : t ≠ ∞) :
    MemLp (trnc ⊤ f t) q μ := by
…
```
Mentions: MeasureTheory.trnc
lemma MeasureTheory.memLp_truncCompl_of_memLp_top line 813 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, MeasureTheory.MemLp, Top.top, LT.lt, Set, Set.ofPred, ENorm.enorm, MeasureTheory.trnc, Bot.bot, Bool
Proof uses: dite, Eq, Eq.mpr, id, congrArg, MeasureTheory.MemLp.truncCompl, Not, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm, OfNat.ofNat, propext, MeasureTheory.memLp_zero_iff_aestronglyMeasurable, MeasureTheory.aestronglyMeasurable_trnc, And, MeasureTheory.StronglyMeasurable, Filter.EventuallyEq, MeasureTheory.ae, Real, ENNReal.toReal, ENNReal.toReal_pos and 70 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 60 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.truncCompl_Lp_Lq_lower If f is in Lp, the complement of the truncation is in Lq for q ≤ p line 873 source
Source documentation
If f is in Lp, the complement of the truncation is in Lq for q ≤ p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Ne, Top.top, Membership.mem, Set, Set.Ioc, OfNat.ofNat, LT.lt, MeasureTheory.MemLp, MeasureTheory.trnc, Bot.bot, Bool
Proof uses: ne_top_of_le_ne_top, And.right, LE.le, dite, Eq, of_eq_true, Eq.trans, True, congrFun', autoParam, congrArg, MeasureTheory.truncCompl, MeasureTheory.truncCompl_top, Not, And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm, MeasureTheory.aestronglyMeasurable_trnc, And.left, Real and 16 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma truncCompl_Lp_Lq_lower
    (hp : p ≠ ⊤) (hpq : q ∈ Ioc 0 p) (ht : 0 < t) (hf : MemLp f p μ) :
    MemLp (trnc ⊥ f t) q μ := by
…
```
Mentions: MeasureTheory.trnc
lemma MeasureTheory.memLp_of_memLp_le_of_memLp_ge Lemma 6.10 in Folland XXX: is the ContinuousAdd hypothesis really necessary for MemLp.add (and hence here)? line 891 source
Source comment
Lemma 6.10 in Folland XXX: is the `ContinuousAdd` hypothesis really necessary for `MemLp.add` (and hence here)?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, ContinuousAdd, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Icc, MeasureTheory.MemLp
Proof uses: dite, Eq, Top.top, Eq.mpr, eq_of_heq, ENorm, autoParam, HEq, Eq.refl, HEq.refl, Eq.symm, LE.le, id, congrArg, propext, eq_top_iff, LE, And.left, Eq.mp, Not and 34 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma memLp_of_memLp_le_of_memLp_ge {f : α → ε} [ContinuousAdd ε]
    {r : ℝ≥0∞} (hp : 0 < p) (hr' : q ∈ Icc p r)
    (hf : MemLp f p μ) (hf' : MemLp f r μ) : MemLp f q μ := by
…
```
def MeasureTheory.res line 929 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, Set, Real
Proof uses: ite, Eq, Top.top, Bool.true, Set.Ioi, OfNat.ofNat, EmptyCollection.emptyCollection, Set.Ioo, ENNReal.toReal
8 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.measurableSet_res line 933 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, MeasurableSet, Real, MeasureTheory.res
Proof uses: id, dite, ite, Set, Eq, Top.top, Bool.true, Set.Ioi, OfNat.ofNat, EmptyCollection.emptyCollection, Set.Ioo, ENNReal.toReal, Eq.mpr, congrArg, ite_eq_left, measurableSet_Ioi, Not, ite_eq_right, MeasurableSet.empty, measurableSet_Ioo
27 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.res_subset_Ioi line 941 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, LE.le, Set, Real, MeasureTheory.res, Set.Ioi, OfNat.ofNat
Proof uses: id, dite, ite, Eq, Top.top, Bool.true, EmptyCollection.emptyCollection, Set.Ioo, ENNReal.toReal, Eq.mpr, congrFun', congrArg, ite_eq_left, Membership.mem, Not, ite_eq_right, of_eq_true, Set.ofPred, LT.lt, propext and 4 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
instance MeasureTheory.decidableMemRes line 952 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Bool, ENNReal, Decidable, Membership.mem, Set, MeasureTheory.res
Proof uses: Classical.propDecidable
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.res' line 955 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, Set, Real
Proof uses: ite, Eq, Top.top, Bool.true, Set.Ioi, OfNat.ofNat, EmptyCollection.emptyCollection, Set.Ioc, ENNReal.toReal, Inter.inter, Set.Ici
9 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.res'comp₀ TODO: this one is probably obsolete line 960 source
Source comment
TODO: this one is probably obsolete

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, LT.lt, OfNat.ofNat, Eq, Set, Real, SDiff.sdiff, Set.Ioi, MeasureTheory.res', MeasureTheory.res, Decidable.decide, Not, Bool.true
Proof uses: id, ite, Top.top, EmptyCollection.emptyCollection, Set.Ioc, ENNReal.toReal, Inter.inter, Set.Ici, dite, Set.Ioo, Eq.mpr, congr, congrArg, ite_eq_left, congrFun', False.elim, Eq.mp, False, Eq.trans, Bool.false and 29 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma res'comp₀ (j : Bool) (β : ℝ≥0∞) (hβ : 0 < β) :
    Ioi (0 : ℝ) \ res' j β = res (¬j) β := by
…
```
Mentions: MeasureTheory.res', MeasureTheory.res
lemma MeasureTheory.res'comp line 970 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, Eq, Set, Real, SDiff.sdiff, Set.Ioi, OfNat.ofNat, MeasureTheory.res', MeasureTheory.res, Decidable.decide, Not, Bool.true
Proof uses: id, ite, Top.top, EmptyCollection.emptyCollection, Set.Ioc, ENNReal.toReal, Inter.inter, Set.Ici, dite, Set.Ioo, Eq.mpr, congr, congrArg, ite_eq_left, congrFun', False.elim, Eq.mp, False, Eq.trans, Bool.false and 34 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measurableSet_res' line 982 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, MeasurableSet, Real, MeasureTheory.res'
Proof uses: id, Eq, Top.top, Decidable, ite, Set, Bool.true, Set.Ioi, OfNat.ofNat, EmptyCollection.emptyCollection, Set.Ioc, ENNReal.toReal, Inter.inter, Set.Ici, Not, Eq.mpr, congrArg, ite_eq_right, of_eq_true, ite_eq_left
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.res'subset_Ioi line 986 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, LE.le, Set, Real, MeasureTheory.res', Set.Ioi, OfNat.ofNat
Proof uses: id, dite, ite, Eq, Top.top, Bool.true, EmptyCollection.emptyCollection, Set.Ioc, ENNReal.toReal, Inter.inter, Set.Ici, Eq.mpr, congrFun', congrArg, ite_eq_left, of_eq_true, Not, ite_eq_right, Set.Ioc_subset_Ioi_self, Set.inter_subset_left
23 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.res'subset_Ici line 994 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, LE.le, Set, Real, MeasureTheory.res', Set.Ici, OfNat.ofNat
Proof uses: id, dite, ite, Eq, Top.top, Bool.true, Set.Ioi, EmptyCollection.emptyCollection, Set.Ioc, ENNReal.toReal, Inter.inter, Eq.mpr, congrFun', congrArg, ite_eq_left, of_eq_true, Eq.trans, True, Not, ite_eq_right and 6 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_trunc_mul₀ line 1002 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, Real, ENNReal, Bool, ToneCouple, LT.lt, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HMul.hMul, HPow.hPow, ENorm.enorm, MeasureTheory.trnc, ToneCouple.ton, ENNReal.ofReal, MeasureTheory.res' and 3 more
Proof uses: Eq.mpr, Inter.inter, Set, id, congrArg, MeasureTheory.lintegral_double_restrict_set, measurableSet_Ioi, MeasureTheory.measurableSet_res', Filter.univ_mem', MeasureTheory.ae, MeasureTheory.Measure, Set.ofPred, Membership.mem, SDiff.sdiff, LE.le, MeasureTheory.res, Decidable.decide, Not, Bool.true, MeasureTheory.res'comp and 64 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 72 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_trunc_mul₁ line 1054 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, Real, ENNReal, Bool, ToneCouple, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, MeasureTheory.res', Bool.xor, ToneCouple.mon, ToneCouple.inv, ENorm.enorm, HMul.hMul, HPow.hPow, MeasureTheory.trnc, ToneCouple.ton, ENNReal.ofReal and 1 more
Proof uses: MeasureTheory.setLIntegral_congr, id, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, ite, Set, Top.top, Bool.true, Set.Ioi, OfNat.ofNat, EmptyCollection.emptyCollection, Set.Ioo, ENNReal.toReal, dite, Set.Ioc, Inter.inter, Set.Ici, Eq.mpr, congr and 20 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_trunc_mul₂ line 1069 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, Real, ENNReal, Bool, ToneCouple, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, MeasureTheory.res, Bool.xor, ToneCouple.mon, ToneCouple.inv, ENorm.enorm, HMul.hMul, HPow.hPow, MeasureTheory.trnc, ToneCouple.ton, ENNReal.ofReal
Proof uses: MeasureTheory.setLIntegral_congr_fun, MeasureTheory.measurableSet_res, id, Set.EqOn, ite, Set, Top.top, Bool.true, Set.Ioi, OfNat.ofNat, EmptyCollection.emptyCollection, Set.Ioo, ENNReal.toReal, MeasureTheory.trnc.match_1, Unit, MeasureTheory.truncCompl, MeasureTheory.trunc, LE.le, And, Iff and 47 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_trunc_mul line 1113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ESeminormedAddMonoid, Real, ENNReal, AEMeasurable, MeasureTheory.MeasureSpace.volume, Bool, ToneCouple, LT.lt, OfNat.ofNat, Eq, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.Ioi, HMul.hMul, HPow.hPow, ENorm.enorm, MeasureTheory.trnc, ToneCouple.ton, ENNReal.ofReal and 4 more
Proof uses: Eq.mpr, MeasureTheory.res', id, congrArg, MeasureTheory.lintegral_trunc_mul₀, MeasureTheory.lintegral_trunc_mul₁, MeasureTheory.lintegral_trunc_mul₂, MeasureTheory.lintegral_mul_const'', AEMeasurable.restrict, Eq.refl
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_rpow_of_gt_abs line 1123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, GT.gt, Neg.neg, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioo, ENNReal.ofReal, HPow.hPow, HDiv.hDiv, HAdd.hAdd, abs
Proof uses: LT.lt, lt_of_not_ge, 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, HMul.hMul, 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 and 33 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.lintegral_Ioi_rpow_of_lt_abs TODO: treat symmetrically to Ioo case? line 1131 source
Source comment
TODO: treat symmetrically to Ioo case?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Neg.neg, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, ENNReal.ofReal, HPow.hPow, HDiv.hDiv, HAdd.hAdd, abs
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, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, HMul.hMul, Nat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 50 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_Ioi_rpow_of_lt_abs {β σ : ℝ} (hβ : 0 < β) (hσ : σ < -1) :
    ∫⁻ s : ℝ in Ioi β, ENNReal.ofReal (s ^ σ) =
    ENNReal.ofReal (β ^ (σ + 1) / |σ + 1|) := by
…
```
Mentions: s
lemma MeasureTheory.lintegral_rpow_Ioi_top line 1141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, OfNat.ofNat, ENNReal.ofReal, HPow.hPow, Top.top
Proof uses: Decidable.byContradiction, Not, not_integrableOn_Ioi_rpow, And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.HasFiniteIntegral, Measurable.aestronglyMeasurable, Measurable.pow_const, measurable_id', Trans.trans, LT.lt, ENorm.enorm, MeasureTheory.lintegral_congr_ae, Filter.mp_mem, MeasureTheory.ae, MeasureTheory.Measure, Set.ofPred, MeasureTheory.self_mem_ae_restrict, measurableSet_Ioi, Filter.univ_mem' and 8 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.value_lintegral_res₀ line 1153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Bool, ENNReal, Real, ite, Eq, Bool.true, GT.gt, Neg.neg, OfNat.ofNat, LT.lt, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, MeasureTheory.res, ENNReal.ofReal, HPow.hPow, HDiv.hDiv, HAdd.hAdd, abs
Proof uses: id, Decidable, Set, Top.top, Set.Ioi, EmptyCollection.emptyCollection, Set.Ioo, ENNReal.toReal, Not, Eq.mpr, congrFun', congrArg, MeasureTheory.Measure, ite_congr, Eq.refl, ite_eq_right_of_eq_false, Eq.trans, Bool.false, False, Bool.eq_false_of_ne_true and 88 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.value_lintegral_res₁ line 1183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, ScaledPowerFunction, LT.lt, OfNat.ofNat, Ne, Top.top, Eq, HMul.hMul, HDiv.hDiv, HPow.hPow, ToneCouple.inv, StrictRangeToneCouple.toToneCouple, spf_to_tc, HAdd.hAdd, ENNReal.ofReal, abs, ScaledPowerFunction.d, Inv.inv, ScaledPowerFunction.σ
Proof uses: ScaledPowerFunction.hd, id, StrictRangeToneCouple.mk, ToneCouple.mk, ite, Bool, Bool.true, Bool.false, Eq.mpr, congrArg, Eq.symm, ENNReal.mul_div_right_comm, ENNReal.mul_rpow_of_ne_zero, ne_of_gt, LT.lt.ne', ENNReal.rpow_pos, mul_assoc, ENNReal.rpow_mul, ENNReal.rpow_add, Eq.refl
60 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.value_lintegral_res₂ line 1196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, Real, ScaledPowerFunction, LT.lt, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Inv.inv, ScaledPowerFunction.σ, LE.le, HDiv.hDiv, HPow.hPow, ToneCouple.inv, StrictRangeToneCouple.toToneCouple, spf_to_tc, ENNReal.ofReal, abs, ScaledPowerFunction.d
Proof uses: dite, Eq, Top.top, ScaledPowerFunction.hd, id, StrictRangeToneCouple.mk, ToneCouple.mk, ite, Bool, Bool.true, Bool.false, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', ENNReal.top_rpow_of_pos, ENNReal.mul_top, LT.lt.ne' and 8 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.AEStronglyMeasurable.induction TODO: move to a lower-level file! line 1208 source
Source comment
TODO: move to a lower-level file!

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, MeasureTheory.Measure, MeasureTheory.StronglyMeasurable, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.AEStronglyMeasurable
Proof uses: And, Exists.choose, Exists.choose_spec, And.left, Eq.mp, congrArg, Eq, rfl, Filter.EventuallyEq.symm, And.right
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma AEStronglyMeasurable.induction {α : Type*} {β : Type*} {mα : MeasurableSpace α} [TopologicalSpace β]
  {μ : Measure α} {motive : (α → β) → Prop}
  (ae_eq_implies : ∀ ⦃f g : α → β⦄ (_ : StronglyMeasurable f) (_ : f =ᶠ[ae μ] g), motive f → motive g)
  (measurable : ∀ ⦃f : α → β⦄ (_ : StronglyMeasurable f), motive f)
    ⦃f : α → β⦄ (hf : AEStronglyMeasurable f μ) : motive f := by
…
```
Mentions: g