Carleson/HolderNorm.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

8 declarations, 0 contain sorry, 0 declared as axioms

L^∞-normalized t-Hölder norm

This file defines the L^∞-normalized t-Hölder norm, which probably in some form should end up in Mathlib. Lemmas about this norm that are proven in Carleson are collected here.

TODO: Assess Mathlib-readiness, complete basic results, optimize imports.

Imports (1)
Imported by 2 files
  1. def iHolENorm the L^∞-normalized t-Hölder norm line 26 source

    Source documentation

    the L^∞-normalized t-Hölder norm. Defined in ℝ≥0∞ to avoid sup-related issues.

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

    Statement uses: PseudoMetricSpace, NormedField, Real, ENNReal

    Proof uses: HAdd.hAdd, iSup, Membership.mem, Set, Metric.ball, ENorm.enorm, HMul.hMul, HPow.hPow, ENNReal.ofReal, Ne, HDiv.hDiv, HSub.hSub, EDist.edist

    43 instances, coercions and auxiliary constants left out.

    def iHolENorm (φ : X → 𝕜) (x₀ : X) (R : ℝ) (t : ℝ) : ℝ≥0∞ :=
…
  2. def iHolNNNorm The NNReal version of the L^∞-normalized t-Hölder norm, iHolENorm line 31 source

    Source documentation

    The NNReal version of the L^∞-normalized t-Hölder norm, iHolENorm.

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

    Statement uses: PseudoMetricSpace, NormedField, Real, NNReal

    Proof uses: ENNReal.toNNReal, iHolENorm

    def iHolNNNorm (φ : X → 𝕜) (x₀ : X) (R : ℝ) (t : ℝ) : ℝ≥0 :=
…
  3. lemma enorm_le_iHolENorm_of_mem line 41 source

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

    Statement uses: Real, MetricSpace, NormedField, Membership.mem, Set, Metric.ball, LE.le, ENNReal, ENorm.enorm, iHolENorm

    Proof uses: le_trans, iSup, HAdd.hAdd, HMul.hMul, HPow.hPow, ENNReal.ofReal, Ne, HDiv.hDiv, HSub.hSub, EDist.edist, Eq.mpr, id, Eq, Eq.trans, forall_congr, implies_congr, Eq.refl, le_self_add

    71 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  4. lemma HolderOnWith.of_iHolENorm_ne_top line 46 source

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

    Statement uses: Real, MetricSpace, NormedField, LE.le, OfNat.ofNat, Ne, ENNReal, iHolENorm, Top.top, HolderOnWith, HDiv.hDiv, NNReal, iHolNNNorm, HPow.hPow, Real.toNNReal, Metric.ball

    Proof uses: Membership.mem, Set, LT.lt, LE.le.trans_lt, Dist.dist, dist_nonneg, Eq.mp, Eq, Or, EDist.edist, HMul.hMul, eq_or_ne, of_eq_true, Eq.trans, Max.max, True, congr, congrArg, WeakPseudoEMetricSpace.edist_self, congrFun' and 44 more

    137 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  5. lemma continuous_of_iHolENorm_ne_top line 67 source

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

    Statement uses: Real, MetricSpace, NormedField, LT.lt, OfNat.ofNat, LE.le, Set, tsupport, Metric.ball, Ne, ENNReal, iHolENorm, Top.top, Continuous

    Proof uses: ContinuousOn.continuous_of_tsupport_subset, HolderOnWith.continuousOn, HDiv.hDiv, NNReal, iHolNNNorm, HPow.hPow, Real.toNNReal, HolderOnWith.of_iHolENorm_ne_top, LT.lt.le, of_eq_true, Eq.trans, True, eq_true, Metric.isOpen_ball

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  6. lemma continuous_of_iHolENorm_ne_top' line 73 source

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

    Statement uses: Real, MetricSpace, NormedField, LT.lt, OfNat.ofNat, LE.le, Set, Function.support, Metric.ball, Ne, ENNReal, iHolENorm, HMul.hMul, Nat, Top.top, Continuous

    Proof uses: Or, le_or_gt, EmptyCollection.emptyCollection, Eq.mp, congrArg, Iff.mpr, Eq, Metric.ball_eq_empty, Eq.mpr, id, Eq.trans, continuous_const, Zero, ContinuousOn.continuous_of_tsupport_subset, HolderOnWith.continuousOn, HDiv.hDiv, NNReal, iHolNNNorm, HPow.hPow, Real.toNNReal and 65 more

    115 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  7. lemma norm_le_iHolNNNorm_of_mem line 88 source

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

    Statement uses: Real, MetricSpace, NormedField, Ne, ENNReal, iHolENorm, Top.top, Membership.mem, Set, Metric.ball, LE.le, Norm.norm, iHolNNNorm

    Proof uses: Iff.mpr, ENNReal.toReal, ENorm.enorm, ENNReal.toReal_le_toReal, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, not_false_eq_true, enorm_le_iHolENorm_of_mem

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma norm_le_iHolNNNorm_of_subset line 92 source

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

    Statement uses: Real, MetricSpace, NormedField, Ne, ENNReal, iHolENorm, Top.top, LE.le, Set, Function.support, Metric.ball, Norm.norm, iHolNNNorm

    Proof uses: dite, Membership.mem, Classical.propDecidable, norm_le_iHolNNNorm_of_mem, Not, of_eq_true, Eq.trans, OfNat.ofNat, True, congrFun', congrArg, Iff.mp, Eq, Function.notMem_support, norm_zero

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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