Carleson/ToMathlib/IntegralBallContinuity.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

5 declarations, 0 contain sorry, 0 declared as axioms

This file contains results about continuity of integrals and averages over balls that were unused in HardyLittleWood, and whose destiny in Mathlib is unclear.

Imports (2)
Imported by 1 file
  1. lemma MeasureTheory.LocallyIntegrable.integrableOn_of_isBounded move line 20 source

    Source comment

    move

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

    Statement uses: MeasurableSpace, PseudoMetricSpace, NormedAddCommGroup, MeasureTheory.Measure, ProperSpace, MeasureTheory.LocallyIntegrable, Set, Bornology.IsBounded, MeasureTheory.IntegrableOn

    Proof uses: MeasureTheory.IntegrableOn.mono_set, closure, MeasureTheory.LocallyIntegrable.integrableOn_isCompact, Bornology.IsBounded.isCompact_closure, subset_closure

    18 instances, coercions and auxiliary constants left out.

    lemma MeasureTheory.LocallyIntegrable.integrableOn_of_isBounded [ProperSpace X]
    {f : X → E} (hf : LocallyIntegrable f μ) {s : Set X}
    (hs : IsBounded s) : IntegrableOn f s μ :=
…

    Mentions: E, s

  2. lemma MeasureTheory.LocallyIntegrable.integrableOn_ball move line 26 source

    Source comment

    move

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

    Statement uses: MeasurableSpace, PseudoMetricSpace, NormedAddCommGroup, MeasureTheory.Measure, ProperSpace, MeasureTheory.LocallyIntegrable, Real, MeasureTheory.IntegrableOn, Metric.ball

    Proof uses: MeasureTheory.LocallyIntegrable.integrableOn_of_isBounded, Metric.isBounded_ball

    12 instances, coercions and auxiliary constants left out.

    lemma MeasureTheory.LocallyIntegrable.integrableOn_ball [ProperSpace X]
    {f : X → E} (hf : LocallyIntegrable f μ) {x : X} {r : ℝ} : IntegrableOn f (ball x r) μ :=
…

    Mentions: E

  3. lemma continuous_integral_ball line 32 source

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

    Statement uses: MeasurableSpace, PseudoMetricSpace, MeasureTheory.Measure, OpensMeasurableSpace, ENNReal, Real, GT.gt, OfNat.ofNat, LT.lt, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Metric.ball, Top.top, AEMeasurable, Eq, Set, Metric.sphere, ContinuousOn, Prod, Prod.fst and 4 more

    Proof uses: Membership.mem, Eq.mp, Eq.trans, And, True, congr, congrArg, true_and, id, ContinuousWithinAt, Filter.Tendsto, nhdsWithin, nhds, Set.indicator, funext, Eq.mpr, Eq.symm, MeasureTheory.lintegral_indicator, measurableSet_ball, Eq.refl and 138 more

    180 instances, coercions and auxiliary constants left out.

    Tactic trace: 106 steps

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

  4. lemma continuous_average_ball unused in Carleson move to separate file (not sure where) line 127 source

    Source comment

    unused in Carleson move to separate file (not sure where)

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

    Statement uses: MeasurableSpace, PseudoMetricSpace, NormedAddCommGroup, MeasureTheory.Measure, MeasureTheory.Measure.IsOpenPosMeasure, MeasureTheory.IsFiniteMeasureOnCompacts, OpensMeasurableSpace, ProperSpace, MeasureTheory.LocallyIntegrable, Real, GT.gt, OfNat.ofNat, Eq, ENNReal, Set, Metric.sphere, ContinuousOn, Prod, MeasureTheory.laverage, MeasureTheory.Measure.restrict and 7 more

    Proof uses: Eq.mpr, Membership.mem, ContinuousAt, id, congrArg, propext, IsOpen.continuousOn_iff, IsOpen.prod, isOpen_univ, isOpen_Ioi, LT.lt, Eq.mp, Eq.trans, And, True, congr, true_and, HMul.hMul, Inv.inv, MeasureTheory.lintegral and 36 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

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

    lemma continuous_average_ball [μ.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts μ] [OpensMeasurableSpace X]
    [ProperSpace X] (hf : LocallyIntegrable f μ)
    (hμ : ∀ z : X, ∀ r > (0 : ℝ), μ (sphere z r) = 0) :
    ContinuousOn (fun x : X × ℝ ↦ ⨍⁻ y in ball x.1 x.2, ‖f y‖ₑ ∂μ) (univ ×ˢ Ioi 0) := by
…
  5. lemma lowerSemiContinuousOn_integral_ball unused in Carleson move to separate file (not sure where) line 160 source

    Source comment

    unused in Carleson move to separate file (not sure where)

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

    Statement uses: MeasurableSpace, PseudoMetricSpace, NormedAddCommGroup, MeasureTheory.Measure, OpensMeasurableSpace, MeasureTheory.AEStronglyMeasurable, LowerSemicontinuousOn, Prod, Real, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Metric.ball, Prod.fst, Prod.snd, ENorm.enorm, SProd.sprod, Set, Set.univ, Set.Ioi and 1 more

    Proof uses: Iff.mpr, Membership.mem, LE.le, Filter.liminf, nhdsWithin, lowerSemicontinuousOn_iff_le_liminf, le_of_forall_pos_le_add, LT.lt, HAdd.hAdd, dite, Eq, Top.top, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, top_add, Not and 72 more

    162 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

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

    lemma lowerSemiContinuousOn_integral_ball [OpensMeasurableSpace X] (hf2 : AEStronglyMeasurable f μ) :
    LowerSemicontinuousOn (fun x : X × ℝ ↦ ∫⁻ y in ball x.1 x.2, ‖f y‖ₑ ∂μ) (univ ×ˢ Ioi 0) := by
…