Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

GitHub source file

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

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

14 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 5 files
  1. lemma MeasureTheory.eLpNorm_zero_of_ae_zero' line 22 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Filter.EventuallyEq, MeasureTheory.ae, Function.comp, ENorm.enorm, OfNat.ofNat, Eq, MeasureTheory.eLpNorm

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, MeasureTheory.eLpNorm_zero, MeasureTheory.eLpNorm_congr_enorm_ae, Filter.Eventually, congrFun', Filter, funext, enorm_zero

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  2. lemma MeasureTheory.eLpNorm_zero_of_ae_zero line 28 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ENormedAddMonoid, Filter.EventuallyEq, MeasureTheory.ae, OfNat.ofNat, Eq, MeasureTheory.eLpNorm

    Proof uses: MeasureTheory.eLpNorm_zero_of_ae_zero', id, Function.comp, ENorm.enorm, Eq.mpr, Filter.Eventually, congrFun', Filter, congrArg, funext

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  3. theorem MeasureTheory.eLpNormEssSup_map_measure' replace the unprimed mathlib version line 41 source

    Source comment

    replace the unprimed mathlib version

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, OpensMeasurableSpace, AEMeasurable, MeasureTheory.Measure.map, Eq, ENNReal, MeasureTheory.eLpNormEssSup, Function.comp

    Proof uses: essSup_map_measure, ENorm.enorm, AEMeasurable.enorm, Filter.isCobounded_le_of_bot, Filter.map, MeasureTheory.ae, Filter.isBounded_le_of_top

    37 instances, coercions and auxiliary constants left out.

    theorem eLpNormEssSup_map_measure' [MeasurableSpace E] [OpensMeasurableSpace E]
    (hg : AEMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    eLpNormEssSup g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ :=
…

    Mentions: E, g

  4. theorem MeasureTheory.eLpNorm_map_measure' replace the unprimed mathlib version line 47 source

    Source comment

    replace the unprimed mathlib version

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, NormedAddCommGroup, OpensMeasurableSpace, AEMeasurable, MeasureTheory.Measure.map, Eq, MeasureTheory.eLpNorm, Function.comp

    Proof uses: dite, OfNat.ofNat, of_eq_true, Eq.trans, True, congr, congrArg, MeasureTheory.eLpNorm_exponent_zero, eq_self, Eq.symm, Not, Top.top, Eq.mpr, id, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_map_measure', HPow.hPow, Real, MeasureTheory.lintegral and 9 more

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

    theorem eLpNorm_map_measure' [MeasurableSpace E] [OpensMeasurableSpace E]
    (hg : AEMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ := by
…

    Mentions: E, g

  5. theorem MeasureTheory.eLpNorm_comp_measurePreserving' replace the unprimed version line 60 source

    Source comment

    replace the unprimed version

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, NormedAddCommGroup, OpensMeasurableSpace, AEMeasurable, MeasureTheory.MeasurePreserving, Eq, MeasureTheory.eLpNorm, Function.comp

    Proof uses: Eq.symm, Eq.rec, MeasureTheory.Measure.map, MeasureTheory.eLpNorm_map_measure', MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.MeasurePreserving.aemeasurable

    16 instances, coercions and auxiliary constants left out.

    theorem eLpNorm_comp_measurePreserving' {ν : Measure β} [MeasurableSpace E]
    [OpensMeasurableSpace E] (hg : AEMeasurable g ν) (hf : MeasurePreserving f μ ν) :
    eLpNorm (g ∘ f) p μ = eLpNorm g p ν :=
…

    Mentions: E, g

  6. theorem MeasureTheory.eLpNormEssSup_iSup line 69 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasureTheory.Measure, ENNReal, Eq, MeasureTheory.eLpNormEssSup, iSup

    Proof uses: id, Eq.mpr, essSup, ENorm.enorm, InfSet.sInf, Set.ofPred, Set, LT.lt, OfNat.ofNat, congr, congrArg, essSup_eq_sInf, funext, le_antisymm, sInf_le, Membership.mem, Iff.mp, LE.le, nonpos_iff_eq_zero, Trans.trans and 33 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

    Open to load the checked before-and-after goal states.

  7. theorem MeasureTheory.eLpNorm_iSup' Monotone convergence applied to eLpNorms line 101 source

    Source documentation

    Monotone convergence applied to eLpNorms. AEMeasurable variant. Possibly imperfect hypotheses, particularly on p. Note that for p = ∞ the stronger statement in eLpNormEssSup_iSup holds.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Nat, AEMeasurable, Filter.Eventually, Monotone, MeasureTheory.ae, Eq, MeasureTheory.eLpNorm, iSup

    Proof uses: id, dite, ite, OfNat.ofNat, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', ENNReal.toReal, Eq.mpr, congr, congrArg, ite_eq_left, funext, of_eq_true, Eq.trans, True, ciSup_const, eq_self, Not, ite_eq_right and 31 more

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

    Open to load the checked before-and-after goal states.

    theorem eLpNorm_iSup' {α : Type*} [MeasurableSpace α] {μ : Measure α} {p : ℝ≥0∞}
    {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, AEMeasurable (f n) μ) (h_mono : ∀ᵐ x ∂μ, Monotone fun n => f n x) :
    eLpNorm (fun x => ⨆ n, f n x) p μ = ⨆ n, eLpNorm (f n) p μ := by
…
  8. lemma MeasureTheory.eLpNormEssSup_indicator_const_eq' complements the mathlib lemma eLpNormEssSup_indicator_const_eq line 125 source

    Source comment

    complements the mathlib lemma eLpNormEssSup_indicator_const_eq

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, Set, Eq, ENNReal, OfNat.ofNat, MeasureTheory.eLpNormEssSup, Set.indicator

    Proof uses: Eq.mpr, MeasureTheory.eLpNorm, Top.top, id, congrArg, Eq.symm, MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNorm_zero_of_ae_zero', Filter.mp_mem, MeasureTheory.ae, Compl.compl, Set.ofPred, Function.comp, ENorm.enorm, Eq.mp, Membership.mem, Filter, propext, MeasureTheory.mem_ae_iff, compl_compl and 4 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

    lemma eLpNormEssSup_indicator_const_eq' {s : Set α} {c : ε} (hμs : μ s = 0) :
    eLpNormEssSup (s.indicator fun _ : α => c) μ = 0 := by
…

    Mentions: s, c

  9. theorem MeasureTheory.eLpNorm'_const_smul_le'' line 146 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, Real, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENormSMulClass, LT.lt, OfNat.ofNat, LE.le, ENNReal, MeasureTheory.eLpNorm', HSMul.hSMul, HMul.hMul, ENorm.enorm

    Proof uses: MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul', NNNorm.nnnorm, Filter.Eventually.of_forall, MeasureTheory.ae, le_of_eq, enorm_smul

    36 instances, coercions and auxiliary constants left out.

  10. theorem MeasureTheory.eLpNormEssSup_const_smul_le'' line 150 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENormSMulClass, LE.le, ENNReal, MeasureTheory.eLpNormEssSup, HSMul.hSMul, HMul.hMul, ENorm.enorm

    Proof uses: MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul', Filter.Eventually.of_forall, MeasureTheory.ae, of_eq_true, Eq.trans, True, congr, congrArg, enorm_smul, congrFun', enorm_NNReal

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  11. theorem MeasureTheory.eLpNorm_const_smul_le'' line 154 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENormSMulClass, LE.le, MeasureTheory.eLpNorm, HSMul.hSMul, HMul.hMul, ENorm.enorm

    Proof uses: MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul', NNNorm.nnnorm, Filter.Eventually.of_forall, MeasureTheory.ae, le_of_eq, enorm_smul

    30 instances, coercions and auxiliary constants left out.

  12. theorem MeasureTheory.MemLp.const_smul'' line 158 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENormSMulClass, ContinuousConstSMul, MeasureTheory.MemLp, HSMul.hSMul

    Proof uses: And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, MeasureTheory.eLpNorm, Top.top, MeasureTheory.AEStronglyMeasurable.const_smul, And.left, LE.le.trans_lt, HMul.hMul, ENorm.enorm, MeasureTheory.eLpNorm_const_smul_le'', ENNReal.mul_lt_top, ENNReal.coe_lt_top, NNNorm.nnnorm, And.right

    22 instances, coercions and auxiliary constants left out.

  13. theorem MeasureTheory.MemLp.const_mul'' line 162 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, ENNReal, MeasureTheory.Measure, TopologicalSpace, ESeminormedAddMonoid, SMul, NNReal, ENormSMulClass, ContinuousConstSMul, MeasureTheory.MemLp, HSMul.hSMul

    Proof uses: MeasureTheory.MemLp.const_smul''

    9 instances, coercions and auxiliary constants left out.

  14. lemma MeasureTheory.MemLp.eLpNormEssSup_lt_top line 172 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, ENorm, MeasureTheory.MemLp, Top.top, ENNReal, LT.lt, MeasureTheory.eLpNormEssSup

    Proof uses: And.right, MeasureTheory.AEStronglyMeasurable, Eq.mp, And, MeasureTheory.eLpNorm, congrArg, congrFun', MeasureTheory.eLpNorm_exponent_top

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.