Section 10.2 and Lemma 10.0.3

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

@[irreducible]

def C10_2_1 (a : ℕ) : NNReal

The constant used in nontangential_from_simple.

Equations

• C10_2_1 a = 2 ^ (2 * 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'`.

@[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 C10_0_3_def (a : ℕ) : 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) (hT : ∃ r > 0, 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'`.