Miscellaneous definitions. These are mostly the definitions used to state the metric Carleson theorem. We should move them to separate files once we start proving things about them.

def localOscillation {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] (E : Set X) (f g : C(X, 𝕜)) : ℝ

The local oscillation of two functions w.r.t. a set E. This is d_E in the blueprint.

Equations

• localOscillation E f g = ⨆ z ∈ E ×ˢ E, ‖f z.1 - g z.1 - f z.2 + g z.2‖

def localOscillationBall {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] (E : Set X) (f : C(X, 𝕜)) (r : ℝ) : Set C(X, 𝕜)

A ball w.r.t. the distance localOscillation

Equations

• localOscillationBall E f r = {g : C(X, 𝕜) | localOscillation E f g < r}

theorem fact_isCompact_ball {X : Type u_2} [PseudoMetricSpace X] (x : X) (r : ℝ) : Fact (Bornology.IsBounded (Metric.ball x r))

class FunctionDistances (𝕜 : outParam (Type u_3)) (X : Type u) [NormedField 𝕜] [TopologicalSpace X] : Type (max (u + 1) u_3)

A class stating that continuous functions have distances associated to every ball. We use a separate type to conveniently index these functions.

• Θ : Type u
• coeΘ : Θ X → C(X, 𝕜)
• coeΘ_injective : ∀ {f g : Θ X}, (∀ (x : X), (coeΘ f) x = (coeΘ g) x) → f = g
• metric : X → ℝ → PseudoMetricSpace (Θ X)

instance instCoeΘContinuousMap {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [FunctionDistances 𝕜 X] : Coe (Θ X) C(X, 𝕜)

Equations

• instCoeΘContinuousMap = { coe := coeΘ }

instance instFunLikeΘ {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [FunctionDistances 𝕜 X] : FunLike (Θ X) X 𝕜

Equations

• instFunLikeΘ = { coe := fun (f : Θ X) => ⇑(coeΘ f), coe_injective' := ⋯ }

instance instContinuousMapClassΘ {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [FunctionDistances 𝕜 X] : ContinuousMapClass (Θ X) X 𝕜

Equations

• ⋯ = ⋯

def WithFunctionDistance {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [FunctionDistances 𝕜 X] (x : X) (r : ℝ) : Type u_2

Equations

• WithFunctionDistance x r = Θ X

def toWithFunctionDistance {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] {x : X} {r : ℝ} [FunctionDistances 𝕜 X] : Θ X ≃ WithFunctionDistance x r

Equations

• toWithFunctionDistance = Equiv.refl (Θ X)

instance instPseudoMetricSpaceWithFunctionDistance {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] {x : X} {r : ℝ} [d : FunctionDistances 𝕜 X] : PseudoMetricSpace (WithFunctionDistance x r)

Equations

• instPseudoMetricSpaceWithFunctionDistance = FunctionDistances.metric x r

def «termDist_{_,_}» : Lean.ParserDescr

Equations

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

def «termDist_{_,_}».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «termNndist_{_,_}».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def «termNndist_{_,_}» : Lean.ParserDescr

Equations

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

def «termBall_{_,_}» : Lean.ParserDescr

Equations

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

def «termBall_{_,_}».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

class CompatibleFunctions (𝕜 : outParam (Type u_3)) (X : Type u) (A : outParam ℕ) [RCLike 𝕜] [PseudoMetricSpace X] extends FunctionDistances 𝕜 X : Type (max (u + 1) u_3)

A set Θ of (continuous) functions is compatible. A will usually be 2 ^ a.

• Θ : Type u
• coeΘ : Θ X → C(X, 𝕜)
• coeΘ_injective : ∀ {f g : Θ X}, (∀ (x : X), (coeΘ f) x = (coeΘ g) x) → f = g
• metric : X → ℝ → PseudoMetricSpace (Θ X)
• eq_zero : ∃ (o : X), ∀ (f : Θ X), f o = 0
• localOscillation_le_cdist : ∀ {x : X} {r : ℝ} {f g : Θ X}, localOscillation (Metric.ball x r) (coeΘ f) (coeΘ g) ≤ dist f g

  The distance is bounded below by the local oscillation. (1.0.7)

• cdist_mono : ∀ {x₁ x₂ : X} {r₁ r₂ : ℝ} {f g : Θ X}, Metric.ball x₁ r₁ ⊆ Metric.ball x₂ r₂ → dist f g ≤ dist f g

  The distance is monotone in the ball. (1.0.9)

• cdist_le : ∀ {x₁ x₂ : X} {r : ℝ} {f g : Θ X}, dist x₁ x₂ < 2 * r → dist f g ≤ ↑A * dist f g

  The distance of a ball with large radius is bounded above. (1.0.8)

• le_cdist : ∀ {x₁ x₂ : X} {r : ℝ} {f g : Θ X}, Metric.ball x₁ r ⊆ Metric.ball x₂ (↑A * r) → 2 * dist f g ≤ dist f g

  The distance of a ball with large radius is bounded below. (1.0.10)

• ballsCoverBalls : ∀ {x : X} {r R : ℝ}, BallsCoverBalls (WithFunctionDistance x r) (2 * R) R A

  The distance of a ball with large radius is bounded below. (1.0.11)

instance nonempty_Space {𝕜 : Type u_1} {X : Type u_2} {A : ℕ} [RCLike 𝕜] [PseudoMetricSpace X] [CompatibleFunctions 𝕜 X A] : Nonempty X

Equations

• ⋯ = ⋯

instance inhabited_Space {𝕜 : Type u_1} {X : Type u_2} {A : ℕ} [RCLike 𝕜] [PseudoMetricSpace X] [CompatibleFunctions 𝕜 X A] : Inhabited X

Equations

• inhabited_Space = { default := ⋯.some }

theorem dist_congr {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [FunctionDistances 𝕜 X] {x₁ x₂ : X} {r₁ r₂ : ℝ} {f g : Θ X} (e₁ : x₁ = x₂) (e₂ : r₁ = r₂) : dist f g = dist f g

def cancelPt {𝕜 : Type u_1} (X : Type u_2) {A : ℕ} [RCLike 𝕜] [PseudoMetricSpace X] [CompatibleFunctions 𝕜 X A] : X

The point o in the blueprint

Equations

• cancelPt X = ⋯.choose

theorem cancelPt_eq_zero {𝕜 : Type u_1} {X : Type u_2} {A : ℕ} [RCLike 𝕜] [PseudoMetricSpace X] [CompatibleFunctions 𝕜 X A] {f : Θ X} : f (cancelPt X) = 0

def iLipNorm {X : Type u_2} [PseudoMetricSpace X] {𝕜 : Type u_3} [NormedField 𝕜] (ϕ : X → 𝕜) (x₀ : X) (R : ℝ) : ℝ

The inhomogeneous Lipschitz norm on a ball.

Equations

• iLipNorm ϕ x₀ R = (⨆ x ∈ Metric.ball x₀ R, ‖ϕ x‖) + R * ⨆ (x : X), ⨆ (y : X), ⨆ (_ : x ≠ y), ‖ϕ x - ϕ y‖ / dist x y

theorem iLipNorm_nonneg {X : Type u_2} [PseudoMetricSpace X] {𝕜 : Type u_3} [NormedField 𝕜] {ϕ : X → 𝕜} {x₀ : X} {R : ℝ} (hR : 0 ≤ R) : 0 ≤ iLipNorm ϕ x₀ R

class IsCancellative (X : Type u_2) {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] (τ : ℝ) [CompatibleFunctions ℝ X A] : Prop

Θ is τ-cancellative. τ will usually be 1 / a

• norm_integral_exp_le : ∀ {x : X} {r : ℝ} {ϕ : X → ℂ} {K : NNReal}, LipschitzWith K ϕ → tsupport ϕ ⊆ Metric.ball x r → ∀ {f g : Θ X}, ‖∫ (x : X) in Metric.ball x r, Complex.exp (Complex.I * (↑(f x) - ↑(g x))) * ϕ x‖ ≤ ↑A * MeasureTheory.volume.real (Metric.ball x r) * iLipNorm ϕ x r * (1 + dist f g) ^ (-τ)

def Real.vol {X : Type u_3} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] (x y : X) : ℝ

The "volume function" V. Note that we will need to assume IsFiniteMeasureOnCompacts and ProperSpace to actually know that this volume is finite.

Equations

• Real.vol x y = MeasureTheory.volume.real (Metric.ball x (dist x y))

def CZOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] (K : X → X → ℂ) (r : ℝ) (f : X → ℂ) (x : X) : ℂ

The Calderon Zygmund operator T_r in chapter Two-sided Metric Space Carleson

Equations

• CZOperator K r f x = ∫ (y : X) in {y : X | dist x y ∈ Set.Ici r}, K x y * f y

def upperRadius {X : Type u_2} [PseudoMetricSpace X] [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ENNReal

R_Q(θ, x) defined in (1.0.20).

Equations

• upperRadius Q θ x = sSup {r : ENNReal | dist θ (Q x) < 1}

def linearizedNontangentialOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The linearized maximally truncated nontangential Calderon Zygmund operator T_Q^θ

Equations

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

def nontangentialOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The maximally truncated nontangential Calderon Zygmund operator T_*

Equations

• nontangentialOperator K f x = ⨆ (R₁ : ℝ), ⨆ (R₂ : ℝ), ⨆ (_ : R₁ < R₂), ⨆ (x' : X), ⨆ (_ : dist x x' ≤ R₁), ↑‖∫ (y : X) in {y : X | dist x' y ∈ Set.Ioo R₁ R₂}, K x' y * f y‖₊

def linearizedCarlesonOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (Q : X → Θ X) (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The linearized generalized Carleson operator T_Q, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number.

Equations

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

def carlesonOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The generalized Carleson operator T, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number.

Equations

• carlesonOperator K f x = ⨆ (θ : Θ X), linearizedCarlesonOperator (fun (x : X) => θ) K f x

@[reducible, inline]

abbrev defaultA (a : ℕ) : ℕ

This is usually the value of the argument A in DoublingMeasure and CompatibleFunctions

Equations

• defaultA a = 2 ^ a

def defaultD (a : ℕ) : ℕ

Equations

• defaultD a = 2 ^ (100 * a ^ 2)

def defaultκ (a : ℕ) : ℝ

Equations

• defaultκ a = 2 ^ (-10 * ↑a)

def defaultZ (a : ℕ) : ℕ

Equations

• defaultZ a = 2 ^ (12 * a)

def defaultτ (a : ℕ) : ℝ

Equations

• defaultτ a = (↑a)⁻¹

theorem defaultD_pos (a : ℕ) : 0 < ↑(defaultD a)

theorem defaultD_pow_pos (a : ℕ) (z : ℤ) : 0 < ↑(defaultD a) ^ z

theorem mul_defaultD_pow_pos (a : ℕ) {r : ℝ} (hr : 0 < r) (z : ℤ) : 0 < r * ↑(defaultD a) ^ z

def C_K (a : ℝ) : ℝ

The constant used twice in the definition of the Calderon-Zygmund kernel.

Equations

• C_K a = 2 ^ a ^ 3

theorem C_K_pos (a : ℝ) : 0 < C_K a

class IsOneSidedKernel {X : Type u_1} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] (a : outParam ℕ) (K : X → X → ℂ) : Prop

K is a one-sided Calderon-Zygmund kernel In the formalization K x y is defined everywhere, even for x = y. The assumptions on K show that K x x = 0.

• measurable_K : Measurable (Function.uncurry K)
• norm_K_le_vol_inv : ∀ (x y : X), ‖K x y‖ ≤ C_K ↑a / Real.vol x y
• norm_K_sub_le : ∀ {x y y' : X}, 2 * dist y y' ≤ dist x y → ‖K x y - K x y'‖ ≤ (dist y y' / dist x y) ^ (↑a)⁻¹ * (C_K ↑a / Real.vol x y)

theorem MeasureTheory.aestronglyMeasurable_K {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [IsOneSidedKernel a K] : MeasureTheory.AEStronglyMeasurable (Function.uncurry K) MeasureTheory.volume

theorem measurable_K_left {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [IsOneSidedKernel a K] (y : X) : Measurable fun (x : X) => K x y

class IsTwoSidedKernel {X : Type u_1} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] (a : outParam ℕ) (K : X → X → ℂ) extends IsOneSidedKernel a K : Prop

K is a two-sided Calderon-Zygmund kernel In the formalization K x y is defined everywhere, even for x = y. The assumptions on K show that K x x = 0.

• measurable_K : Measurable (Function.uncurry K)
• norm_K_le_vol_inv : ∀ (x y : X), ‖K x y‖ ≤ C_K ↑a / Real.vol x y
• norm_K_sub_le : ∀ {x y y' : X}, 2 * dist y y' ≤ dist x y → ‖K x y - K x y'‖ ≤ (dist y y' / dist x y) ^ (↑a)⁻¹ * (C_K ↑a / Real.vol x y)
• norm_K_sub_le' : ∀ {x x' y : X}, 2 * dist x x' ≤ dist x y → ‖K x y - K x' y‖ ≤ (dist x x' / dist x y) ^ (↑a)⁻¹ * (C_K ↑a / Real.vol x y)

def C_Ts (a : ℝ) : NNReal

Equations

• C_Ts a = 2 ^ a ^ 3

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

Data common through most of chapters 2-9.

• d : MeasureTheory.DoublingMeasure X ↑(defaultA a)
• four_le_a : 4 ≤ a
• cf : CompatibleFunctions ℝ X (defaultA a)
• c : IsCancellative X (defaultτ a)
• hcz : IsOneSidedKernel a K
• hasBoundedStrongType_Tstar : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => (nontangentialOperator K x1 x2).toReal) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)
• 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)
• q_mem_Ioc : q ∈ Set.Ioc 1 2

theorem le_cdist_iterate {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] {x : X} {r : ℝ} (hr : 0 ≤ r) (f g : Θ X) (k : ℕ) : 2 ^ k * dist f g ≤ dist f g

theorem cdist_le_iterate {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] {x : X} {r : ℝ} (hr : 0 < r) (f g : Θ X) (k : ℕ) : dist f g ≤ ↑(defaultA a) ^ k * dist f g

theorem ballsCoverBalls_iterate_nat {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] {x : X} {d r : ℝ} {n : ℕ} : BallsCoverBalls (WithFunctionDistance x d) (2 ^ n * r) r (defaultA a ^ n)

theorem ballsCoverBalls_iterate {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] {x : X} {d R r : ℝ} (hR : 0 < R) (hr : 0 < r) : BallsCoverBalls (WithFunctionDistance x d) R r (defaultA a ^ ⌈Real.logb 2 (R / r)⌉₊)

theorem measurable_Q₂ {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : Measurable fun (p : X × X) => (Q p.1) p.2

theorem aestronglyMeasurable_Q₂ {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : MeasureTheory.AEStronglyMeasurable (fun (p : X × X) => (Q p.1) p.2) MeasureTheory.volume

theorem S_spec (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : ∃ (n : ℕ), ∀ (x : X), -↑n ≤ σ₁ x ∧ σ₂ x ≤ ↑n

theorem twentyfive_le_realD (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 25 ≤ ↑(defaultD a)

theorem eight_le_realD (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 8 ≤ ↑(defaultD a)

theorem five_le_realD (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 5 ≤ ↑(defaultD a)

theorem four_le_realD (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 4 ≤ ↑(defaultD a)

theorem one_le_realD (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 1 ≤ ↑(defaultD a)

def defaultS (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData 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] [PreProofData 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] [PreProofData a q K σ₁ σ₂ F G] : Set.range σ₂ ⊆ Set.Icc (-↑(defaultS X)) ↑(defaultS X)

theorem Icc_σ_subset_Icc_S {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] {x : X} : Set.Icc (σ₁ x) (σ₂ x) ⊆ Set.Icc (-↑(defaultS X)) ↑(defaultS X)

theorem neg_S_mem_or_S_mem {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] [Nonempty X] : -↑(defaultS X) ∈ Set.range σ₁ ∨ ↑(defaultS X) ∈ Set.range σ₂

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

theorem cast_a_pos (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 0 < ↑a

theorem τ_pos (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 0 < defaultτ a

theorem τ_nonneg (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData a q K σ₁ σ₂ F G] : 0 ≤ defaultτ a

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

τ as an element of ℝ≥0.

Equations

• nnτ X = ⟨defaultτ a, ⋯⟩

theorem q_pos (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData 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] [PreProofData a q K σ₁ σ₂ F G] : 0 ≤ q

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

q as an element of ℝ≥0.

Equations

• nnq X = ⟨q, ⋯⟩

theorem nnq_pos (X : Type u_1) {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [PreProofData 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] [PreProofData a q K σ₁ σ₂ F G] : nnq X ∈ Set.Ioc 1 2

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

• d : MeasureTheory.DoublingMeasure X ↑(defaultA a)
• four_le_a : 4 ≤ a
• cf : CompatibleFunctions ℝ X (defaultA a)
• c : IsCancellative X (defaultτ a)
• hcz : IsOneSidedKernel a K
• hasBoundedStrongType_Tstar : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => (nontangentialOperator K x1 x2).toReal) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)
• 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)
• q_mem_Ioc : q ∈ Set.Ioc 1 2
• F_subset : F ⊆ Metric.ball (cancelPt X) (↑(defaultD a) ^ defaultS X / 4)
• G_subset : G ⊆ Metric.ball (cancelPt X) (↑(defaultD a) ^ defaultS X / 4)
• volume_F_pos : 0 < MeasureTheory.volume F
• volume_G_pos : 0 < MeasureTheory.volume G

def ShortVariables.termD : Lean.ParserDescr

Equations

• ShortVariables.termD = Lean.ParserDescr.node `ShortVariables.termD 1024 (Lean.ParserDescr.symbol "D")

def ShortVariables.termκ : Lean.ParserDescr

Equations

• ShortVariables.termκ = Lean.ParserDescr.node `ShortVariables.termκ 1024 (Lean.ParserDescr.symbol "κ")

def ShortVariables.termZ : Lean.ParserDescr

Equations

• ShortVariables.termZ = Lean.ParserDescr.node `ShortVariables.termZ 1024 (Lean.ParserDescr.symbol "Z")

def ShortVariables.termτ : Lean.ParserDescr

Equations

• ShortVariables.termτ = Lean.ParserDescr.node `ShortVariables.termτ 1024 (Lean.ParserDescr.symbol "τ")

def ShortVariables.termO : Lean.ParserDescr

Equations

• ShortVariables.termO = Lean.ParserDescr.node `ShortVariables.termO 1024 (Lean.ParserDescr.symbol "o")

def ShortVariables.termS : Lean.ParserDescr

Equations

• ShortVariables.termS = Lean.ParserDescr.node `ShortVariables.termS 1024 (Lean.ParserDescr.symbol "S")

def ShortVariables.termNnτ : Lean.ParserDescr

Equations

• ShortVariables.termNnτ = Lean.ParserDescr.node `ShortVariables.termNnτ 1024 (Lean.ParserDescr.symbol "nnτ")

def ShortVariables.termNnq : Lean.ParserDescr

Equations

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

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

theorem one_le_D {a : ℕ} : 1 ≤ ↑(defaultD a)

theorem D_nonneg {a : ℕ} : 0 ≤ ↑(defaultD a)

theorem κ_nonneg {a : ℕ} : 0 ≤ defaultκ a

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

def nnD (a : ℕ) : NNReal

D as an element of ℝ≥0.

Equations

• nnD a = ⟨↑(defaultD a), ⋯⟩

def ShortVariables.termNnD : Lean.ParserDescr

Equations

• ShortVariables.termNnD = Lean.ParserDescr.node `ShortVariables.termNnD 1024 (Lean.ParserDescr.symbol "nnD")

def hnorm {X : Type u_1} {a : ℕ} [PseudoMetricSpace X] (ϕ : X → ℂ) (x₀ : X) (R : NNReal) : ENNReal

the L^∞-normalized τ-Hölder norm. Do we use this for other values of τ?

Equations

• hnorm ϕ x₀ R = ⨆ x ∈ Metric.ball x₀ ↑R, ↑‖ϕ x‖₊ + ↑R ^ defaultτ a * ⨆ x ∈ Metric.ball x₀ ↑R, ⨆ y ∈ Metric.ball x₀ ↑R, ⨆ (_ : x ≠ y), ↑‖ϕ x - ϕ y‖₊ / ↑(nndist x y) ^ defaultτ a

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𝓩 : 𝓩 ⊆ Metric.ball f (r * 2 ^ k)) (h2𝓩 : 𝓩.PairwiseDisjoint fun (x : Θ X) => Metric.ball 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𝓩 : 𝓩 ⊆ Metric.ball f (r * 2 ^ k)) (h2𝓩 : 𝓩.PairwiseDisjoint fun (x : Θ X) => Metric.ball x r) : Nat.card ↑𝓩 ≤ C2_1_1 k a