Carleson/Classical/ControlApproximationEffectBasic.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

13 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
Imported by 3 files
  1. lemma ENNReal.le_on_subset TODO: might be generalized line 22 source

    Source comment

    TODO: might be generalized.

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, Set, MeasurableSet, Measurable, Membership.mem, LE.le, HAdd.hAdd, Exists, And, HMul.hMul, OfNat.ofNat, Nat, Or, HDiv.hDiv

    Proof uses: Inter.inter, Set.preimage, Set.Ici, Eq, rfl, Union.union, Eq.mpr, id, congrArg, Eq.trans, congr, Classical.byContradiction, Not, absurd, False, le_refl, LT.lt, Trans.trans, ENNReal.add_lt_add, And.left and 59 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

    lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : Measure X) {f g : X → ℝ≥0∞}
    {E : Set X} (hE : MeasurableSet E)
    (hf : Measurable f) (hg : Measurable g) {a : ℝ≥0∞} (h : ∀ x ∈ E, a ≤ f x + g x) :
    ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E'
      ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ (∀ x ∈ E', a / 2 ≤ g x)) := by
…

    Mentions: g, E

  2. lemma Dirichlet_Hilbert_eq line 63 source

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

    Statement uses: Nat, Real, Eq, Complex, HMul.hMul, Max.max, HSub.hSub, OfNat.ofNat, abs, dirichletKernel', HAdd.hAdd, Complex.exp, Complex.I, Neg.neg, k, RingHom, starRingEnd

    Proof uses: Eq.mpr, HDiv.hDiv, id, congr, congrArg, Eq.trans, mul_comm, congrFun', mul_neg, map_mul, map_neg, NNRat, RingHom.id, Complex.conj_I, Complex.conj_ofReal, map_natCast, neg_neg, map_div₀, map_sub, map_one and 43 more

    132 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  3. lemma Dirichlet_Hilbert_diff line 69 source

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

    Statement uses: Nat, Real, Membership.mem, Set, Set.Icc, Neg.neg, Real.pi, LE.le, Norm.norm, Complex, HSub.hSub, dirichletKernel', HAdd.hAdd, HMul.hMul, Complex.exp, Complex.I, k, RingHom, starRingEnd

    Proof uses: Eq.mpr, Max.max, OfNat.ofNat, abs, id, Eq, congrArg, Eq.symm, Dirichlet_Hilbert_eq, dite, dirichletKernel'_eq_zero, Eq.mp, propext, sub_eq_zero, of_eq_true, Eq.trans, True, congrFun', MulZeroClass.mul_zero, sub_self and 142 more

    241 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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

  4. lemma le_iSup_of_tendsto line 117 source

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

    Statement uses: TopologicalSpace, CompleteLinearOrder, OrderTopology, Nonempty, SemilatticeSup, Filter.Tendsto, Filter.atTop, nhds, LE.le, iSup

    Proof uses: le_of_forall_lt, LT.lt, Filter.Eventually, Filter.Tendsto.eventually_const_lt, Exists, Filter.Eventually.exists, lt_of_lt_of_le, le_iSup

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  5. lemma integrable_annulus line 125 source

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

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Complex, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Neg.neg, LE.le, LT.lt, MeasureTheory.Integrable, MeasureTheory.Measure.restrict, Set.ofPred, Set.Ioo, Dist.dist

    Proof uses: Eq.mpr, MeasureTheory.IntegrableOn, id, Eq, congrArg, Eq.symm, MeasureTheory.IntegrableOn.eq_1, Union.union, HSub.hSub, HAdd.hAdd, annulus_real_eq, MeasureTheory.IntegrableOn.union, propext, intervalIntegrable_iff_integrableOn_Ioo_of_le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 69 more

    140 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  6. lemma intervalIntegrable_mul_dirichletKernel' line 136 source

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

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Complex, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Neg.neg, dirichletKernel', HSub.hSub, HAdd.hAdd

    Proof uses: IntervalIntegrable.mul_bdd, Function.comp, id, IntervalIntegrable.mono_set, Eq.mpr, LE.le, Set.uIcc, Eq, congrArg, Set.uIcc_of_le, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance and 63 more

    128 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  7. lemma intervalIntegrable_mul_dirichletKernel'_max line 148 source

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

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Complex, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Neg.neg, Max.max, HSub.hSub, abs, dirichletKernel', HAdd.hAdd

    Proof uses: Eq.mpr, id, Eq, congrFun', MeasureTheory.Measure, congrArg, funext, Eq.trans, Eq.symm, mul_assoc, Eq.refl, intervalIntegrable_mul_dirichletKernel', Function.comp, IntervalIntegrable.mul_bdd, Measurable.aestronglyMeasurable, Measurable.comp, Complex.measurable_ofReal, Measurable.max, Measurable.const_sub, Continuous.measurable and 14 more

    140 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  8. lemma intervalIntegrable_mul_dirichletKernel'_max' line 161 source

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

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Complex, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Neg.neg, HSub.hSub, dirichletKernel', Max.max, abs, HAdd.hAdd

    Proof uses: Eq.mpr, id, Eq, congrFun', MeasureTheory.Measure, congrArg, funext, Eq.trans, mul_sub, Eq.refl, IntervalIntegrable.sub, intervalIntegrable_mul_dirichletKernel', intervalIntegrable_mul_dirichletKernel'_max

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  9. lemma domain_reformulation line 170 source

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

    Statement uses: Real, Complex, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Neg.neg, Real.pi, HMul.hMul, OfNat.ofNat, Nat, Membership.mem, Set, Set.Icc, Eq, intervalIntegral, Max.max, HSub.hSub, abs, dirichletKernel', HAdd.hAdd, MeasureTheory.integral and 4 more

    Proof uses: Trans.trans, rfl, Eq.mpr, Union.union, id, congrArg, annulus_real_eq, le_refl, MeasureTheory.setIntegral_union, of_eq_true, Disjoint, Eq.trans, LE.le, Min.min, True, congr, sub_zero, congrFun', add_zero, Or and 121 more

    237 instances, coercions and auxiliary constants left out.

    Tactic trace: 55 steps

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

  10. lemma intervalIntegrable_mul_dirichletKernel'_specific line 213 source

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

    Statement uses: Real, Membership.mem, Set, Set.Icc, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Complex, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Neg.neg, MeasureTheory.IntegrableOn, Max.max, HSub.hSub, abs, dirichletKernel', Set.ofPred, Set.Ioo, Dist.dist

    Proof uses: HAdd.hAdd, intervalIntegrable_mul_dirichletKernel'_max, MeasureTheory.IntegrableOn.mono_set, Eq.mp, congrArg, propext, intervalIntegrable_iff_integrableOn_Ioo_of_le, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 65 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  11. lemma le_CarlesonOperatorReal line 228 source

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

    Statement uses: Real, Complex, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Neg.neg, Real.pi, HMul.hMul, OfNat.ofNat, Nat, Membership.mem, Set, Set.Icc, LE.le, ENNReal, ENorm.enorm, intervalIntegral, Max.max, HSub.hSub, abs, dirichletKernel' and 6 more

    Proof uses: Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.ofPred, Set.Ioo, Dist.dist, id, Eq, congrArg, domain_reformulation, HDiv.hDiv, rfl, Set.iUnion, Set.ext, Iff.intro, LT.lt, Exists, exists_nat_gt, propext, Set.mem_iUnion and 224 more

    403 instances, coercions and auxiliary constants left out.

    Tactic trace: 132 steps

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

  12. def operatorBound The function used to bound the partial Fourier sum in partialFourierSum_bound line 366 source

    Source documentation

    The function used to bound the partial Fourier sum in partialFourierSum_bound

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

    Statement uses: Real, Complex, ENNReal

    Proof uses: HAdd.hAdd, HDiv.hDiv, carlesonOperatorReal, K, Function.comp, RingHom, starRingEnd, ENNReal.ofReal, HMul.hMul, OfNat.ofNat, Real.pi, MeasureTheory.eLpNorm, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc

    38 instances, coercions and auxiliary constants left out.

    def operatorBound (g : ℝ → ℂ) (x : ℝ) : ℝ≥0∞ :=
…

    Mentions: g

  13. lemma partialFourierSum_bound line 370 source

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

    Statement uses: Real, Complex, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, IntervalIntegrable, MeasureTheory.MeasureSpace.volume, Membership.mem, Set, Set.Icc, LE.le, ENNReal, ENorm.enorm, partialFourierSum, operatorBound

    Proof uses: Neg.neg, Function.Periodic.intervalIntegrable₀, LT.lt.ne', Real.two_pi_pos, Eq, HDiv.hDiv, HAdd.hAdd, intervalIntegral, Max.max, HSub.hSub, abs, dirichletKernel', Trans.trans, rfl, Eq.mpr, id, congrArg, partialFourierSum_eq_conv_dirichletKernel', IntervalIntegrable.mono_set, Set.uIcc and 173 more

    252 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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