Section 10.2 and Lemma 10.0.3

Question:

@[irreducible]

def C10_2_1 (a : ℕ) : NNReal

The constant used in nontangential_from_simple. I(F) think the constant needs to be fixed in the blueprint.

Equations

• C10_2_1 a = 2 ^ (4 * a)

theorem C10_2_1_def (a : ℕ) : C10_2_1 a = 2 ^ (4 * a)

theorem maximal_theorem {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) : MeasureTheory.HasBoundedWeakType (globalMaximalFunction MeasureTheory.volume 1) 1 1 MeasureTheory.volume MeasureTheory.volume (C10_2_1 a)

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

theorem lebesgue_differentiation {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (h2f : MeasureTheory.volume (Function.support f) < ⊤) : ∀ᵐ (x : X), ∃ (c : ℕ → X) (r : ℕ → ℝ), Filter.Tendsto (fun (i : ℕ) => ⨍ (y : X) in Metric.ball (c i) (r i), f y) Filter.atTop (nhds (f x)) ∧ Filter.Tendsto r Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) ∧ ∀ (i : ℕ), x ∈ Metric.ball (c i) (r i)

Lemma 10.2.2. Should be an easy consequence of VitaliFamily.ae_tendsto_average.

Lemma 10.2.3 is in Mathlib: Pairwise.countable_of_isOpen_disjoint.

theorem ball_covering {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {O : Set X} (hO : IsOpen O ∧ O ≠ Set.univ) : ∃ (c : ℕ → X) (r : ℕ → ℝ), (Set.univ.PairwiseDisjoint fun (i : ℕ) => Metric.closedBall (c i) (r i)) ∧ ⋃ (i : ℕ), Metric.ball (c i) (3 * r i) = O ∧ (∀ (i : ℕ), ¬Disjoint (Metric.ball (c i) (7 * r i)) Oᶜ) ∧ ∀ x ∈ O, Cardinal.mk ↑{i : ℕ | x ∈ Metric.ball (c i) (3 * r i)} ≤ ↑(2 ^ (6 * a))

Lemma 10.2.4 This is very similar to Vitali.exists_disjoint_subfamily_covering_enlargement. Can we use that (or adapt it so that we can use it)?

Lemma 10.2.5

Lemma 10.2.5 has an annoying case distinction between the case E_α ≠ X (general case) and E_α = X (finite case). It isn't easy to get rid of this case distinction.

In the formalization we state most properties of Lemma 10.2.5 twice, once for each case (in some cases the condition is vacuous in the finite case, and then we omit it)

We could have tried harder to uniformize the cases, but in the finite case there is really only set B*_j, and in the general case it is convenient to index B*_j by the natural numbers.

def BoundedFiniteSupport {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] (f : X → ℂ) : Prop

An auxillary definition bundling the properties of Lemma 10.2.5 so that we don't have to write this every time. Slightly weaker than BoundedCompactSupport.

Equations

• BoundedFiniteSupport f = (Measurable f ∧ MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤ ∧ MeasureTheory.volume (Function.support f) < ⊤)

def GeneralCase {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] (f : X → ℂ) (α : ENNReal) : Prop

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

Equations

• GeneralCase f α = ∃ (x : X), α < globalMaximalFunction MeasureTheory.volume 1 f x

theorem volume_lt_of_not_GeneralCase {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (h : ¬GeneralCase f α) : MeasureTheory.volume Set.univ < ⊤

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

theorem isOpen_MB_preimage_Ioi {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) : IsOpen (globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α) ∧ globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α ≠ Set.univ

def czCenter {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) : X

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

Equations

• czCenter hf hX i = ⋯.choose i

def czRadius {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) : ℝ

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

Equations

• czRadius hf hX i = ⋯.choose i

@[reducible, inline]

abbrev czBall {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) : Set X

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

Equations

• czBall hf hX i = Metric.ball (czCenter hf hX i) (czRadius hf hX i)

@[reducible, inline]

abbrev czBall2 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) : Set X

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

Equations

• czBall2 hf hX i = Metric.ball (czCenter hf hX i) (2 * czRadius hf hX i)

@[reducible, inline]

abbrev czBall3 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) : Set X

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

Equations

• czBall3 hf hX i = Metric.ball (czCenter hf hX i) (3 * czRadius hf hX i)

@[reducible, inline]

abbrev czBall7 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) : Set X

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

Equations

• czBall7 hf hX i = Metric.ball (czCenter hf hX i) (7 * czRadius hf hX i)

theorem czBall_pairwiseDisjoint {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} : Set.univ.PairwiseDisjoint fun (i : ℕ) => Metric.closedBall (czCenter hf hX i) (czRadius hf hX i)

theorem iUnion_czBall3 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} : ⋃ (i : ℕ), czBall3 hf hX i = globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α

theorem not_disjoint_czBall7 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} {i : ℕ} : ¬Disjoint (czBall7 hf hX i) (globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α)ᶜ

theorem cardinalMk_czBall3_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} {y : X} (hy : α < globalMaximalFunction MeasureTheory.volume 1 f y) : Cardinal.mk ↑{i : ℕ | y ∈ czBall3 hf hX i} ≤ ↑(2 ^ (6 * a))

Part of Lemma 10.2.5 (general case).

theorem mem_czBall3_finite {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} {y : X} (hy : α < globalMaximalFunction MeasureTheory.volume 1 f y) : {i : ℕ | y ∈ czBall3 hf hX i}.Finite

@[irreducible]

def czPartition {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) : Set X

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

Equations

• czPartition hf hX i = czBall3 hf hX i \ ((⋃ (j : ℕ), ⋃ (_ : j < i), czPartition hf hX j) ∪ ⋃ (j : ℕ), ⋃ (_ : j > i), czBall hf hX i)

theorem czBall_subset_czPartition {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} {i : ℕ} : czBall hf hX i ⊆ czPartition hf hX i

theorem czPartition_subset_czBall3 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} {i : ℕ} : czPartition hf hX i ⊆ czBall3 hf hX i

theorem czPartition_pairwiseDisjoint {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} : Set.univ.PairwiseDisjoint fun (i : ℕ) => czPartition hf hX i

theorem czPartition_pairwiseDisjoint' {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} {x : X} {i j : ℕ} (hi : x ∈ czPartition hf hX i) (hj : x ∈ czPartition hf hX j) : i = j

theorem iUnion_czPartition {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} : ⋃ (i : ℕ), czPartition hf hX i = globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α

def czApproximation {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} (hf : BoundedFiniteSupport f) (α : ENNReal) (x : X) : ℂ

The function g in Lemma 10.2.5. (both cases)

Equations

• czApproximation hf α x = if hX : GeneralCase f α then if hx : ∃ (j : ℕ), x ∈ czPartition hf hX j then ⨍ (y : X) in czPartition hf hX hx.choose, f y else f x else ⨍ (y : X), f y

theorem czApproximation_def_of_mem {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} {x : X} {i : ℕ} (hx : x ∈ czPartition hf hX i) : czApproximation hf α x = ⨍ (y : X) in czPartition hf hX i, f y

theorem czApproximation_def_of_nmem {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {x : X} (hX : GeneralCase f α) (hx : x ∉ globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α) : czApproximation hf α x = f x

theorem czApproximation_def_of_volume_lt {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {x : X} (hX : ¬GeneralCase f α) : czApproximation hf α x = ⨍ (y : X), f y

def czRemainder' {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (i : ℕ) (x : X) : ℂ

The function b_i in Lemma 10.2.5 (general case).

Equations

• czRemainder' hf hX i x = (czPartition hf hX i).indicator (f - czApproximation hf α) x

def czRemainder {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} (hf : BoundedFiniteSupport f) (α : ENNReal) (x : X) : ℂ

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.

Equations

• czRemainder hf α x = f x - czApproximation hf α x

def tsum_czRemainder' {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (x : X) : ∑ᶠ (i : ℕ), czRemainder' hf hX i x = czRemainder hf α x

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

Equations

• ⋯ = ⋯

theorem measurable_czApproximation {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} : Measurable (czApproximation hf α)

Part of Lemma 10.2.5 (both cases).

theorem czApproximation_add_czRemainder {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {x : X} : czApproximation hf α x + czRemainder hf α x = f x

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

theorem norm_czApproximation_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hα : ⨍⁻ (x : X), ‖f x‖ₑ < α) : ∀ᵐ (x : X), ‖czApproximation hf α x‖ₑ ≤ 2 ^ (3 * a) * α

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

theorem norm_czApproximation_le_infinite {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hX : GeneralCase f α) (hα : 0 < α) : ∀ᵐ (x : X), ‖czApproximation hf α x‖ₑ ≤ 2 ^ (3 * a) * α

Equation (10.2.17) specialized to the general case.

theorem eLpNorm_czApproximation_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hα : 0 < α) : MeasureTheory.eLpNorm (czApproximation hf α) 1 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 1 MeasureTheory.volume

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

theorem support_czRemainder'_subset {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} (hα : 0 < α) {i : ℕ} : Function.support (czRemainder' hf hX i) ⊆ czBall3 hf hX i

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

theorem integral_czRemainder' {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} (hα : 0 < α) {i : ℕ} : ∫ (x : X), czRemainder' hf hX i x = 0

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

theorem integral_czRemainder {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hX : ¬GeneralCase f α) (hα : 0 < α) : ∫ (x : X), czRemainder hf α x = 0

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

theorem eLpNorm_czRemainder'_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} {hX : GeneralCase f α} (hα : 0 < α) {i : ℕ} : MeasureTheory.eLpNorm (czRemainder' hf hX i) 1 MeasureTheory.volume ≤ 2 ^ (2 * a + 1) * α * MeasureTheory.volume (czBall3 hf hX i)

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

theorem eLpNorm_czRemainder_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hX : ¬GeneralCase f α) (hα : 0 < α) : MeasureTheory.eLpNorm (czRemainder hf α) 1 MeasureTheory.volume ≤ 2 ^ (2 * a + 1) * α * MeasureTheory.volume Set.univ

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

theorem tsum_volume_czBall3_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hX : GeneralCase f α) (hα : 0 < α) : ∑' (i : ℕ), MeasureTheory.volume (czBall3 hf hX i) ≤ 2 ^ (4 * a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

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

theorem volume_univ_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hX : ¬GeneralCase f α) (hα : 0 < α) : MeasureTheory.volume Set.univ ≤ 2 ^ (4 * a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

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

theorem tsum_eLpNorm_czRemainder'_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hX : GeneralCase f α) (hα : 0 < α) : ∑' (i : ℕ), MeasureTheory.eLpNorm (czRemainder' hf hX i) 1 MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

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

theorem tsum_eLpNorm_czRemainder_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hX : ¬GeneralCase f α) (hα : 0 < α) : MeasureTheory.eLpNorm (czRemainder hf α) 1 MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

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

@[irreducible]

def c10_0_3 (a : ℕ) : NNReal

The constant c introduced below Lemma 10.2.5.

Equations

• c10_0_3 a = (2 ^ (a ^ 3 + 12 * a + 4))⁻¹

theorem c10_0_3_def (a : ℕ) : c10_0_3 a = (2 ^ (a ^ 3 + 12 * a + 4))⁻¹

def Ω {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} (hf : BoundedFiniteSupport f) (α : ENNReal) : Set X

The set Ω introduced below Lemma 10.2.5.

Equations

• Ω hf α = if hX : GeneralCase f α then ⋃ (i : ℕ), czBall2 hf hX i else Set.univ

theorem C10_2_6_def (a : ℕ) : C10_2_6 a = 2 ^ (2 * a ^ 3 + 3 * a + 2) * c10_0_3 a

@[irreducible]

def C10_2_6 (a : ℕ) : NNReal

The constant used in estimate_good.

Equations

• C10_2_6 a = 2 ^ (2 * a ^ 3 + 3 * a + 2) * c10_0_3 a

theorem estimate_good {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) : MeasureTheory.distribution (czOperator K r (czApproximation hf α)) (α / 2) MeasureTheory.volume ≤ ↑(C10_2_6 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

Lemma 10.2.6

@[irreducible]

def C10_2_7 (a : ℕ) : NNReal

The constant used in czOperatorBound.

Equations

• C10_2_7 a = 2 ^ (a ^ 3 + 2 * a + 1) * c10_0_3 a

theorem C10_2_7_def (a : ℕ) : C10_2_7 a = 2 ^ (a ^ 3 + 2 * a + 1) * c10_0_3 a

def czOperatorBound {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} (hf : BoundedFiniteSupport f) (hX : GeneralCase f α) (x : X) : ENNReal

The function F defined in Lemma 10.2.7.

Equations

• One or more equations did not get rendered due to their size.

theorem estimate_bad_partial {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} {x : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) (hx : x ∈ (Ω hf α)ᶜ) (hX : GeneralCase f α) : ‖czOperator K r (czRemainder hf α) x‖ₑ ≤ 3 * czOperatorBound hf hX x + α / 8

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

theorem C10_2_8_def (a : ℕ) : C10_2_8 a = 2 ^ (a ^ 3 + 9 * a + 4)

@[irreducible]

def C10_2_8 (a : ℕ) : NNReal

The constant used in distribution_czOperatorBound.

Equations

• C10_2_8 a = 2 ^ (a ^ 3 + 9 * a + 4)

theorem distribution_czOperatorBound {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) (hX : GeneralCase f α) : MeasureTheory.volume ((Ω hf α)ᶜ ∩ czOperatorBound hf hX ⁻¹' Set.Ioi (α / 8)) ≤ ↑(C10_2_8 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

Lemma 10.2.8

@[irreducible]

def C10_2_9 (a : ℕ) : NNReal

The constant used in estimate_bad.

Equations

• C10_2_9 a = 2 ^ (5 * a) / c10_0_3 a + 2 ^ (a ^ 3 + 9 * a + 4)

theorem C10_2_9_def (a : ℕ) : C10_2_9 a = 2 ^ (5 * a) / c10_0_3 a + 2 ^ (a ^ 3 + 9 * a + 4)

theorem estimate_bad {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] {f : X → ℂ} {α : ENNReal} {hf : BoundedFiniteSupport f} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) (hX : GeneralCase f α) : MeasureTheory.distribution (czOperator K r (czRemainder hf α)) (α / 2) MeasureTheory.volume ≤ ↑(C10_2_9 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

Lemma 10.2.9

theorem C10_0_3_def (a : ℕ) : C10_0_3 a = 2 ^ (a ^ 3 + 19 * a)

@[irreducible]

def C10_0_3 (a : ℕ) : NNReal

The constant used in czoperator_weak_1_1.

Equations

• C10_0_3 a = 2 ^ (a ^ 3 + 19 * a)

theorem czoperator_weak_1_1 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hr : 0 < r) (hT : MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) : MeasureTheory.HasBoundedWeakType (czOperator K r) 1 1 MeasureTheory.volume MeasureTheory.volume (C10_0_3 a)

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