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

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. theorem ContinuousWithinAt.ennreal_mul line 12 source

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

    Statement uses: TopologicalSpace, ENNReal, Set, ContinuousWithinAt, Or, Ne, OfNat.ofNat, Top.top, HMul.hMul

    Proof uses: Membership.mem, Filter, nhds, ENNReal.Tendsto.mul, nhdsWithin

    19 instances, coercions and auxiliary constants left out.

  2. lemma ContinuousWithinAt.measure_lt_ne_zero TODO: generalize? line 21 source

    Source comment

    TODO: generalize?

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, LinearOrder, DenselyOrdered, OrderTopology, ClosedIicTopology, MeasureTheory.Measure.IsOpenPosMeasure, ENNReal, Not, IsMax, ContinuousWithinAt, Set.Ioi, LT.lt, Ne, Set, Set.ofPred, OfNat.ofNat

    Proof uses: Membership.mem, Filter, Filter.map, nhdsWithin, IsOpen.mem_nhds, isOpen_Ioi, Eq.mpr, id, Eq, Bot.bot, congrArg, Eq.symm, ENNReal.bot_eq_zero, propext, bot_lt_iff_ne_bot, And, IsOpen, LE.le, Inter.inter, Set.preimage and 13 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

    lemma ContinuousWithinAt.measure_lt_ne_zero {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α]
    [OrderTopology α] [ClosedIicTopology α] [μ.IsOpenPosMeasure] {f : α → ℝ≥0∞} {x : α}
    (hx : ¬IsMax x) (hf : ContinuousWithinAt f (Set.Ioi x) x)
    {a : ℝ≥0∞} (ha : a < f x) :
    μ {y | a < f y} ≠ 0 := by
…
  3. lemma eLpNormEssSup_eq_iSup' TODO: generalize? line 49 source

    Source comment

    TODO: generalize? currently unused

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

    Statement uses: ENNReal, LT.lt, ContinuousWithinAt, Set.Ioi, Eq, Top.top, Bot.bot, MeasureTheory.eLpNormEssSup, MeasureTheory.MeasureSpace.volume, iSup

    Proof uses: Eq.symm, iSup_eq_essSup, ContinuousWithinAt.measure_lt_ne_zero, Mathlib.Tactic.Contrapose.contrapose₃, IsMax, Eq.mpr, Not, LE.le, id, implies_congr, Eq.refl, congrArg, Eq.mp, propext, isMax_iff_eq_top, zero_le

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

    lemma eLpNormEssSup_eq_iSup' {f : ℝ≥0∞ → ℝ≥0∞}
  (hf : ∀ (a : ℝ≥0∞) (x : ℝ≥0∞), a < f x → ContinuousWithinAt f (Set.Ioi x) x) (f_top : f ⊤ = ⊥) :
    eLpNormEssSup f volume = ⨆ x, f x := by
…
  4. lemma eLpNormEssSup_nnreal_eq_iSup_nnreal TODO: generalize? line 62 source

    Source comment

    TODO: generalize?

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

    Statement uses: ENNReal, NNReal, LT.lt, ContinuousWithinAt, Set.Ioi, Eq, MeasureTheory.eLpNormEssSup, MeasureTheory.MeasureSpace.volume, iSup

    Proof uses: Eq.symm, iSup_eq_essSup, ContinuousWithinAt.measure_lt_ne_zero, of_eq_true, Not, IsMax, Eq.trans, False, True, congrArg, not_false_eq_true, Set.univ, Continuous.continuousWithinAt, ENNReal.continuous_coe, Eq.mpr, Function.comp, Inter.inter, Set, Set.preimage, eq_of_heq and 14 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

    lemma eLpNormEssSup_nnreal_eq_iSup_nnreal {f : ℝ≥0∞ → ℝ≥0∞}
  (hf : ∀ (a : ℝ≥0∞) (x : ℝ≥0), a < f x → ContinuousWithinAt f (Set.Ioi ↑x) ↑x) :
    eLpNormEssSup (fun t : ℝ≥0 ↦ f t) volume = ⨆ (x : ℝ≥0), f x := by
…