ProofData. #

This file introduces the class ProofData, used to bundle data common through most of chapters 2-7 (except 3), and provides API for it.

source

class ProofData {X : Type u_1} (a : outParam ℕ) (q : outParam ℝ) (K : outParam (X → X → ℂ)) (σ₁ σ₂ : outParam (X → ℤ)) (F G : outParam (Set X)) [PseudoMetricSpace X] extends KernelProofData a K :

Type (u_1 + 1)

Data common through most of chapters 2-7 (except 3).

d : MeasureTheory.DoublingMeasure X ↑(defaultA a)
four_le_a : 4 ≤ a
cf : CompatibleFunctions ℝ X (defaultA a)
hcz : IsOneSidedKernel a K
c : IsCancellative X (defaultτ a)
q_mem_Ioc : q ∈ Set.Ioc 1 2
isBounded_F : Bornology.IsBounded F
isBounded_G : Bornology.IsBounded G
measurableSet_F : MeasurableSet F
measurableSet_G : MeasurableSet G
measurable_σ₁ : Measurable σ₁
measurable_σ₂ : Measurable σ₂
finite_range_σ₁ : Finite ↑(Set.range σ₁)
finite_range_σ₂ : Finite ↑(Set.range σ₂)
σ₁_le_σ₂ : σ₁ ≤ σ₂
Q : MeasureTheory.SimpleFunc X (Θ X)
BST_T_Q (θ : Θ X) : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => linearizedNontangentialOperator (⇑Q) θ K x1 x2) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)

Instances

source

theorem S_spec (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

∃ (n : ℕ), (∀ (x : X), -↑n ≤ σ₁ x ∧ σ₂ x ≤ ↑n) ∧ F ⊆ Metric.ball (cancelPt X) (↑(defaultD a) ^ n / 4) ∧ G ⊆ Metric.ball (cancelPt X) (↑(defaultD a) ^ n / 4) ∧ 0 < n

source

def defaultS (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

ℕ

Equations

defaultS X = Nat.find ⋯

Instances For

source

theorem range_σ₁_subset {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

Set.range σ₁ ⊆ Set.Icc (-↑(defaultS X)) ↑(defaultS X)

source

theorem range_σ₂_subset {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

Set.range σ₂ ⊆ Set.Icc (-↑(defaultS X)) ↑(defaultS X)

source

theorem F_subset {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

F ⊆ Metric.ball (cancelPt X) (↑(defaultD a) ^ defaultS X / 4)

source

theorem G_subset {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

G ⊆ Metric.ball (cancelPt X) (↑(defaultD a) ^ defaultS X / 4)

source

theorem defaultS_pos {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

0 < defaultS X

source

theorem Icc_σ_subset_Icc_S {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x : X} :

Set.Icc (σ₁ x) (σ₂ x) ⊆ Set.Icc (-↑(defaultS X)) ↑(defaultS X)

source

theorem one_lt_q (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

1 < q

source

theorem q_le_two (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

q ≤ 2

source

theorem q_pos (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

0 < q

source

theorem q_nonneg (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

0 ≤ q

source

theorem inv_q_sub_half_nonneg (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

0 ≤ q⁻¹ - 2⁻¹

source

theorem inv_q_mem_Ico (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

q⁻¹ ∈ Set.Ico 2⁻¹ 1

source

def nnq (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

NNReal

q as an element of ℝ≥0.

Equations

nnq X = ⟨q, ⋯⟩

Instances For

source

theorem one_lt_nnq (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

1 < nnq X

source

theorem nnq_le_two (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

nnq X ≤ 2

source

theorem nnq_pos (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

0 < nnq X

source

theorem nnq_mem_Ioc (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

nnq X ∈ Set.Ioc 1 2

source

def ShortVariables.termNnq :

Lean.ParserDescr

Equations

ShortVariables.termNnq = Lean.ParserDescr.node `ShortVariables.termNnq 1024 (Lean.ParserDescr.symbol "nnq")

Instances For

source

theorem two_le_κZ {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

2 ≤ defaultκ a * ↑(defaultZ a)

Used in third_exception (Lemma 5.2.10).

source

theorem DκZ_le_two_rpow_100 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

↑(defaultD a) ^ (-defaultκ a * ↑(defaultZ a)) ≤ 2 ^ (-100)

Used in third_exception (Lemma 5.2.10).

source

theorem four_le_Z {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

4 ≤ defaultZ a

source

theorem volume_F_lt_top {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

MeasureTheory.volume F < ⊤

source

theorem volume_F_ne_top {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

MeasureTheory.volume F ≠ ⊤

source

theorem volume_G_lt_top {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

MeasureTheory.volume G < ⊤

source

theorem volume_G_ne_top {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :

MeasureTheory.volume G ≠ ⊤

Lemma 2.1.1

source

def C2_1_1 (k a : ℕ) :

ℕ

Equations

C2_1_1 k a = 2 ^ (k * a)

Instances For

source

theorem Θ.finite_and_mk_le_of_le_dist {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x₀ : X} {r R : ℝ} {f : Θ X} {k : ℕ} {𝓩 : Set (Θ X)} (h𝓩 : 𝓩 ⊆ ball_{x₀, R} f (r * 2 ^ k)) (h2𝓩 : 𝓩.PairwiseDisjoint fun (x : Θ X) => ball_{x₀, R} x r) :

𝓩.Finite ∧ Cardinal.mk ↑𝓩 ≤ ↑(C2_1_1 k a)

source

theorem Θ.card_le_of_le_dist {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x₀ : X} {r R : ℝ} {f : Θ X} {k : ℕ} {𝓩 : Set (Θ X)} (h𝓩 : 𝓩 ⊆ ball_{x₀, R} f (r * 2 ^ k)) (h2𝓩 : 𝓩.PairwiseDisjoint fun (x : Θ X) => ball_{x₀, R} x r) :

Nat.card ↑𝓩 ≤ C2_1_1 k a

Documentation

Carleson.ProofData

ProofData. #