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.

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)

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

noncomputable 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 ⋯

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)

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)

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)

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)

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

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)

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

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

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

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

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⁻¹

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

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, ⋯⟩

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

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

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

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

def ShortVariables.termNnq : Lean.ParserDescr

Equations

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

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).

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).

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

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 < ⊤

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 ≠ ⊤

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 < ⊤

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

def C2_1_1 (k a : ℕ) : ℕ

Equations

• C2_1_1 k a = 2 ^ (k * a)

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)

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