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

49 declarations, 0 contain sorry, 0 declared as axioms

The distribution function `d_f`

Imports (1)

Carleson.ToMathlib.Misc

Imported by 3 files

def MeasureTheory.superlevelSet The superlevel set of a function f line 32 source
Source documentation
The superlevel set of a function f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, ENNReal, Set
Proof uses: Set.ofPred, LT.lt, ENorm.enorm
3 instances, coercions and auxiliary constants left out.
```
def superlevelSet (f : α → ε) (t : ℝ≥0∞) : Set α := {x | t < ‖f x‖ₑ}
```
lemma MeasureTheory.superlevelSet_antitone line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, Antitone, ENNReal, Set, MeasureTheory.superlevelSet
Proof uses: LE.le, id, Membership.mem, Set.ofPred, LT.lt, ENorm.enorm, lt_of_le_of_lt
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.superlevelSet_zero_eq_support line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, ENormedAddCommMonoid, Eq, Set, MeasureTheory.superlevelSet, OfNat.ofNat, ENNReal, Function.support
Proof uses: id, Set.ofPred, LT.lt, ENorm.enorm, of_eq_true, Not, Eq.trans, True, congrFun', congrArg, funext, Ne, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.nullMeasurableSet_superlevelSet line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ContinuousENorm, MeasureTheory.AEStronglyMeasurable, MeasureTheory.NullMeasurableSet, MeasureTheory.superlevelSet
Proof uses: id, MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_lt, ENorm.enorm, MeasureTheory.aestronglyMeasurable_const, AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.enorm
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.measurableSet_superlevelSet line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENNReal, TopologicalSpace, ContinuousENorm, OpensMeasurableSpace, Measurable, MeasurableSet, MeasureTheory.superlevelSet
Proof uses: id, Eq.mpr, Set.ofPred, LT.lt, ENorm.enorm, Eq, Measurable.fun_comp, Prod, Prod.fst, Prod.snd, Prod.mk, measurable_lt, Measurable.prodMk, measurable_const, measurable_enorm
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.superlevelSet_const line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENNReal, ENorm, Eq, Set, MeasureTheory.superlevelSet, Function.const, ite, LT.lt, ENorm.enorm, Set.univ, EmptyCollection.emptyCollection
Proof uses: id, dite, Set.ofPred, Eq.mpr, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, congrFun', funext, eq_true, eq_self, Not, ite_eq_right, False, eq_false
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.distribution The distribution function of a function f line 68 source
Source documentation
The distribution function of a function f. Todo: rename to something more Mathlib-appropriate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, ENNReal, MeasureTheory.Measure
Proof uses: Set, Set.ofPred, LT.lt, ENorm.enorm
5 instances, coercions and auxiliary constants left out.
```
def distribution (f : α → ε) (t : ℝ≥0∞) (μ : Measure α) : ℝ≥0∞ :=
…
```
lemma MeasureTheory.distribution_eq_measure_superlevelSet line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENorm, Eq, MeasureTheory.distribution, Set, MeasureTheory.superlevelSet
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 MeasureTheory.distibution_top line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ENorm, MeasureTheory.Measure, Eq, ENNReal, MeasureTheory.distribution, Top.top, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set, Set.ofPred, LT.lt, ENorm.enorm, EmptyCollection.emptyCollection, False, funext, MeasureTheory.measure_empty, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_mono_right line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENorm, LE.le, MeasureTheory.distribution
Proof uses: MeasureTheory.measure_mono, Set.ofPred, LT.lt, ENorm.enorm, Membership.mem, Set, lt_of_le_of_lt
8 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.distribution_mono_right' line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Antitone, ENNReal, MeasureTheory.distribution
Proof uses: LE.le, MeasureTheory.distribution_mono_right
5 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.distribution_congr_ae line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENorm, Filter.Eventually, Eq, MeasureTheory.ae, MeasureTheory.distribution
Proof uses: MeasureTheory.measure_congr, Set.ofPred, LT.lt, ENorm.enorm, Filter.mp_mem, Filter.univ_mem', Membership.mem, Set, id, rfl, Eq.mpr, congrArg, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_measurable₀ line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Measurable, ENNReal, MeasureTheory.distribution
Proof uses: Antitone.measurable, MeasureTheory.distribution_mono_right'
8 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.distribution_measurable line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, ENNReal, Measurable, MeasureTheory.distribution
Proof uses: Measurable.fun_comp, MeasureTheory.distribution_measurable₀
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_toReal_le line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, LE.le, MeasureTheory.distribution, Real, Function.comp, ENNReal.toReal
Proof uses: id, MeasureTheory.measure_mono, Set.ofPred, LT.lt, ENorm.enorm, Set.ofPred_subset_ofPred_of_imp, lt_imp_lt_of_le_of_le, le_refl, of_eq_true
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_toReal_eq line 107 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.distribution, Real, Function.comp, ENNReal.toReal
Proof uses: MeasureTheory.measure_congr, Set.ofPred, LT.lt, ENorm.enorm, Filter.Eventually.set_eq, Filter.mp_mem, Iff, Membership.mem, Set, Filter.univ_mem', id, of_eq_true, Eq.trans, True, congrFun', congrArg, Real.enorm_toReal, Not, False, eq_false and 2 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_add_le_of_enorm line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENorm, Filter.Eventually, LE.le, ENorm.enorm, HMul.hMul, HAdd.hAdd, MeasureTheory.ae, MeasureTheory.distribution
Proof uses: id, Eq, Set, SDiff.sdiff, Set.ofPred, LT.lt, Union.union, OfNat.ofNat, MeasureTheory.measure_mono_null, Compl.compl, Eq.mpr, Membership.mem, Eq.trans, And, implies_congr, Not, congrArg, Or, congr, Eq.refl and 7 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.approx_above_superset line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, ENNReal, Eq, Set, Set.iUnion, Nat, Set.ofPred, LT.lt, HAdd.hAdd, Inv.inv, ENorm.enorm
Proof uses: Set.ext, Iff.intro, Membership.mem, Exists, Iff.mp, And, exists_exists_eq_and, Trans.trans, LE.le, le_self_add, Filter, nhds, OfNat.ofNat, Set.Iio, HSub.hSub, Iio_mem_nhds, tsub_pos_of_lt, Filter.map, Filter.atTop, ENNReal.tendsto_inv_nat_nhds_zero and 13 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.tendsto_measure_iUnion_distribution line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, ENNReal, Filter.Tendsto, Nat, Function.comp, Set, Set.ofPred, LT.lt, HAdd.hAdd, Inv.inv, ENorm.enorm, Filter.atTop, nhds
Proof uses: Eq.mpr, Set.iUnion, id, Eq, congrArg, Eq.symm, MeasureTheory.approx_above_superset, MeasureTheory.tendsto_measure_iUnion_atTop, LE.le, Membership.mem, Trans.trans, add_le_add, le_refl, ENNReal.inv_le_inv', Nat.mono_cast
55 instances, coercions and auxiliary constants left out.

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

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, ENNReal, LT.lt, MeasureTheory.distribution, Exists, Nat, HAdd.hAdd, Inv.inv
Proof uses: Membership.mem, Set, Filter, Filter.map, Function.comp, Set.ofPred, ENorm.enorm, Filter.atTop, Set.Ioi, MeasureTheory.tendsto_measure_iUnion_distribution, Ioi_mem_nhds, LE.le, Eq.mp, Eq.trans, Set.preimage, congrArg, funext, forall_congr, implies_congr, Eq.refl and 2 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma select_neighborhood_distribution (t₀ : ℝ≥0∞) (l : ℝ≥0∞)
    (hu : l < distribution f t₀ μ) :
    ∃ n : ℕ, l < distribution f (t₀ + (↑n)⁻¹) μ := by
…
```
Mentions: MeasureTheory.distribution
lemma MeasureTheory.continuousWithinAt_distribution line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, ENNReal, ContinuousWithinAt, MeasureTheory.distribution, Set.Ioi
Proof uses: Eq, Top.top, LT.lt, Or, eq_top_or_lt_top, continuousWithinAt_of_notMem_closure, of_eq_true, Not, Membership.mem, Set, closure, Eq.trans, False, True, congrArg, EmptyCollection.emptyCollection, congrFun', IsMax.Ioi_eq, IsMax, eq_self and 68 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_pow TODO: investigate generalising this to enorm classes This requires adding enorm versions of NormOneClass and NormMulClass line 212 source
Source comment
TODO: investigate generalising this to enorm classes This requires adding enorm versions of NormOneClass and NormMulClass

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, SeminormedRing, NormOneClass, NormMulClass, ENNReal, MeasureTheory.Measure, Nat, Ne, OfNat.ofNat, Eq, MeasureTheory.distribution, HPow.hPow
Proof uses: id, Set, Set.ofPred, LT.lt, ENorm.enorm, congrArg, Set.ext, Iff.intro, Membership.mem, lt_of_pow_lt_pow_left', LE.le, Eq.mp, enorm_pow, Set.mem_ofPred_eq, Eq.mpr, ENNReal.pow_right_strictMono
68 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma distribution_pow (ε : Type*) [SeminormedRing ε] [NormOneClass ε] [NormMulClass ε] (f : α → ε)
    (t : ℝ≥0∞) (μ : Measure α) {n : ℕ} (hn : n ≠ 0) :
    distribution (f ^ n) (t ^ n) μ = distribution f t μ := by
…
```
Mentions: MeasureTheory.distribution
lemma MeasureTheory.distribution_mono_left line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENorm, Filter.Eventually, LE.le, ENorm.enorm, MeasureTheory.ae, MeasureTheory.distribution
Proof uses: Set, SDiff.sdiff, Set.ofPred, LT.lt, Not, Eq.mpr, Membership.mem, And, id, Eq, implies_congr, Eq.refl, congrArg, LE.le.trans_lt, Trans.trans, Inter.inter, HAdd.hAdd, MeasureTheory.measure_le_inter_add_sdiff, OfNat.ofNat, MeasureTheory.measure_mono_null and 3 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_mono line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENorm, Filter.Eventually, LE.le, ENorm.enorm, MeasureTheory.ae, MeasureTheory.distribution
Proof uses: LE.le.trans, MeasureTheory.distribution_mono_left, MeasureTheory.distribution_mono_right
8 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.distribution_eLpNormEssSup line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, Eq, ENNReal, MeasureTheory.distribution, MeasureTheory.eLpNormEssSup, OfNat.ofNat
Proof uses: meas_essSup_lt, ENorm.enorm, Filter.isBounded_le_of_top, Filter.map, MeasureTheory.ae
19 instances, coercions and auxiliary constants left out.
lemma MeasureTheory.distribution_add_le line 245 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, LE.le, MeasureTheory.distribution, HAdd.hAdd
Proof uses: Trans.trans, Set, Union.union, Set.ofPred, LT.lt, ENorm.enorm, MeasureTheory.measure_mono, Membership.mem, Eq.mpr, Or, id, Eq, Mathlib.Tactic.Contrapose.contrapose₁, Not, And, implies_congr, Eq.trans, congr, congrArg, LE.le.trans and 5 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_eq_zero_of_ae_zero_enorm TODO: make this an iff? line 256 source
Source comment
TODO: make this an iff?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENorm, Filter.EventuallyEq, MeasureTheory.ae, Function.comp, ENorm.enorm, OfNat.ofNat, Eq, MeasureTheory.distribution
Proof uses: id, Eq.mpr, Set, Set.ofPred, LT.lt, LE.le, congrArg, Eq.symm, propext, nonpos_iff_eq_zero, Trans.trans, Ne, rfl, MeasureTheory.measure_mono, Membership.mem, pos_of_gt, eq_of_heq, HEq, DFunLike, HEq.refl and 9 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma distribution_eq_zero_of_ae_zero_enorm {f : α → ε} (h : enorm ∘ f =ᵐ[μ] 0) :
    distribution f t μ = 0 := by
…
```
Mentions: MeasureTheory.distribution
lemma MeasureTheory.distribution_eq_zero_of_ae_zero line 273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Filter.EventuallyEq, MeasureTheory.ae, OfNat.ofNat, Eq, MeasureTheory.distribution
Proof uses: MeasureTheory.distribution_eq_zero_of_ae_zero_enorm, Filter.mp_mem, Set.ofPred, Function.comp, ENorm.enorm, Filter.univ_mem', Membership.mem, Set, id, of_eq_true, Eq.trans, True, congrFun', congrArg, enorm_zero, eq_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_zero line 279 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ENormedAddMonoid, Eq, MeasureTheory.distribution, OfNat.ofNat
Proof uses: MeasureTheory.distribution_eq_zero_of_ae_zero, MeasureTheory.ae_eq_rfl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_zero_eq_measure_support line 283 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, Eq, ENNReal, MeasureTheory.distribution, OfNat.ofNat, Set, Function.support
Proof uses: id, Set.ofPred, LT.lt, ENorm.enorm, eq_of_heq, Ne, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Eq.rec, funext, propext, of_eq_true, Iff, Not, Eq.trans, True, congrFun' and 2 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_indicator_eq line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Set, Eq, MeasureTheory.distribution, Set.indicator, Inter.inter, MeasureTheory.superlevelSet
Proof uses: id, Set.ofPred, LT.lt, ENorm.enorm, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Set.ext, Iff, Membership.mem, Eq.mpr, ite, Classical.decPred, OfNat.ofNat, And, congrArg, dite and 16 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_indicator_le_measure Lemma 1.1.24 of [Ian Tice] line 301 source
Source comment
Lemma 1.1.24 of [Ian Tice]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Set, LE.le, MeasureTheory.distribution, Set.indicator
Proof uses: Eq.mpr, Inter.inter, MeasureTheory.superlevelSet, id, Eq, congrArg, MeasureTheory.distribution_indicator_eq, MeasureTheory.measure_mono, of_eq_true
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma distribution_indicator_le_measure {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε]
  {f : α → ε} {X : Set α} :
    distribution (X.indicator f) x μ ≤ μ X := by
…
```
Mentions: MeasureTheory.distribution
lemma MeasureTheory.distribution_indicator_const line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Set, Eq, MeasureTheory.distribution, Set.indicator, Function.const, Set.Iio, ENorm.enorm
Proof uses: Eq.mpr, Inter.inter, MeasureTheory.superlevelSet, id, congrArg, MeasureTheory.distribution_indicator_eq, ite, LT.lt, Set.univ, EmptyCollection.emptyCollection, MeasureTheory.superlevelSet_const, Membership.mem, Classical.decPred, OfNat.ofNat, ite_congr, Eq.refl, Not, dite, congr, ite_eq_left and 9 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.distribution_const line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Eq, MeasureTheory.distribution, Function.const, Set.indicator, Set.Iio, ENorm.enorm, Set, Set.univ
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Set.indicator_univ, MeasureTheory.distribution_indicator_const, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_indicator_superlevelSet line 319 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ENormedAddMonoid, Eq, MeasureTheory.distribution, Set.indicator, MeasureTheory.superlevelSet, Min.min
Proof uses: Eq.mpr, Set, Inter.inter, id, congrArg, MeasureTheory.distribution_indicator_eq, dite, LE.le, Iff.mpr, Set.inter_eq_right, MeasureTheory.superlevelSet_antitone, min_eq_right, MeasureTheory.distribution_mono_right, Eq.refl, Not, Set.inter_eq_left, LT.lt.le, Eq.mp, LT.lt, min_eq_left
29 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_indicator_superlevelSet_compl line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ENormedAddMonoid, MeasureTheory.AEStronglyMeasurable, Ne, MeasureTheory.distribution, Top.top, Eq, Set.indicator, Compl.compl, Set, MeasureTheory.superlevelSet, HSub.hSub
Proof uses: Eq.mpr, Inter.inter, id, congrArg, MeasureTheory.distribution_indicator_eq, dite, LE.le, OfNat.ofNat, tsub_eq_zero_of_le, MeasureTheory.distribution_mono_right, EmptyCollection.emptyCollection, Eq.symm, MeasureTheory.measure_empty, SDiff.sdiff, Set.sdiff_eq_compl_inter, Iff.mpr, Set.sdiff_eq_empty, MeasureTheory.superlevelSet_antitone, Eq.refl, Not and 5 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_eq_zero_iff line 344 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Iff, Eq, MeasureTheory.distribution, OfNat.ofNat, LE.le, MeasureTheory.eLpNormEssSup
Proof uses: Eq.mpr, Set, Set.ofPred, LT.lt, ENorm.enorm, id, congrArg, MeasureTheory.distribution.eq_1, essSup, MeasureTheory.eLpNormEssSup.eq_1, Compl.compl, Eq.symm, compl_compl, Membership.mem, Filter, MeasureTheory.ae, propext, MeasureTheory.mem_ae_iff, Not, Set.compl_def and 18 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.support_distribution line 357 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Eq, Set, ENNReal, Function.support, MeasureTheory.distribution, Set.Iio, MeasureTheory.eLpNormEssSup
Proof uses: Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, LT.lt, True, congr, congrArg, Ne, OfNat.ofNat, Not, LE.le, iff_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_add line 362 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Disjoint, Set, Function.support, MeasureTheory.AEStronglyMeasurable, Eq, MeasureTheory.distribution, HAdd.hAdd
Proof uses: id, Eq.mpr, Set.ofPred, LT.lt, ENorm.enorm, Union.union, congrArg, Eq.symm, MeasureTheory.measure_union₀, nullMeasurableSet_lt, aemeasurable_const, MeasureTheory.AEStronglyMeasurable.enorm, Disjoint.aedisjoint, Set.disjoint_of_subset, Membership.mem, Not, OfNat.ofNat, implies_congr, Ne, Eq.refl and 29 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_const_smul line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Or, Ne, OfNat.ofNat, Top.top, Eq, MeasureTheory.distribution, HSMul.hSMul, HDiv.hDiv
Proof uses: id, eq_of_heq, Set, Set.ofPred, LT.lt, ENorm.enorm, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Eq.rec, funext, propext, Iff, Eq.mpr, HMul.hMul, congrArg, mul_comm, Iff.symm and 1 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_mul line 401 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Or, Ne, Top.top, OfNat.ofNat, Eq, MeasureTheory.distribution, HMul.hMul, HDiv.hDiv
Proof uses: Inv.inv, Eq.mpr, id, congrArg, ENNReal.div_eq_inv_mul, inv_inv, Eq.refl, HSMul.hSMul, Eq.symm, MeasureTheory.distribution_const_smul, Not, congrFun', ENorm, Eq.rec, funext, of_eq_true, Eq.trans, True, eq_self
32 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_indicator_add_of_support_subset line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, TopologicalSpace, ESeminormedAddMonoid, Eq, ENorm.enorm, HAdd.hAdd, Ne, Top.top, Set, LE.le, Function.support, MeasureTheory.distribution, Set.indicator, Function.const, ite, LT.lt, HSub.hSub
Proof uses: id, dite, Set.ofPred, Eq.mpr, congrArg, ite_eq_left, eq_of_heq, HEq, DFunLike, HEq.refl, Eq.refl, heq_of_eq, Set.ext, Iff, Membership.mem, Iff.intro, Mathlib.Tactic.Contrapose.contrapose₁, Not, implies_congr, of_eq_true and 28 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_indicator_add_of_support_subset_ennreal ENNReal version of the previous lemma line 450 source
Source comment
ENNReal version of the previous lemma

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Ne, Top.top, Set, LE.le, Function.support, Eq, MeasureTheory.distribution, HAdd.hAdd, Set.indicator, Function.const, ite, LT.lt, HSub.hSub
Proof uses: Eq.mpr, ENorm.enorm, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, ite_congr, LT, Not, ENorm, outParam, HSub, MeasureTheory.distribution_indicator_add_of_support_subset, of_eq_true, Eq.trans, True, forall_congr, eq_self, implies_true and 1 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma distribution_indicator_add_of_support_subset_ennreal {f : α → ℝ≥0∞} {c : ℝ≥0∞} (hc : c ≠ ⊤)
  {s : Set α} (hfs : Function.support f ⊆ s) :
    distribution (f + s.indicator (Function.const α c)) t μ
      = if t < c then μ s else distribution f (t - c) μ := by
…
```
Mentions: c, s, MeasureTheory.distribution
lemma MeasureTheory.distribution_indicator_add_of_support_subset_nnreal NNReal version of the previous lemma line 457 source
Source comment
NNReal version of the previous lemma

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, NNReal, Set, LE.le, Function.support, Eq, MeasureTheory.distribution, HAdd.hAdd, Set.indicator, Function.const, ite, LT.lt, HSub.hSub
Proof uses: Eq.mpr, ENorm.enorm, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, ite_congr, LT, Not, ENorm, outParam, HSub, MeasureTheory.distribution_indicator_add_of_support_subset, of_eq_true, Eq.trans, True, forall_congr, congr, congrArg and 8 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma distribution_indicator_add_of_support_subset_nnreal {f : α → ℝ≥0} {c : ℝ≥0}
  {s : Set α} (hfs : Function.support f ⊆ s) :
    distribution (f + s.indicator (Function.const α c)) t μ
      = if t < c then μ s else distribution f (t - c) μ := by
…
```
Mentions: c, s, MeasureTheory.distribution
lemma MeasureTheory.distribution_eq_distribution_prod line 463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENorm, ENNReal, MeasureTheory.IsProbabilityMeasure, Eq, MeasureTheory.distribution, Prod, Prod.fst, MeasureTheory.Measure.prod
Proof uses: id, Set, Set.ofPred, LT.lt, ENorm.enorm, SProd.sprod, Set.univ, Set.ext, Iff, Membership.mem, Eq.mpr, Prod.mk, And, Prod.snd, congrArg, propext, Set.mem_prod, of_eq_true, Eq.trans, True and 8 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_le_mul_pow_eLpNorm_enorm line 474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, ENNReal, Ne, OfNat.ofNat, Top.top, MeasureTheory.AEStronglyMeasurable, Eq, Set, Set.ofPred, ENorm.enorm, LE.le, MeasureTheory.distribution, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal and 1 more
Proof uses: LE.le.trans', MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm, id, MeasureTheory.measure_mono, LT.lt, Set.ofPred_subset_ofPred_of_imp
36 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def MeasureTheory.C_distribution_le_of_eLpNorm_le The constant used in C_distribution_le_of_eLpNorm_le line 485 source
Source documentation
The constant used in C_distribution_le_of_eLpNorm_le.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal
Proof uses: HMul.hMul, HPow.hPow, Real, Inv.inv
8 instances, coercions and auxiliary constants left out.
```
def C_distribution_le_of_eLpNorm_le (δ ε p : NNReal) : NNReal := δ * ε ^ p.toReal⁻¹
```
lemma MeasureTheory.C_distribution_le_of_eLpNorm_le_pos line 487 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, LT.lt, OfNat.ofNat, MeasureTheory.C_distribution_le_of_eLpNorm_le
Proof uses: mul_pos, HPow.hPow, Real, Inv.inv, NNReal.rpow_pos
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.distribution_le_of_eLpNorm_le line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ContinuousENorm, NNReal, LT.lt, OfNat.ofNat, MeasureTheory.AEStronglyMeasurable, LE.le, ENNReal, MeasureTheory.eLpNorm, MeasureTheory.C_distribution_le_of_eLpNorm_le, MeasureTheory.distribution
Proof uses: LE.le.trans, HMul.hMul, HPow.hPow, Real, Inv.inv, ENNReal.toReal, MeasureTheory.distribution_le_mul_pow_eLpNorm_enorm, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, eq_false, LT.lt.ne', not_false_eq_true, Top.top, Set, Set.ofPred and 19 more
83 instances, coercions and auxiliary constants left out.

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

Carleson/ToMathlib/Distribution.lean

The distribution function d_f

`Carleson/ToMathlib/Distribution.lean`

The distribution function `d_f`