Section 10.2 and Lemma 10.0.3

Question:

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

@[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 maximal_theorem {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] [Nonempty X] : 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 → ℂ} (hf : BoundedFiniteSupport f MeasureTheory.volume) : ∀ᵐ (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)] (ha : 4 ≤ 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 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (hf : BoundedFiniteSupport f MeasureTheory.volume) (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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hf : BoundedFiniteSupport f MeasureTheory.volume) (hX : GeneralCase f α) (i : ℕ) : X

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

Equations

• czCenter ha hf hX i = ⋯.choose i

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

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

Equations

• czRadius ha hf hX i = ⋯.choose i

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

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

theorem iUnion_czBall3 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} : ⋃ (i : ℕ), czBall3 ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} {i : ℕ} : ¬Disjoint (czBall7 ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} {y : X} (hy : α < globalMaximalFunction MeasureTheory.volume 1 f y) : Cardinal.mk ↑{i : ℕ | y ∈ czBall3 ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} {y : X} (hy : α < globalMaximalFunction MeasureTheory.volume 1 f y) : {i : ℕ | y ∈ czBall3 ha hf hX i}.Finite

@[irreducible]

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

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

Equations

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

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

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

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

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

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

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

The function g in Lemma 10.2.5. (both cases)

Equations

• czApproximation ha hf α x = if hX : GeneralCase f α then if hx : ∃ (j : ℕ), x ∈ czPartition ha hf hX j then ⨍ (y : X) in czPartition ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} {x : X} {i : ℕ} (hx : x ∈ czPartition ha hf hX i) : czApproximation ha hf α x = ⨍ (y : X) in czPartition ha hf hX i, f y

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

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

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

The function b_i in Lemma 10.2.5 (general case).

Equations

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

def czRemainder {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {f : X → ℂ} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hf : BoundedFiniteSupport f MeasureTheory.volume) (α : 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 ha hf α x = f x - czApproximation ha hf α x

def tsum_czRemainder' {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hf : BoundedFiniteSupport f MeasureTheory.volume) (hX : GeneralCase f α) (x : X) : ∑ᶠ (i : ℕ), czRemainder' ha hf hX i x = czRemainder ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} : Measurable (czApproximation ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {x : X} : czApproximation ha hf α x + czRemainder ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hα : ⨍⁻ (x : X), ‖f x‖ₑ < α) : ∀ᵐ (x : X), ‖czApproximation ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hX : GeneralCase f α) (hα : 0 < α) : ∀ᵐ (x : X), ‖czApproximation ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hα : 0 < α) : MeasureTheory.eLpNorm (czApproximation ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} (hα : 0 < α) {i : ℕ} : Function.support (czRemainder' ha hf hX i) ⊆ czBall3 ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} (hα : 0 < α) {i : ℕ} : ∫ (x : X), czRemainder' ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hX : ¬GeneralCase f α) (hα : 0 < α) : ∫ (x : X), czRemainder ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} {hX : GeneralCase f α} (hα : 0 < α) {i : ℕ} : MeasureTheory.eLpNorm (czRemainder' ha hf hX i) 1 MeasureTheory.volume ≤ 2 ^ (2 * a + 1) * α * MeasureTheory.volume (czBall3 ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hX : ¬GeneralCase f α) (hα : 0 < α) : MeasureTheory.eLpNorm (czRemainder ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hX : GeneralCase f α) (hα : 0 < α) : ∑' (i : ℕ), MeasureTheory.volume (czBall3 ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hX : GeneralCase f α) (hα : 0 < α) : ∑' (i : ℕ), MeasureTheory.eLpNorm (czRemainder' ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hX : ¬GeneralCase f α) (hα : 0 < α) : MeasureTheory.eLpNorm (czRemainder ha hf α) 1 MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

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

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

@[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))⁻¹

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

The set Ω introduced below Lemma 10.2.5.

Equations

• Ω ha hf α = if hX : GeneralCase f α then ⋃ (i : ℕ), czBall2 ha 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] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) : MeasureTheory.distribution (czOperator K r (czApproximation ha hf α)) (α / 2) MeasureTheory.volume ≤ ↑(C10_2_6 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

Lemma 10.2.6

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

@[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

def czOperatorBound {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hf : BoundedFiniteSupport f MeasureTheory.volume) (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] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) (hx : x ∈ (Ω ha hf α)ᶜ) (hX : GeneralCase f α) : ‖czOperator K r (czRemainder ha hf α) x‖ₑ ≤ 3 * czOperatorBound ha 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)] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) (hX : GeneralCase f α) : MeasureTheory.volume ((Ω ha hf α)ᶜ ∩ czOperatorBound ha hf hX ⁻¹' Set.Ioi (α / 8)) ≤ ↑(C10_2_8 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume

Lemma 10.2.8

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

@[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 estimate_bad {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsTwoSidedKernel a K] {f : X → ℂ} {α : ENNReal} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {hf : BoundedFiniteSupport f MeasureTheory.volume} (hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α) (hX : GeneralCase f α) : MeasureTheory.distribution (czOperator K r (czRemainder ha 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'.