Carleson/TwoSidedCarleson/WeakCalderonZygmund.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

127 declarations, 0 contain sorry, 0 declared as axioms

Section 10.2 and Lemma 10.0.3

Question:

Imports (2)
Imported by 3 files
  1. class IsTwoSidedKernel K is a two-sided Calderon-Zygmund kernel line 17 source

    Source documentation

    K is a two-sided Calderon-Zygmund kernel. In the formalization K x y is defined everywhere, even for x = y. The assumptions on K show that K x x = 0.

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

    Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, outParam, Nat, Complex

    class IsTwoSidedKernel {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (a : outParam ℕ)
    (K : X → X → ℂ) extends IsOneSidedKernel a K where
…

    Mentions: K, IsOneSidedKernel

  2. theorem maximal_theorem Lemma 10.2.1, formulated differently line 41 source

    Source documentation

    Lemma 10.2.1, formulated differently. The blueprint version is basically this after unfolding HasBoundedWeakType, wnorm and wnorm'.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, MeasureTheory.HasBoundedWeakType, Complex, ENNReal, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Real, C10_2_1

    Proof uses: MeasureTheory.HasWeakType.hasBoundedWeakType, Eq, C_weakType_maximalFunction, id, dite, ite, HPow.hPow, HDiv.hDiv, C2_0_6, Eq.mpr, congrArg, ite_eq_left, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congr, HMul.hMul, C10_2_1_def, pow_mul' and 29 more

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

    theorem maximal_theorem :
    HasBoundedWeakType (globalMaximalFunction volume 1 : (X → ℂ) → X → ℝ≥0∞) 1 1 volume volume
      (C10_2_1 a) := by
…
  3. theorem maximal_theorem' line 54 source
  4. theorem maximal_theorem'' Alternate version of maximal_theorem' line 64 source

    Source comment

    Alternate version of `maximal_theorem'`
    private theorem maximal_theorem'' (hα : 0 < α) (hf : BoundedFiniteSupport f) :
    volume {x | α < ‖globalMaximalFunction volume 1 f x‖ₑ} ≤
    (C10_2_1 a) * eLpNorm f 1 volume / α := by
…

    Mentions: BoundedFiniteSupport

  5. theorem lebesgue_differentiation Lemma 10.2.2 line 73 source

    Source documentation

    Lemma 10.2.2.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Filter.Eventually, Exists, Real, And, Filter.Tendsto, MeasureTheory.average, MeasureTheory.Measure.restrict, Metric.ball, Filter.atTop, nhds, nhdsWithin, OfNat.ofNat and 5 more

    Proof uses: GT.gt, LE.le, ENNReal, Metric.closedBall, HMul.hMul, HPow.hPow, Trans.trans, OfScientific.ofScientific, Bool.true, MeasureTheory.measure_mono, Metric.closedBall_subset_ball, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 195 more

    307 instances, coercions and auxiliary constants left out.

    Tactic trace: 55 steps

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

    theorem lebesgue_differentiation {f : X → ℂ} (hf : BoundedFiniteSupport f) :
    ∀ᵐ x ∂volume, ∃ (c : ℕ → X) (r : ℕ → ℝ),
    Tendsto (fun i ↦ ⨍ y in ball (c i) (r i), f y ∂volume) atTop (𝓝 (f x)) ∧
    Tendsto r atTop (𝓝[>] 0) ∧
    ∀ i, x ∈ ball (c i) (r i) := by
…

    Mentions: BoundedFiniteSupport, c

  6. def depth δ(x) in the blueprint line 144 source

    Source documentation

    δ(x) in the blueprint. The depth of a point x in a set O is the supremum of radii of balls centred on x that are subsets of O.

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

    Statement uses: MetricSpace, Set, ENNReal

    Proof uses: iSup, NNReal, LE.le, Metric.ball

    11 instances, coercions and auxiliary constants left out.

    def depth (O : Set X) (x : X) : ℝ≥0∞ :=
…
  7. lemma depth_lt_iff_not_disjoint line 149 source

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

    Statement uses: MetricSpace, Set, Real, Iff, LT.lt, ENNReal, depth, ENNReal.ofReal, Not, Disjoint, Metric.ball, Compl.compl

    Proof uses: Iff.intro, And, NNReal, LE.le, Exists, Eq.mp, iSup, congrArg, funext, forall_congr, Real.toNNReal, Function.mt, Membership.mem, propext, Set.not_subset_iff_exists_mem_notMem, not_le, OfNat.ofNat, LE.le.trans_lt, zero_le, Eq and 21 more

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  8. lemma le_depth_iff_subset line 165 source

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

    Statement uses: MetricSpace, Set, Real, Iff, LE.le, ENNReal, ENNReal.ofReal, depth, Metric.ball

    Proof uses: Eq.mpr, Disjoint, Compl.compl, id, Eq, congrArg, Eq.symm, propext, Set.disjoint_compl_right_iff_subset, Not, not_iff_not, LT.lt, not_le, depth_lt_iff_not_disjoint

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  9. lemma depth_pos_iff_mem A point's depth in an open set O is positive iff it lies in O line 170 source

    Source documentation

    A point's depth in an open set O is positive iff it lies in O.

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

    Statement uses: MetricSpace, Set, IsOpen, Iff, LT.lt, ENNReal, OfNat.ofNat, depth, Membership.mem

    Proof uses: Iff.intro, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, LE.le, id, Eq, implies_congr, Eq.refl, iSup, NNReal, Metric.ball, Eq.trans, forall_congr, Decidable.byContradiction, absurd, False, Metric.mem_ball_self, Eq.mp, Ne and 22 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    lemma depth_pos_iff_mem (hO : IsOpen O) : 0 < depth O x ↔ x ∈ O := by
…

    Mentions: depth

  10. lemma depth_eq_zero_iff_notMem line 181 source

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

    Statement uses: MetricSpace, Set, IsOpen, Iff, Eq, ENNReal, depth, OfNat.ofNat, Not, Membership.mem

    Proof uses: LT.lt, Iff.not, depth_pos_iff_mem, Eq.mp, LE.le, congrArg, propext, nonpos_iff_eq_zero, not_lt

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  11. lemma depth_lt_top_iff_ne_univ A point has finite depth in O iff O is not the whole space line 186 source

    Source documentation

    A point has finite depth in O iff O is not the whole space.

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

    Statement uses: MetricSpace, Set, Iff, LT.lt, ENNReal, depth, Top.top, Ne, Set.univ

    Proof uses: Iff.intro, Mathlib.Tactic.Contrapose.contrapose₃, Eq, Eq.mpr, Not, LE.le, id, implies_congr, Eq.refl, iSup, NNReal, Metric.ball, Exists, forall_congr, congrArg, funext, propext, exists_prop_congr, Iff.of_eq, True and 28 more

    85 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

    lemma depth_lt_top_iff_ne_univ : depth O x < ⊤ ↔ O ≠ univ := by
…

    Mentions: depth

  12. lemma depth_le_edist_add_depth A "triangle inequality" for depths line 201 source

    Source documentation

    A "triangle inequality" for depths.

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

    Statement uses: MetricSpace, Set, LE.le, ENNReal, depth, HAdd.hAdd, EDist.edist

    Proof uses: iSup₂_le, NNReal, Metric.ball, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, LT.lt, id, Eq, implies_congr, Eq.refl, And, Membership.mem, HSub.hSub, Real, Dist.dist, Compl.compl, Exists, Eq.mp, Disjoint and 16 more

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

    lemma depth_le_edist_add_depth : depth O x ≤ edist x y + depth O y := by
…

    Mentions: depth

  13. lemma depth_bound_1 line 210 source

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

    Statement uses: MetricSpace, Set, Ne, Set.univ, Not, Disjoint, Metric.ball, HDiv.hDiv, Real, ENNReal.toReal, depth, OfNat.ofNat, Nat, Membership.mem, HMul.hMul

    Proof uses: Eq.mpr, LT.lt, Dist.dist, id, Eq, congrArg, propext, Metric.mem_ball, ENNReal, Top.top, LT.lt.ne, Iff.mpr, depth_lt_top_iff_ne_univ, LE.le, HAdd.hAdd, Trans.trans, ENNReal.ofReal, EDist.edist, Eq.symm, ENNReal.add_div and 64 more

    139 instances, coercions and auxiliary constants left out.

    Tactic trace: 45 steps

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

  14. lemma depth_bound_2 line 246 source

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

    Statement uses: MetricSpace, Set, Ne, Set.univ, Membership.mem, Metric.ball, HMul.hMul, Real, OfNat.ofNat, Nat, HDiv.hDiv, ENNReal.toReal, depth, LE.le, HAdd.hAdd, Dist.dist

    Proof uses: ENNReal, EDist.edist, Top.top, edist_ne_top, LT.lt.ne, Iff.mpr, LT.lt, depth_lt_top_iff_ne_univ, Trans.trans, Eq, add_le_add, div_le_div_of_nonneg_right, ENNReal.toReal_mono, Eq.mpr, And, id, congrArg, propext, ENNReal.add_ne_top, And.intro and 57 more

    106 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  15. lemma depth_bound_3 line 262 source

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

    Statement uses: MetricSpace, Set, Ne, Set.univ, Membership.mem, Metric.ball, HMul.hMul, Real, OfNat.ofNat, Nat, HDiv.hDiv, ENNReal.toReal, depth, LE.le, HAdd.hAdd, Dist.dist

    Proof uses: ENNReal, Top.top, LT.lt.ne, Iff.mpr, LT.lt, depth_lt_top_iff_ne_univ, ENNReal.div_ne_top, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_zero, Bool, Bool.false, Eq.mpr, id, Eq, congrArg, mul_comm, Eq.symm and 111 more

    138 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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

  16. lemma ball_covering_bounded_intersection line 280 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Set, And, IsOpen, Ne, Set.univ, Set.Countable, Set.PairwiseDisjoint, Metric.ball, HDiv.hDiv, Real, ENNReal.toReal, depth, OfNat.ofNat, Membership.mem, LE.le and 5 more

    Proof uses: Eq.mpr, id, Eq, congrArg, rfl, LT.lt, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Metric.measure_ball_pos, div_pos, Top.top, propext, ENNReal.toReal_pos_iff, depth_pos_iff_mem, And.left, depth_lt_top_iff_ne_univ, And.intro, And.right, Mathlib.Meta.NormNum.isNat_lt_true and 57 more

    168 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

  17. lemma ball_covering' Lemma 10.2.4, but following the blueprint exactly (with a countable set of centres rather than functions from ℕ) line 318 source

    Source documentation

    Lemma 10.2.4, but following the blueprint exactly (with a countable set of centres rather than functions from ℕ).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Set, And, IsOpen, Ne, Set.univ, Exists, Real, Set.Countable, Set.PairwiseDisjoint, Metric.ball, Eq, Set.iUnion, Membership.mem, HMul.hMul, OfNat.ofNat and 8 more

    Proof uses: HDiv.hDiv, ENNReal.toReal, depth, Maximal, zorn_subset, IsChain, Exists.intro, Set.sUnion, And.intro, Eq.mpr, id, congrFun', congrArg, And.left, Iff.mpr, Set.pairwiseDisjoint_sUnion, IsChain.directedOn, And.right, Set.subset_sUnion_of_mem, Set.PairwiseDisjoint.countable_of_isOpen and 76 more

    165 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

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

    lemma ball_covering' (hO : IsOpen O ∧ O ≠ univ) :
    ∃ (U : Set X) (r : X → ℝ), U.Countable ∧ (U.PairwiseDisjoint fun c ↦ ball c (r c)) ∧
      ⋃ c ∈ U, ball c (3 * r c) = O ∧ (∀ c ∈ U, ¬Disjoint (ball c (7 * r c)) Oᶜ) ∧
      ∀ x ∈ O, {c ∈ U | x ∈ ball c (3 * r c)}.encard ≤ (2 ^ (6 * a) : ℕ) := by
…

    Mentions: c

  18. lemma ball_covering_finite line 360 source

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

    Statement uses: Nat, MetricSpace, Set, And, IsOpen, Ne, Set.univ, Real, Set.Finite, Set.PairwiseDisjoint, Metric.ball, Eq, Set.iUnion, Membership.mem, HMul.hMul, OfNat.ofNat, Not, Disjoint, Compl.compl, LE.le and 6 more

    Proof uses: Finset, CanLift.prf, Iff.mp, Set.ne_univ_iff_exists_notMem, And.right, Equiv, Subtype, Fin, Finset.card, Finset.equivFin, dite, Equiv.symm, Fin.mk, Exists.intro, And.intro, id, Function.onFun, of_eq_true, Eq.trans, eq_true and 71 more

    122 instances, coercions and auxiliary constants left out.

    Tactic trace: 93 steps

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

  19. theorem ball_covering Lemma 10.2.4 line 428 source

    Source documentation

    Lemma 10.2.4.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Set, And, IsOpen, Ne, Set.univ, Exists, Real, Set.PairwiseDisjoint, Metric.ball, Eq, Set.iUnion, HMul.hMul, OfNat.ofNat, LT.lt, Not and 8 more

    Proof uses: Set.Countable, ball_covering', Set.Finite, Set.Infinite, Or, Set.finite_or_infinite, ball_covering_finite, Equiv, Denumerable.eqv, Nonempty.some, Denumerable, Iff.mp, Nonempty, Set.countable_infinite_iff_nonempty_denumerable, And.intro, Equiv.symm, Exists.intro, of_eq_true, id, Mathlib.Tactic.Contrapose.contrapose₄ and 36 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

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

    theorem ball_covering (hO : IsOpen O ∧ O ≠ univ) :
    ∃ (c : ℕ → X) (r : ℕ → ℝ), (univ.PairwiseDisjoint fun i ↦ ball (c i) (r i)) ∧
      ⋃ i, ball (c i) (3 * r i) = O ∧ (∀ i, 0 < r i → ¬Disjoint (ball (c i) (7 * r i)) Oᶜ) ∧
      ∀ x ∈ O, {i | x ∈ ball (c i) (3 * r i)}.encard ≤ (2 ^ (6 * a) : ℕ) := by
…

    Mentions: c

  20. def GeneralCase The property specifying whether we are in the "general case" line 482 source

    Source documentation

    The property specifying whether we are in the "general case".

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal

    Proof uses: Exists, GE.ge, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Real

    31 instances, coercions and auxiliary constants left out.

    def GeneralCase (f : X → ℂ) (α : ℝ≥0∞) : Prop :=
…
  21. lemma volume_lt_of_not_GeneralCase In the finite case, the volume of X is finite line 486 source

    Source documentation

    In the finite case, the volume of X is finite.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Not, GeneralCase, LT.lt, OfNat.ofNat, MeasureTheory.Measure, Set, Set.univ, Top.top

    Proof uses: ENNReal.lt_top_of_mul_ne_top_right, LT.lt.ne, HMul.hMul, lt_of_le_of_lt, C10_2_1, MeasureTheory.eLpNorm, Eq.rec, WithBot.LT, OrderDual, globalMaximalFunction, Real, Eq, LE.le, Set.ofPred, Iff.mpr, Membership.mem, Set.eq_univ_iff_forall, Eq.mp, Eq.trans, Exists and 7 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma volume_lt_of_not_GeneralCase
    (hf : BoundedFiniteSupport f) (h : ¬ GeneralCase f α) (hα : 0 < α) :
    volume (univ : Set X) < ∞ := by
…

    Mentions: BoundedFiniteSupport, GeneralCase

  22. lemma isFiniteMeasure_of_not_generalCase line 494 source
  23. lemma isOpen_MB_preimage_Ioi line 499 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, And, IsOpen, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Real, Set.Ioi, Ne, Set, Set.univ

    Proof uses: GE.ge, And.intro, LowerSemicontinuous.isOpen_preimage, maximalFunction, Prod, Prod.fst, Prod.snd, lowerSemiContinuous_maximalFunction, Iff.mpr, Exists, Not, Membership.mem, Set.ne_univ_iff_exists_notMem, Exists.intro, Eq.mpr, LE.le, id, Eq, Eq.trans, LT.lt and 2 more

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  24. def czCenter The center of B_j in the proof of Lemma 10.2.5 (general case) line 507 source

    Source documentation

    The center of B_j in the proof of Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase

    Proof uses: Exists.choose, Exists, Real, And, Set.PairwiseDisjoint, Set, Set.univ, Metric.ball, Eq, Set.iUnion, HMul.hMul, OfNat.ofNat, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, Set.Ioi, LT.lt, Not, Disjoint, Compl.compl and 6 more

    61 instances, coercions and auxiliary constants left out.

    def czCenter (hX : GeneralCase f α) (i : ℕ) : X :=
…

    Mentions: GeneralCase

  25. def czRadius The radius of B_j in the proof of Lemma 10.2.5 (general case) line 511 source

    Source documentation

    The radius of B_j in the proof of Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Real

    Proof uses: Exists.choose, And, Set.PairwiseDisjoint, Set, Set.univ, Metric.ball, Exists, Eq, Set.iUnion, HMul.hMul, OfNat.ofNat, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, Set.Ioi, LT.lt, Not, Disjoint, Compl.compl, Membership.mem and 5 more

    62 instances, coercions and auxiliary constants left out.

    def czRadius (hX : GeneralCase f α) (i : ℕ) : ℝ :=
…

    Mentions: GeneralCase

  26. abbrev czBall The ball B_j in the proof of Lemma 10.2.5 (general case) line 515 source

    Source documentation

    The ball B_j in the proof of Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set

    Proof uses: Metric.ball, czCenter, czRadius

    14 instances, coercions and auxiliary constants left out.

    abbrev czBall (hX : GeneralCase f α) (i : ℕ) : Set X :=
…

    Mentions: GeneralCase

  27. abbrev czBall6 The ball B_j' introduced below Lemma 10.2.5 (general case) line 519 source

    Source documentation

    The ball B_j' introduced below Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set

    Proof uses: Metric.ball, czCenter, HMul.hMul, Real, OfNat.ofNat, czRadius

    19 instances, coercions and auxiliary constants left out.

    abbrev czBall6 (hX : GeneralCase f α) (i : ℕ) : Set X :=
…

    Mentions: GeneralCase

  28. abbrev czBall3 The ball B_j* in Lemma 10.2.5 (general case) line 523 source

    Source documentation

    The ball B_j* in Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set

    Proof uses: Metric.ball, czCenter, HMul.hMul, Real, OfNat.ofNat, czRadius

    19 instances, coercions and auxiliary constants left out.

    abbrev czBall3 (hX : GeneralCase f α) (i : ℕ) : Set X :=
…

    Mentions: GeneralCase

  29. abbrev czBall7 The ball B_j in the proof of Lemma 10.2.5 (general case) line 527 source

    Source documentation

    The ball B_j** in the proof of Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set

    Proof uses: Metric.ball, czCenter, HMul.hMul, Real, OfNat.ofNat, czRadius

    19 instances, coercions and auxiliary constants left out.

    abbrev czBall7 (hX : GeneralCase f α) (i : ℕ) : Set X :=
…

    Mentions: GeneralCase

  30. lemma czBall_pairwiseDisjoint line 530 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set.PairwiseDisjoint, Set, Set.univ, Metric.ball, czCenter, czRadius

    Proof uses: And.left, Exists.choose, Exists, Real, And, Eq, Set.iUnion, HMul.hMul, OfNat.ofNat, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, Set.Ioi, LT.lt, Not, Disjoint, Compl.compl, Membership.mem, LE.le, ENat and 6 more

    69 instances, coercions and auxiliary constants left out.

  31. lemma iUnion_czBall3 line 534 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Eq, Set, Set.iUnion, czBall3, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Real, Set.Ioi

    Proof uses: And.left, Metric.ball, Exists.choose, Exists, And, Set.PairwiseDisjoint, Set.univ, HMul.hMul, LT.lt, Not, Disjoint, Compl.compl, Membership.mem, LE.le, ENat, Set.encard, Set.ofPred, HPow.hPow, ball_covering, isOpen_MB_preimage_Ioi and 2 more

    78 instances, coercions and auxiliary constants left out.

  32. lemma not_disjoint_czBall7 line 538 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, LT.lt, Real, OfNat.ofNat, czRadius, Not, Disjoint, Set, czBall7, Compl.compl, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume and 1 more

    Proof uses: And.left, Exists.choose, And, Set.PairwiseDisjoint, Set.univ, Metric.ball, Exists, Eq, Set.iUnion, HMul.hMul, Membership.mem, LE.le, ENat, Set.encard, Set.ofPred, HPow.hPow, ball_covering, isOpen_MB_preimage_Ioi, Exists.choose_spec, And.right

    91 instances, coercions and auxiliary constants left out.

  33. lemma czBall_subset_czBall line 542 source
  34. lemma encard_czBall3_le Part of Lemma 10.2.5 (general case) line 550 source

    Source documentation

    Part of Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, LE.le, ENat, Set.encard, Set.ofPred, Membership.mem, Set, czBall3, HPow.hPow, OfNat.ofNat, HMul.hMul

    Proof uses: dite, LT.lt, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, Real, And.right, Exists.choose, And, Set.PairwiseDisjoint, Set.univ, Metric.ball, Exists, Eq, Set.iUnion, Set.preimage, Set.Ioi, Not, Disjoint, Compl.compl, ball_covering and 16 more

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

    lemma encard_czBall3_le {hX : GeneralCase f α} {y : X} :
    {i | y ∈ czBall3 hX i}.encard ≤ (2 ^ (6 * a) : ℕ) := by
…

    Mentions: GeneralCase, czBall3

  35. lemma mem_czBall3_finite line 557 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set.Finite, Set.ofPred, Membership.mem, Set, czBall3

    Proof uses: Set.finite_of_encard_le_coe, HPow.hPow, OfNat.ofNat, HMul.hMul, encard_czBall3_le

    23 instances, coercions and auxiliary constants left out.

  36. def czPartition Q_i in the proof of Lemma 10.2.5 (general case) line 562 source

    Source documentation

    Q_i in the proof of Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set

    Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, SDiff.sdiff, czBall3, Union.union, Set.iUnion, GT.gt, czBall

    18 instances, coercions and auxiliary constants left out.

    def czPartition (hX : GeneralCase f α) (i : ℕ) : Set X :=
…

    Mentions: GeneralCase

  37. lemma MeasurableSet.czPartition line 566 source
  38. lemma czBall_subset_czPartition line 573 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, LE.le, Set, czBall, czPartition

    Proof uses: Membership.mem, Eq.mpr, SDiff.sdiff, czBall3, Union.union, Set.iUnion, LT.lt, GT.gt, id, Eq, congrFun', congrArg, czPartition.eq_def, Set.mem_sdiff_of_mem, Real, Dist.dist, czCenter, HMul.hMul, OfNat.ofNat, czRadius and 90 more

    94 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  39. lemma czPartition_subset_czBall3 line 586 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, LE.le, Set, czPartition, czBall3

    Proof uses: Eq.mpr, SDiff.sdiff, Union.union, Set.iUnion, LT.lt, GT.gt, czBall, id, Eq, congrArg, czPartition.eq_1, Set.sdiff_subset

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  40. lemma czPartition_subset_czBall7 line 590 source
  41. lemma czPartition_pairwiseDisjoint line 594 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Set.PairwiseDisjoint, Set, Set.univ, czPartition

    Proof uses: Eq.mpr, Set.Nonempty, Inter.inter, Eq, id, Eq.trans, Membership.mem, forall_congr, True, implies_congr, Eq.refl, Exists, And, Iff.mp, Set.inter_nonempty, LT.lt, Not, LE.le, Set.iUnion, Set.subset_biUnion_of_mem and 13 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  42. lemma czPartition_pairwiseDisjoint' line 606 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Membership.mem, Set, czPartition, Eq

    Proof uses: Set.PairwiseDisjoint, Set.univ, czPartition_pairwiseDisjoint, Iff.mp, Set.Nonempty, Inter.inter, Set.pairwiseDisjoint_iff, Set.mem_univ, Exists, And, Set.inter_nonempty, Exists.intro, And.intro

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  43. lemma czPartition_pairwise_disjoint_on line 613 source
  44. lemma iUnion_czPartition line 617 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Eq, Set, Set.iUnion, czPartition, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Real, Set.Ioi

    Proof uses: Eq.mpr, czBall3, id, congrArg, Eq.symm, iUnion_czBall3, Set.ext, Iff.intro, Membership.mem, LE.le, Exists, Iff.mp, Set.mem_iUnion, Set.mem_iUnion_of_mem, czPartition_subset_czBall3, propext, Classical.byContradiction, Not, False, Eq.mp and 26 more

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  45. lemma globalMaximalFunction_preimage_finite line 638 source
  46. lemma volume_czPartition_lt_top line 655 source
  47. lemma volume_czBall7_le line 659 source
  48. lemma volume_czBall3_le line 668 source
  49. lemma laverage_czBall7_le Inequality (10.2.30) line 675 source

    Source comment

    Inequality (10.2.30)
    private lemma laverage_czBall7_le (hX : GeneralCase f α) (i : ℕ) :
    ⨍⁻ x in czBall7 hX i, ‖f x‖ₑ ∂volume ≤ α := by
…

    Mentions: GeneralCase, czBall7

  50. def czApproximation The function g in Lemma 10.2.5 line 687 source

    Source documentation

    The function g in Lemma 10.2.5. (both cases)

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal

    Proof uses: dite, GeneralCase, Classical.propDecidable, Exists, Membership.mem, Set, czPartition, MeasureTheory.average, Real, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Exists.choose, Not

    22 instances, coercions and auxiliary constants left out.

    def czApproximation (α : ℝ≥0∞) (x : X) : ℂ :=
…
  51. lemma czApproximation_def_of_mem line 692 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Membership.mem, Set, czPartition, Eq, czApproximation, MeasureTheory.average, Real, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume

    Proof uses: Exists, Exists.intro, of_eq_true, Eq.trans, eq_true, True, congrFun', congrArg, dite, Classical.propDecidable, Exists.choose, Not, dite_eq_left_of_eq_true, MeasureTheory.Measure, czPartition_pairwiseDisjoint', Exists.choose_spec, eq_self

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  52. lemma czApproximation_def_of_notMem line 698 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Not, Membership.mem, Set, Set.preimage, globalMaximalFunction, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Real, Set.Ioi, Eq, czApproximation

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, dite, Classical.propDecidable, Exists, czPartition, MeasureTheory.average, MeasureTheory.Measure.restrict, Exists.choose, eq_true, dite_eq_left_of_eq_true, dite_eq_right_of_eq_false, False, funext, eq_false, Eq.mp, propext and 6 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  53. lemma czApproximation_def_of_volume_lt line 704 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, Not, GeneralCase, Eq, czApproximation, MeasureTheory.average, Real, MeasureTheory.MeasureSpace.volume

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, dite_eq_right_of_eq_false, Classical.propDecidable, dite, Exists, Membership.mem, Set, czPartition, MeasureTheory.Measure.restrict, Exists.choose, eq_false, eq_self

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  54. lemma lintegral_czPartition_le line 708 source
  55. def czRemainder' The function b_i in Lemma 10.2.5 (general case) line 720 source

    Source documentation

    The function b_i in Lemma 10.2.5 (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase

    Proof uses: Set.indicator, czPartition, HSub.hSub, czApproximation

    18 instances, coercions and auxiliary constants left out.

    def czRemainder' (hX : GeneralCase f α) (i : ℕ) (x : X) : ℂ :=
…

    Mentions: GeneralCase

  56. lemma czRemainder'_eq_zero line 723 source
  57. def czRemainder The function b = ∑ⱼ bⱼ introduced below Lemma 10.2.5 line 733 source

    Source documentation

    The function b = ∑ⱼ bⱼ introduced below Lemma 10.2.5. In the finite case, we also use this as the function b = b₁ in Lemma 10.2.5. We choose a more convenient definition, but prove in tsum_czRemainder' that this is the same.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal

    Proof uses: HSub.hSub, czApproximation

    16 instances, coercions and auxiliary constants left out.

    def czRemainder (α : ℝ≥0∞) (x : X) : ℂ :=
…
  58. lemma tsum_czRemainder' Part of Lemma 10.2.5, this is essentially (10.2.16) (both cases) line 737 source

    Source documentation

    Part of Lemma 10.2.5, this is essentially (10.2.16) (both cases).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Eq, tsum, czRemainder', SummationFilter.unconditional, czRemainder

    Proof uses: id, dite, Set.indicator, czPartition, HSub.hSub, czApproximation, Exists, Membership.mem, Set, Classical.propDecidable, Eq.mpr, congrArg, tsum_eq_single, Ne, Set.indicator_of_notMem, Disjoint.notMem_of_mem_right, Set.indicator_of_mem, Eq.refl, Not, OfNat.ofNat and 26 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    lemma tsum_czRemainder' (hX : GeneralCase f α) (x : X) :
    ∑' i, czRemainder' hX i x = czRemainder f α x := by
…

    Mentions: GeneralCase, czRemainder', czRemainder

  59. lemma aemeasurable_czApproximation Part of Lemma 10.2.5 (both cases) line 752 source

    Source documentation

    Part of Lemma 10.2.5 (both cases).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, AEMeasurable, MeasureTheory.MeasureSpace.volume, czApproximation

    Proof uses: dite, GeneralCase, Classical.propDecidable, Exists, Membership.mem, Set, czPartition, MeasureTheory.average, Real, MeasureTheory.Measure.restrict, Exists.choose, Not, AEMeasurable.mk, Exists.intro, And, Measurable, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, And.intro and 54 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

    lemma aemeasurable_czApproximation {hf : AEMeasurable f} : AEMeasurable (czApproximation f α) := by
…

    Mentions: czApproximation

  60. lemma AEMeasurable.czRemainder' line 775 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, AEMeasurable, MeasureTheory.MeasureSpace.volume, GeneralCase, czRemainder'

    Proof uses: id, Iff.mpr, Set.indicator, czPartition, HSub.hSub, czApproximation, MeasureTheory.Measure.restrict, aemeasurable_indicator_iff, AEMeasurable.restrict, AEMeasurable.sub, aemeasurable_czApproximation

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  61. lemma BoundedFiniteSupport.czApproximation Part of Lemma 10.2.5 (both cases) line 783 source

    Source documentation

    Part of Lemma 10.2.5 (both cases).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, LT.lt, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, czApproximation

    Proof uses: dite, Nonempty, Classical.propDecidable, BoundedFiniteSupport.mk, And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm, Top.top, AEMeasurable.aestronglyMeasurable, aemeasurable_czApproximation, BoundedFiniteSupport.aemeasurable, lt_of_le_of_lt, essSup_le_of_ae_le, ENorm.enorm, Filter.Eventually.mono, LE.le, essSup, MeasureTheory.ae, MeasureTheory.Measure, ENNReal.ae_le_essSup and 70 more

    139 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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

    protected lemma BoundedFiniteSupport.czApproximation {α : ℝ≥0∞} (hα : 0 < α)
    (hf : BoundedFiniteSupport f) : BoundedFiniteSupport (czApproximation f α) := by
…

    Mentions: BoundedFiniteSupport

  62. lemma BoundedFiniteSupport.czRemainder line 812 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, LT.lt, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, czRemainder

    Proof uses: BoundedFiniteSupport.sub, czApproximation, BoundedFiniteSupport.czApproximation

    59 instances, coercions and auxiliary constants left out.

  63. lemma BoundedFiniteSupport.czRemainder' line 816 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, LT.lt, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, GeneralCase, czRemainder'

    Proof uses: BoundedFiniteSupport.indicator, HSub.hSub, czApproximation, BoundedFiniteSupport.sub, BoundedFiniteSupport.czApproximation, czPartition

    66 instances, coercions and auxiliary constants left out.

  64. lemma AEMeasurable.czRemainder line 821 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, LT.lt, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, AEMeasurable, czRemainder

    Proof uses: BoundedFiniteSupport.aemeasurable, BoundedFiniteSupport.czRemainder

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  65. lemma czApproximation_add_czRemainder Part of Lemma 10.2.5, equation (10.2.16) (both cases) line 827 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.16) (both cases). This is true by definition, the work lies in tsum_czRemainder'

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, Eq, HAdd.hAdd, czApproximation, czRemainder

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, add_sub_cancel, dite, GeneralCase, Classical.propDecidable, Exists, Membership.mem, Set, czPartition, MeasureTheory.average, Real, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Exists.choose, Not, eq_self

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    lemma czApproximation_add_czRemainder {x : X} :
    czApproximation f α x + czRemainder f α x = f x := by
…

    Mentions: czApproximation, czRemainder

  66. lemma α_le_mul_α line 831 source
  67. lemma enorm_czApproximation_le_finite Equation (10.2.17), finite case line 835 source

    Source comment

    Equation (10.2.17), finite case
    private lemma enorm_czApproximation_le_finite
    (hα : ⨍⁻ x, ‖f x‖ₑ ≤ α) (hX : ¬ GeneralCase f α) :
    ∀ᵐ x, ‖czApproximation f α x‖ₑ ≤ 2 ^ (3 * a) * α := by
…

    Mentions: GeneralCase, czApproximation

  68. lemma enorm_czApproximation_le_infinite Equation (10.2.17) specialized to the general case line 844 source

    Source documentation

    Equation (10.2.17) specialized to the general case.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, GeneralCase, Filter.Eventually, LE.le, ENorm.enorm, czApproximation, HMul.hMul, HPow.hPow, OfNat.ofNat, MeasureTheory.ae, MeasureTheory.Measure

    Proof uses: Exists, Membership.mem, Set, czPartition, Trans.trans, Inv.inv, czBall7, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.laverage, Eq, MeasureTheory.average, Real, rfl, Eq.mpr, id, congrArg, czApproximation_def_of_mem, Eq.refl, MeasureTheory.enorm_integral_le_lintegral_enorm and 74 more

    181 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

    lemma enorm_czApproximation_le_infinite {hf : BoundedFiniteSupport f} (hX : GeneralCase f α) :
    ∀ᵐ x, ‖czApproximation f α x‖ₑ ≤ 2 ^ (3 * a) * α := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czApproximation

  69. lemma enorm_czApproximation_le Part of Lemma 10.2.5, equation (10.2.17) (both cases) line 872 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.17) (both cases).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LE.le, MeasureTheory.laverage, ENorm.enorm, Filter.Eventually, czApproximation, HMul.hMul, HPow.hPow, OfNat.ofNat, MeasureTheory.ae, MeasureTheory.Measure

    Proof uses: by_cases, GeneralCase, enorm_czApproximation_le_infinite

    85 instances, coercions and auxiliary constants left out.

    lemma enorm_czApproximation_le
    {hf : BoundedFiniteSupport f} (hα : ⨍⁻ x, ‖f x‖ₑ ≤ α) :
    ∀ᵐ x, ‖czApproximation f α x‖ₑ ≤ 2 ^ (3 * a) * α :=
…

    Mentions: BoundedFiniteSupport, czApproximation

  70. lemma eLpNorm_czApproximation_le_finite Equation (10.2.18), finite case line 878 source

    Source comment

    Equation (10.2.18), finite case
    private lemma eLpNorm_czApproximation_le_finite
    (hf : BoundedFiniteSupport f) (hα : 0 < α) (hX : ¬ GeneralCase f α) :
    eLpNorm (czApproximation f α) 1 volume ≤ eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czApproximation

  71. lemma eLpNorm_czApproximation_le_infinite Equation (10.2.18), infinite case line 893 source

    Source comment

    Equation (10.2.18), infinite case
    private lemma eLpNorm_czApproximation_le_infinite (hX : GeneralCase f α) :
    eLpNorm (czApproximation f α) 1 volume ≤ eLpNorm f 1 volume := by
…

    Mentions: GeneralCase, czApproximation

  72. lemma eLpNorm_czApproximation_le Part of Lemma 10.2.5, equation (10.2.18) (both cases) line 911 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.18) (both cases).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.eLpNorm, czApproximation

    Proof uses: by_cases, GeneralCase

    66 instances, coercions and auxiliary constants left out.

    lemma eLpNorm_czApproximation_le
    {hf : BoundedFiniteSupport f} (hα : 0 < α) :
    eLpNorm (czApproximation f α) 1 volume ≤ eLpNorm f 1 volume :=
…

    Mentions: BoundedFiniteSupport, czApproximation

  73. lemma support_czRemainder'_subset Part of Lemma 10.2.5, equation (10.2.19) (general case) line 917 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.19) (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, LE.le, Set, Function.support, czRemainder', czBall3

    Proof uses: subset_trans, czPartition, Membership.mem, And.left, Not, Eq, HSub.hSub, czApproximation, OfNat.ofNat, Eq.mp, And, congrArg, propext, Classical.not_imp, Set.indicator, Set.indicator_apply_eq_zero, Ne, ne_eq, czRemainder'.eq_1, Function.mem_support and 1 more

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    lemma support_czRemainder'_subset {hX : GeneralCase f α} {i : ℕ} :
    support (czRemainder' hX i) ⊆ czBall3 hX i := by
…

    Mentions: GeneralCase, czRemainder', czBall3

  74. lemma integral_czRemainder' Part of Lemma 10.2.5, equation (10.2.20) (general case) line 924 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.20) (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, Eq, MeasureTheory.integral, Real, MeasureTheory.MeasureSpace.volume, czRemainder', OfNat.ofNat

    Proof uses: id, Eq.mpr, Set.indicator, czPartition, HSub.hSub, czApproximation, MeasureTheory.Measure.restrict, congrArg, MeasureTheory.integral_indicator, MeasureTheory.average, Eq.symm, MeasureTheory.setAverage_sub_setAverage, LT.lt.ne, MeasureTheory.Measure, Set, Top.top, MeasureTheory.setIntegral_congr_fun, Membership.mem, Pi.sub_apply, czApproximation_def_of_mem and 1 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    lemma integral_czRemainder' {hX : GeneralCase f α} {i : ℕ} :
    ∫ x, czRemainder' hX i x = 0 := by
…

    Mentions: GeneralCase, czRemainder'

  75. lemma integral_czRemainder Part of Lemma 10.2.5, equation (10.2.20) (finite case) line 933 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.20) (finite case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Not, GeneralCase, LT.lt, OfNat.ofNat, Eq, MeasureTheory.integral, Real, czRemainder

    Proof uses: MeasureTheory.IsFiniteMeasure, Eq.mpr, HSub.hSub, MeasureTheory.average, id, congrFun', congrArg, funext, czApproximation, dite_eq_right_of_eq_false, Classical.propDecidable, dite, Exists, Membership.mem, Set, czPartition, MeasureTheory.Measure.restrict, Exists.choose, eq_false, MeasureTheory.integral_sub_average

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    lemma integral_czRemainder {hf : BoundedFiniteSupport f}
    (hX : ¬ GeneralCase f α) (hα : 0 < α) :
    ∫ x, czRemainder f α x = 0 := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czRemainder

  76. lemma ineq_10_2_32 Inequality (10.2.32) line 940 source

    Source comment

    Inequality (10.2.32)
    private lemma ineq_10_2_32 (hf : BoundedFiniteSupport f) {hX : GeneralCase f α}
    {i : ℕ} :
    eLpNorm (czRemainder' hX i) 1 volume ≤ 2 * (∫⁻ x in czPartition hX i, ‖f x‖ₑ) := calc
…

    Mentions: BoundedFiniteSupport, GeneralCase, czRemainder', czPartition

  77. lemma eLpNorm_czRemainder'_le Part of Lemma 10.2.5, equation (10.2.21) (general case) line 953 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.21) (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, GeneralCase, LE.le, MeasureTheory.eLpNorm, czRemainder', OfNat.ofNat, HMul.hMul, HPow.hPow, HAdd.hAdd, MeasureTheory.Measure, Set, czBall3

    Proof uses: dite, Real, czRadius, of_eq_true, Eq.trans, True, congrFun', congrArg, autoParam, MeasureTheory.eLpNorm_zero, Not, Trans.trans, Eq, Metric.ball, czCenter, czBall7, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, czPartition, ENorm.enorm and 79 more

    176 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    lemma eLpNorm_czRemainder'_le {hf : BoundedFiniteSupport f} {hX : GeneralCase f α}
    {i : ℕ} :
    eLpNorm (czRemainder' hX i) 1 volume ≤ 2 ^ (2 * a + 1) * α * volume (czBall3 hX i) := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czRemainder', czBall3

  78. lemma eLpNorm_restrict_czRemainder'_le Weaker version of eLpNorm_czRemainder'_le which is used repeatedly below line 973 source

    Source comment

    Weaker version of `eLpNorm_czRemainder'_le` which is used repeatedly below
    private lemma eLpNorm_restrict_czRemainder'_le {hf : BoundedFiniteSupport f} {hX : GeneralCase f α}
    {i : ℕ} :
    ∫⁻ y in czBall3 hX i, ‖czRemainder' hX i y‖ₑ ≤ 2 ^ (2 * a + 1) * α * volume (czBall3 hX i) := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czBall3, czRemainder'

  79. lemma eLpNorm_czRemainder_le' Used to prove eLpNorm_czRemainder_le and tsum_eLpNorm_czRemainder_le line 981 source

    Source comment

    Used to prove `eLpNorm_czRemainder_le` and `tsum_eLpNorm_czRemainder_le`
    private lemma eLpNorm_czRemainder_le'
    (hf : BoundedFiniteSupport f) (hX : ¬ GeneralCase f α) (hα : ⨍⁻ x, ‖f x‖ₑ < α) :
    eLpNorm (czRemainder f α) 1 volume ≤ 2 * ∫⁻ x, ‖f x‖ₑ :=
…

    Mentions: BoundedFiniteSupport, GeneralCase, czRemainder

  80. lemma eLpNorm_czRemainder_le Part of Lemma 10.2.5, equation (10.2.21) (finite case) line 994 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.21) (finite case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Not, GeneralCase, LT.lt, MeasureTheory.laverage, ENorm.enorm, LE.le, MeasureTheory.eLpNorm, czRemainder, OfNat.ofNat, HMul.hMul, HPow.hPow and 4 more

    Proof uses: dite, Nonempty, Classical.propDecidable, MeasureTheory.IsFiniteMeasure, lt_of_le_of_lt, zero_le, Trans.trans, MeasureTheory.lintegral, mul_le_mul_right, LT.lt.le, Iff.mp, HDiv.hDiv, ENNReal.div_lt_iff, Or.inl, Ne, NeZero.ne, Top.top, LT.lt.ne, MeasureTheory.IsFiniteMeasure.measure_univ_lt_top, Eq.mp and 20 more

    134 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma eLpNorm_czRemainder_le {hf : BoundedFiniteSupport f}
    (hX : ¬ GeneralCase f α) (hα : ⨍⁻ x, ‖f x‖ₑ < α) :
    eLpNorm (czRemainder f α) 1 volume ≤ 2 ^ (2 * a + 1) * α * volume (univ : Set X) := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czRemainder

  81. lemma tsum_volume_czBall3_le Part of Lemma 10.2.5, equation (10.2.22) (general case) line 1010 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.22) (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, GeneralCase, LT.lt, OfNat.ofNat, LE.le, tsum, MeasureTheory.Measure, Set, czBall3, SummationFilter.unconditional, HMul.hMul, HDiv.hDiv and 2 more

    Proof uses: Trans.trans, Eq, C10_2_1, Set.preimage, globalMaximalFunction, Real, Set.Ioi, czBall, ENNReal.tsum_le_tsum, id, Eq.mpr, HSMul.hSMul, congrFun', congrArg, ENNReal.tsum_const_smul, smul_le_smul_left, Set.iUnion, Metric.ball, czCenter, czRadius and 64 more

    174 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

    lemma tsum_volume_czBall3_le (hf : BoundedFiniteSupport f)
    (hX : GeneralCase f α) (hα : 0 < α) :
    ∑' i, volume (czBall3 hX i) ≤ 2 ^ (4 * a) / α * eLpNorm f 1 volume := calc
…

    Mentions: BoundedFiniteSupport, GeneralCase, czBall3

  82. lemma volume_univ_le Part of Lemma 10.2.5, equation (10.2.22) (finite case) line 1027 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.22) (finite case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Not, GeneralCase, LT.lt, OfNat.ofNat, LE.le, MeasureTheory.Measure, Set, Set.univ, HMul.hMul, HDiv.hDiv, HPow.hPow and 1 more

    Proof uses: Eq.mpr, Set.ofPred, ENorm.enorm, globalMaximalFunction, Real, C10_2_1, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True, congrArg, funext, eq_true, id and 7 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

    lemma volume_univ_le (hf : BoundedFiniteSupport f) (hX : ¬GeneralCase f α) (hα : 0 < α) :
    volume (univ : Set X) ≤ 2 ^ (2 * a) / α * eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, GeneralCase

  83. lemma tsum_eLpNorm_czRemainder'_le Part of Lemma 10.2.5, equation (10.2.23) (general case) line 1034 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.23) (general case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, GeneralCase, LE.le, tsum, MeasureTheory.eLpNorm, czRemainder', OfNat.ofNat, SummationFilter.unconditional, HMul.hMul

    Proof uses: le_trans, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, czPartition, ENorm.enorm, ENNReal.tsum_le_tsum, id, Eq.mpr, HSMul.hSMul, Eq, congrFun', congrArg, ENNReal.tsum_const_smul, smul_le_smul_left, Set.iUnion, Eq.symm, MeasureTheory.lintegral_iUnion, Eq.trans, ite, Top.top and 22 more

    129 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    lemma tsum_eLpNorm_czRemainder'_le {hf : BoundedFiniteSupport f} (hX : GeneralCase f α) :
    ∑' i, eLpNorm (czRemainder' hX i) 1 volume ≤ 2 * eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czRemainder'

  84. lemma tsum_eLpNorm_czRemainder_le Part of Lemma 10.2.5, equation (10.2.23) (finite case) line 1043 source

    Source documentation

    Part of Lemma 10.2.5, equation (10.2.23) (finite case).

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Not, GeneralCase, LT.lt, MeasureTheory.laverage, ENorm.enorm, LE.le, MeasureTheory.eLpNorm, czRemainder, OfNat.ofNat, HMul.hMul

    Proof uses: Eq.mpr, MeasureTheory.lintegral, id, Eq, congr, congrArg, Eq.trans, ite, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm', ENNReal.toReal, ite_eq_right_of_eq_false, HPow.hPow, Real, HDiv.hDiv, funext, ENNReal.rpow_one, div_self, of_eq_true and 5 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    lemma tsum_eLpNorm_czRemainder_le
    {hf : BoundedFiniteSupport f} (hX : ¬ GeneralCase f α) (hα : ⨍⁻ x, ‖f x‖ₑ < α) :
    eLpNorm (czRemainder f α) 1 volume ≤ 2 * eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, czRemainder

  85. def Ω The set Ω introduced below Lemma 10.2.5 line 1056 source

    Source documentation

    The set Ω introduced below Lemma 10.2.5.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, Set

    Proof uses: dite, GeneralCase, Classical.propDecidable, Set.iUnion, czBall6, Not, Set.univ

    14 instances, coercions and auxiliary constants left out.

    def Ω (α : ℝ≥0∞) : Set X :=
…
  86. lemma czBall3_subset_of_mem_Ω line 1059 source
  87. lemma six_mul_czRadius_le_of_mem_Ω line 1068 source
  88. def α' Auxiliary constant used in the proofs of estimate_good, estimate_bad and distribution_czOperatorBound line 1078 source

    Source documentation

    Auxiliary constant used in the proofs of estimate_good, estimate_bad and distribution_czOperatorBound.

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

    Statement uses: Nat, ENNReal

    Proof uses: HMul.hMul, c10_0_3

    6 instances, coercions and auxiliary constants left out.

    @[no_expose] def α' (α : ℝ≥0∞) : ℝ≥0∞ := c10_0_3 a * α
  89. lemma α'_pos Auxiliary constant used in the proofs of estimate_good, estimate_bad and distribution_czOperatorBound line 1080 source

    Source documentation

    Auxiliary constant used in the proofs of estimate_good, estimate_bad and distribution_czOperatorBound.

    private lemma α'_pos {α : ℝ≥0∞} (hα : 0 < α) : 0 < α' a α :=
…

    Mentions: α'

  90. lemma div_α'_eq line 1083 source
  91. lemma estimate_good Lemma 10.2.6 line 1092 source

    Source documentation

    Lemma 10.2.6

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, MeasureTheory.laverage, HDiv.hDiv, ENorm.enorm, c10_0_3, MeasureTheory.HasBoundedStrongType, czOperator, OfNat.ofNat, C_Ts and 7 more

    Proof uses: dite, Eq, Top.top, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', MeasureTheory.Measure, Nat.AtLeastTwo, ENNReal.top_div_of_lt_top, ENNReal.ofNat_lt_top, MeasureTheory.distibution_top, ENNReal.div_top, MulZeroClass.zero_mul, Not, Ne, Inv.inv, HPow.hPow and 149 more

    261 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

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

    lemma estimate_good (hf : BoundedFiniteSupport f) (hα : ⨍⁻ x, ‖f x‖ₑ / c10_0_3 a < α)
    (hT : HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :
    distribution (czOperator K r (czApproximation f (α' a α))) (α / 2) volume ≤
    C10_2_6 a / α * eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, czOperator, K, C_Ts, czApproximation, α'

  92. abbrev czOperatorBoundSummand line 1144 source
  93. def czOperatorBound The function F defined in Lemma 10.2.7 line 1149 source

    Source documentation

    The function F defined in Lemma 10.2.7.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, GeneralCase, α'

    Proof uses: HMul.hMul, C10_2_7, tsum, HDiv.hDiv, HPow.hPow, Real, Real.toNNReal, OfNat.ofNat, czRadius, NNDist.nndist, czCenter, Inv.inv, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, czBall3, Metric.ball, Dist.dist, SummationFilter.unconditional

    38 instances, coercions and auxiliary constants left out.

    def czOperatorBound (hX : GeneralCase f (α' a α)) (x : X) : ℝ≥0∞ :=
…

    Mentions: GeneralCase, α'

  94. lemma czOperatorBound_eq line 1153 source
  95. def 𝒥₁ line 1157 source
  96. def 𝒥₂ line 1160 source
  97. def 𝒥₃ line 1163 source
  98. lemma union_𝒥 line 1166 source
  99. lemma lemma_10_2_7_bound' Auxiliary bound used to prove lemma_10_2_7_bound line 1176 source

    Source comment

    Auxiliary bound used to prove `lemma_10_2_7_bound`
    private lemma lemma_10_2_7_bound' (hx : x ∈ (Ω f (α' a α))ᶜ) (hX : GeneralCase f (α' a α)) (j : ℕ)
    {g : X → ℂ} (g_aemeas : AEMeasurable g (volume.restrict (czBall3 hX j)))
    (hg : ∫⁻ y in czBall3 hX j, ‖g y‖ₑ ≤ 2 ^ (2 * a + 1) * (α' a α) * volume (czBall3 hX j)) :
    ∫⁻ y in czBall3 hX j, ‖K x y - K x (czCenter hX j)‖ₑ * ‖g y‖ₑ ≤
    czOperatorBoundSummand hX j x := calc
…

    Mentions: Ω, α', GeneralCase, g, czBall3, K, czCenter, czOperatorBoundSummand

  100. lemma lemma_10_2_7_bound Bound used twice in the proof of Lemma 10.2.7 line 1206 source

    Source comment

    Bound used twice in the proof of Lemma 10.2.7
    private lemma lemma_10_2_7_bound (hx : x ∈ (Ω f (α' a α))ᶜ) (hX : GeneralCase f (α' a α)) (j : ℕ)
    {g : X → ℂ} (g_int : IntegrableOn g (czBall3 hX j)) (hg0 : ∫ y in czBall3 hX j, g y = 0)
    (hg : ∫⁻ y in czBall3 hX j, ‖g y‖ₑ ≤ 2 ^ (2 * a + 1) * (α' a α) * volume (czBall3 hX j)) :
    ‖∫ y in czBall3 hX j, K x y * g y‖ₑ ≤ czOperatorBoundSummand hX j x := by
…

    Mentions: Ω, α', GeneralCase, g, czBall3, K, czOperatorBoundSummand

  101. lemma 𝒥₁_bound line 1223 source
  102. lemma tsum_𝒥₁ line 1241 source
  103. def d line 1250 source
  104. lemma integrableOn_d line 1253 source
  105. lemma enorm_d_le line 1258 source
  106. abbrev g₀ line 1279 source
  107. abbrev g line 1283 source
  108. lemma integrableOn_g₀ line 1286 source
  109. lemma lintegral_enorm_g₀_le line 1290 source
  110. lemma integrableOn_g line 1298 source
  111. lemma integral_g line 1302 source
  112. lemma lintegral_enorm_half_g line 1313 source
  113. lemma 𝒥₂_bound The bounds on ‖czOperator K r (czRemainder' hX j) x‖ₑ used for the 𝒥₂ estimate (even though this part of the estimate doesn't require j ∈ 𝒥₂) line 1332 source

    Source comment

    The bounds on `‖czOperator K r (czRemainder' hX j) x‖ₑ` used for the `𝒥₂` estimate (even though this part of the estimate doesn't require j ∈ 𝒥₂).
    private lemma 𝒥₂_bound (hf : BoundedFiniteSupport f) (hα : 0 < α) (hx : x ∈ (Ω f (α' a α))ᶜ)
    (hX : GeneralCase f (α' a α)) {j : ℕ} :
    ‖czOperator K r (czRemainder' hX j) x‖ₑ ≤ 2 * czOperatorBoundSummand hX j x +
      2 ^ (2 * a + 1) * (α' a α) * ∫⁻ y in czBall3 hX j, ‖K x y‖ₑ := calc
…

    Mentions: BoundedFiniteSupport, Ω, α', GeneralCase, czOperator, K, czRemainder', czOperatorBoundSummand, czBall3

  114. def A line 1388 source
  115. lemma A_subset (10.2.52) line 1391 source

    Source comment

    (10.2.52)
    private lemma A_subset (hx : x ∈ (Ω f (α' a α))ᶜ) (hX : GeneralCase f (α' a α)) :
    A r x hX ⊆ Annulus.co x (r / 3) (3 * r) := by
…

    Mentions: Ω, α', GeneralCase, A

  116. lemma sum_volume_restrict_le line 1402 source
  117. lemma tsum_integral_K_le Long calculation toward the end of Lemma 10.2.7 line 1409 source

    Source comment

    Long calculation toward the end of Lemma 10.2.7
    private lemma tsum_integral_K_le (hx : x ∈ (Ω f (α' a α))ᶜ) (hX : GeneralCase f (α' a α)) :
    ∑' (j : 𝒥₂ r x hX), ∫⁻ y in czBall3 hX j, ‖K x y‖ₑ ≤ 2 ^ (a ^ 3 + 10 * a) := calc
…

    Mentions: Ω, α', GeneralCase, 𝒥₂, czBall3, K

  118. lemma tsum_𝒥₂ line 1441 source
  119. lemma tsum_𝒥₃ line 1467 source
  120. lemma czOperator_czRemainder' line 1477 source
  121. lemma czOperator_czRemainder line 1483 source
  122. lemma estimate_bad_partial Lemma 10.2.7 line 1498 source

    Source documentation

    Lemma 10.2.7. Note that hx implies hX, but we keep the superfluous hypothesis to shorten the statement.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, ENNReal, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, MeasureTheory.laverage, HDiv.hDiv, ENorm.enorm, c10_0_3, Membership.mem, Set, Compl.compl and 9 more

    Proof uses: Trans.trans, Eq, tsum, czRemainder', SummationFilter.unconditional, Union.union, Eq.mpr, id, congrArg, pos_of_gt, Eq.refl, enorm_tsum_le_tsum_enorm, Set.univ, Eq.symm, tsum_univ, ENNReal.tsum_union_le, add_zero, add_le_add, Mathlib.Tactic.Ring.of_eq, HPow.hPow and 22 more

    140 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma estimate_bad_partial (hf : BoundedFiniteSupport f) (hr : 0 < r)
    (hα : ⨍⁻ x, ‖f x‖ₑ / c10_0_3 a < α)
    (hx : x ∈ (Ω f (α' a α))ᶜ) (hX : GeneralCase f (α' a α)) :
    ‖czOperator K r (czRemainder f (α' a α)) x‖ₑ ≤ 3 * czOperatorBound hX x + α / 8 := calc
…

    Mentions: BoundedFiniteSupport, Ω, α', GeneralCase, czOperator, K, czRemainder, czOperatorBound

  123. lemma czOperatorBound_inner_le line 1511 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, LE.le, OfNat.ofNat, GeneralCase, α', MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Compl.compl, Set, Ω, HDiv.hDiv, HPow.hPow, Real and 9 more

    Proof uses: Eq.mpr, id, Eq, congrArg, rfl, LT.lt, Or, le_or_gt, congrFun', funext, Real.toNNReal_of_nonpos, ENNReal.zero_div, ENNReal.zero_rpow_of_pos, propext, inv_pos, Nat.cast_pos, LT.lt.trans_le, zero_lt_four, MeasureTheory.lintegral_zero, zero_le and 200 more

    264 instances, coercions and auxiliary constants left out.

    Tactic trace: 95 steps

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

  124. lemma distribution_czOperatorBound Lemma 10.2.8 line 1594 source

    Source documentation

    Lemma 10.2.8

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, ENNReal, LE.le, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, MeasureTheory.laverage, HDiv.hDiv, ENorm.enorm, c10_0_3, GeneralCase, α', MeasureTheory.Measure, Set and 9 more

    Proof uses: Eq, Or, eq_zero_or_pos, False.elim, Eq.mp, False, Eq.symm, Top.top, eq_top_or_lt_top, EmptyCollection.emptyCollection, Eq.mpr, id, congrArg, ENNReal.top_div_of_ne_top, of_eq_true, Not, Eq.trans, True, eq_false, not_false and 162 more

    236 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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

    lemma distribution_czOperatorBound (ha : 4 ≤ a) (hf : BoundedFiniteSupport f)
    (hα : ⨍⁻ x, ‖f x‖ₑ / c10_0_3 a < α) (hX : GeneralCase f (α' a α)) :
    volume ((Ω f (α' a α))ᶜ ∩ czOperatorBound hX ⁻¹' Ioi (α / 8)) ≤
    C10_2_8 a / α * eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, GeneralCase, α', Ω, czOperatorBound

  125. lemma estimate_bad Lemma 10.2.9 line 1649 source

    Source documentation

    Lemma 10.2.9

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, ENNReal, LE.le, OfNat.ofNat, LT.lt, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, MeasureTheory.laverage, HDiv.hDiv, ENorm.enorm, c10_0_3, MeasureTheory.distribution, czOperator and 5 more

    Proof uses: Eq, Or, eq_zero_or_pos, False.elim, Eq.mp, False, eq_false, ENNReal.not_lt_zero, Eq.symm, dite, GeneralCase, Classical.propDecidable, Trans.trans, HAdd.hAdd, HPow.hPow, C10_2_8, tsum, MeasureTheory.Measure, Set, czBall3 and 117 more

    223 instances, coercions and auxiliary constants left out.

    Tactic trace: 56 steps

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

    lemma estimate_bad (ha : 4 ≤ a) (hr : 0 < r)
    (hf : BoundedFiniteSupport f) (hα : ⨍⁻ x, ‖f x‖ₑ / c10_0_3 a < α) :
    distribution (czOperator K r (czRemainder f (α' a α))) (α / 2) volume ≤
    C10_2_9 a / α * eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, czOperator, K, czRemainder, α'

  126. lemma estimate_czOperator Lemma 10.0.3, blueprint form line 1704 source

    Source documentation

    Lemma 10.0.3, blueprint form.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, ENNReal, LE.le, OfNat.ofNat, LT.lt, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, MeasureTheory.HasBoundedStrongType, czOperator, C_Ts, MeasureTheory.distribution, HMul.hMul, HDiv.hDiv and 2 more

    Proof uses: MeasureTheory.laverage, ENorm.enorm, c10_0_3, Or, le_or_gt, Eq, eq_zero_or_pos, funext, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.restrict, Compl.compl, Set, Metric.ball, id, congrArg, czOperator.eq_1, MeasureTheory.integral_eq_zero_of_ae, Filter.EventuallyEq, MeasureTheory.ae and 192 more

    302 instances, coercions and auxiliary constants left out.

    Tactic trace: 88 steps

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

    lemma estimate_czOperator (ha : 4 ≤ a) (hr : 0 < r) (hf : BoundedFiniteSupport f)
    (hT : HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :
    distribution (czOperator K r f) α volume ≤ C10_0_3 a / α * eLpNorm f 1 volume := by
…

    Mentions: BoundedFiniteSupport, czOperator, K, C_Ts

  127. theorem czOperator_weak_1_1 Lemma 10.0.3, formulated differently line 1773 source

    Source documentation

    Lemma 10.0.3, formulated differently. The blueprint version is basically this after unfolding HasBoundedWeakType, wnorm and wnorm'.

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, LT.lt, MeasureTheory.HasBoundedStrongType, czOperator, ENNReal, MeasureTheory.MeasureSpace.volume, C_Ts, MeasureTheory.HasBoundedWeakType, C10_0_3

    Proof uses: BoundedFiniteSupport, And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.wnorm, HMul.hMul, MeasureTheory.eLpNorm, czOperator_aestronglyMeasurable, BoundedFiniteSupport.aestronglyMeasurable, id, Eq.mpr, ite, Eq, Top.top, MeasureTheory.eLpNormEssSup, MeasureTheory.wnorm', ENNReal.toReal, False, congrFun', congrArg, ite_congr and 14 more

    113 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

    theorem czOperator_weak_1_1 (ha : 4 ≤ a) (hr : 0 < r)
    (hT : HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :
    HasBoundedWeakType (czOperator K r) 1 1 volume volume (C10_0_3 a) := fun f hf ↦ by
…

    Mentions: czOperator, K, C_Ts