Basic definitions and lemmas

This file contains definitions from Section 2 of the blueprint and used throughout the proof of metric Carleson, as well as results about structures defined in sections 1 and 2 (DoublingMeasure KernelProofData, IsCancellative, FunctionDistances, ...). The constants D, κ, Z from the blueprint are introduce here, and useful inequalities are provided for them (as well as for the constants a and tau).

theorem seven_le_c : 7 ≤ 𝕔

theorem c_le_100 : 𝕔 ≤ 100

def defaultD (a : ℕ) : ℕ

The constant D from (2.0.1).

Equations

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

def nnD (a : ℕ) : NNReal

D as an element of ℝ≥0.

Equations

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

def defaultκ (a : ℕ) : ℝ

The constant κ from (2.0.2).

Equations

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

def defaultZ (a : ℕ) : ℕ

The constant Z from (2.0.3).

Equations

• defaultZ a = 2 ^ (12 * a)

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

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

theorem realD_nonneg (a : ℕ) : 0 ≤ ↑(defaultD a)

theorem one_le_realD (a : ℕ) : 1 ≤ ↑(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

theorem hundred_lt_D {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 100 < defaultD a

theorem hundred_lt_realD {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 100 < ↑(defaultD a)

theorem twentyfive_le_realD {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 25 ≤ ↑(defaultD a)

theorem eight_le_realD {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 8 ≤ ↑(defaultD a)

theorem five_le_realD {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 5 ≤ ↑(defaultD a)

theorem four_le_realD {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 4 ≤ ↑(defaultD a)

theorem one_lt_realD {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 1 < ↑(defaultD a)

theorem a_pos {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 0 < a

theorem cast_a_pos {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 0 < ↑a

theorem τ_pos {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 0 < defaultτ a

theorem τ_nonneg {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 0 ≤ defaultτ a

theorem τ_le_one {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : defaultτ a ≤ 1

def nnτ {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : NNReal

τ as an element of ℝ≥0.

Equations

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

theorem nnτ_pos {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : 0 < nnτ X

@[simp]

theorem nnτ_def {a : ℕ} (X : Type u_1) [PseudoMetricSpace X] {K : X → X → ℂ} [hK : KernelProofData a K] : nnτ X = (defaultτ a).toNNReal

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.termNnD : Lean.ParserDescr

Equations

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

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

theorem κ_le_one {a : ℕ} : defaultκ a ≤ 1

instance MeasureTheory.instProperSpace_carleson {X : Type u_1} {A : NNReal} [PseudoMetricSpace X] [DoublingMeasure X A] : ProperSpace X

instance MeasureTheory.instIsOpenPosMeasureVolume_carleson {X : Type u_1} {A : NNReal} [PseudoMetricSpace X] [DoublingMeasure X A] : volume.IsOpenPosMeasure

@[reducible]

def MeasureTheory.DoublingMeasure.mono {X : Type u_1} {A : NNReal} [PseudoMetricSpace X] [DoublingMeasure X A] {A' : NNReal} (h : A ≤ A') : DoublingMeasure X A'

Monotonicity of doubling measure metric spaces in A.

Equations

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

instance MeasureTheory.InnerProductSpace.DoublingMeasure {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] : MeasureTheory.DoublingMeasure E (2 ^ Module.finrank ℝ E)

Equations

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

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

instance instContinuousMapClassΘ {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [FunctionDistances 𝕜 X] : ContinuousMapClass (Θ X) 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)

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

The ℝ≥0-valued distance function on WithFunctionDistance x r. Preferably use edist

Equations

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

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

The ball with center x and radius r in WithFunctionDistance x r.

Equations

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

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

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 le_localOscillation {𝕜 : Type u_1} {X : Type u_2} {A : ℕ} [RCLike 𝕜] [PseudoMetricSpace X] [CompatibleFunctions 𝕜 X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X} (hy : y ∈ Metric.ball x r) (hz : z ∈ Metric.ball x r) : ‖(coeΘ f) y - (coeΘ g) y - (coeΘ f) z + (coeΘ g) z‖ ≤ (localOscillation (Metric.ball x r) (coeΘ f) (coeΘ g)).toReal

theorem oscillation_le_cdist {𝕜 : Type u_1} {X : Type u_2} {A : ℕ} [RCLike 𝕜] [PseudoMetricSpace X] [CompatibleFunctions 𝕜 X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X} (hy : y ∈ Metric.ball x r) (hz : z ∈ Metric.ball x r) : ‖(coeΘ f) y - (coeΘ g) y - (coeΘ f) z + (coeΘ g) z‖ ≤ dist_{x, r} f g

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_{x₁, r₁} f g = dist_{x₂, r₂} 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

theorem enorm_integral_exp_le {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] [CompatibleFunctions ℝ X A] {τ : ℝ} [IsCancellative X τ] {x : X} {r : ℝ} {φ : X → ℂ} (h2 : Function.support φ ⊆ Metric.ball x r) {f g : Θ X} : ‖∫ (x : X), Complex.exp (Complex.I * (↑(f x) - ↑(g x))) * φ x‖ₑ ≤ ↑A * MeasureTheory.volume (Metric.ball x r) * iLipENorm φ x r * (1 + edist_{x, r} f g) ^ (-τ)

theorem isCancellative_of_norm_integral_exp_le {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] (τ : ℝ) [CompatibleFunctions ℝ X A] (h : ∀ {x : X} {r : ℝ} {φ : X → ℂ}, 0 < r → iLipENorm φ x r ≠ ⊤ → Function.support φ ⊆ 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) * ↑(iLipNNNorm φ x r) * (1 + dist_{x, r} f g) ^ (-τ)) : IsCancellative X τ

Constructor of IsCancellative in terms of real norms instead of extended reals.

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

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

Equations

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

theorem measurable_vol {X : Type u_3} [PseudoMetricSpace X] [SecondCountableTopology X] [MeasureTheory.MeasureSpace X] [OpensMeasurableSpace X] [MeasureTheory.SFinite MeasureTheory.volume] : Measurable (Function.uncurry vol)

theorem measurable_vol₁ {X : Type u_3} [PseudoMetricSpace X] [SecondCountableTopology X] [MeasureTheory.MeasureSpace X] [OpensMeasurableSpace X] [MeasureTheory.SFinite MeasureTheory.volume] {y : X} : Measurable fun (x : X) => vol x y

theorem Real.vol_def {X : Type u_3} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] {x y : X} : Real.vol x y = (vol x y).toReal

theorem ofReal_vol {X : Type u_3} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {x y : X} : ENNReal.ofReal (Real.vol x y) = vol x y

theorem le_upperRadius {X : Type u_2} [PseudoMetricSpace X] [FunctionDistances ℝ X] {Q : X → Θ X} {θ : Θ X} {x : X} {r : ℝ} (hr : dist_{x, r} θ (Q x) < 1) : ENNReal.ofReal r ≤ upperRadius Q θ x

theorem carlesonOperator_const_smul {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (z : ℂ) : carlesonOperator (z • K) f = ‖z‖ₑ • carlesonOperator K f

theorem nontangentialOperator_const_smul {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] (z : ℂ) {K : X → X → ℂ} : nontangentialOperator (z • K) = ‖z‖ₑ • nontangentialOperator K

theorem carlesonOperator_const_smul' {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [hXA : MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (z : ℂ) : carlesonOperator K (z • f) = ‖z‖ₑ • carlesonOperator K f

theorem C_K_pos {a : ℝ} : 0 < C_K a

theorem C_K_pos_real {a : ℝ} : 0 < ↑(C_K a)

theorem isOneSidedKernel_const_smul {X : Type u_1} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] {a : ℕ} {K : X → X → ℂ} [IsOneSidedKernel a K] {r : ℝ} (hr : |r| ≤ 1) : IsOneSidedKernel a (r • K)

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

theorem MeasureTheory.aestronglyMeasurable_K {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureSpace X] [IsOneSidedKernel a K] : AEStronglyMeasurable (Function.uncurry K) 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

theorem measurable_K_right {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [IsOneSidedKernel a K] (x : X) : Measurable (K x)

theorem enorm_K_le_vol_inv {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [IsOneSidedKernel a K] (x y : X) : ‖K x y‖ₑ ≤ ↑(C_K ↑a) / vol x y

theorem enorm_K_le_ball_complement {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [IsOneSidedKernel a K] {r : ℝ} {x y : X} (hy : y ∈ (Metric.ball x r)ᶜ) : ‖K x y‖ₑ ≤ ↑(C_K ↑a) / MeasureTheory.volume (Metric.ball x r)

theorem enorm_K_le_ball_complement' {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [MeasureTheory.volume.IsOpenPosMeasure] [IsOneSidedKernel a K] {r : ℝ} (hr : 0 < r) {x y : X} (hy : y ∈ (Metric.ball x r)ᶜ) : ‖K x y‖ₑ ≤ ↑(↑(C_K ↑a) / MeasureTheory.volume (Metric.ball x r)).toNNReal

theorem enorm_K_sub_le {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [IsOneSidedKernel a K] {x y y' : X} (h : 2 * dist y y' ≤ dist x y) : ‖K x y - K x y'‖ₑ ≤ (edist y y' / edist x y) ^ (↑a)⁻¹ * (↑(C_K ↑a) / vol x y)

theorem integrableOn_K_mul {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [MeasureTheory.volume.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [ProperSpace X] [IsOneSidedKernel a K] {f : X → ℂ} {s : Set X} (hf : MeasureTheory.IntegrableOn f s MeasureTheory.volume) (x : X) {r : ℝ} (hr : 0 < r) (hs : s ⊆ (Metric.ball x r)ᶜ) : MeasureTheory.IntegrableOn (K x * f) s MeasureTheory.volume

theorem integrableOn_K_Icc {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] [MeasureTheory.volume.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [ProperSpace X] [IsOneSidedKernel a K] {x : X} {r R : ℝ} (hr : r > 0) : MeasureTheory.IntegrableOn (K x) {y : X | dist x y ∈ Set.Icc r R} MeasureTheory.volume

theorem le_cdist_iterate {X : Type u_1} {a : ℕ} [PseudoMetricSpace X] [CompatibleFunctions ℝ X (defaultA a)] {x : X} {r : ℝ} (hr : 0 ≤ r) (f g : Θ X) (k : ℕ) : 2 ^ k * dist_{x, r} f g ≤ dist_{x, ↑(defaultA a) ^ k * r} f g

theorem cdist_le_iterate {X : Type u_1} {a : ℕ} [PseudoMetricSpace X] [CompatibleFunctions ℝ X (defaultA a)] {x : X} {r : ℝ} (hr : 0 < r) (f g : Θ X) (k : ℕ) : dist_{x, 2 ^ k * r} f g ≤ ↑(defaultA a) ^ k * dist_{x, r} f g

theorem cdist_le_mul_cdist {X : Type u_1} {a : ℕ} [PseudoMetricSpace X] [CompatibleFunctions ℝ X (defaultA a)] {x x' : X} {r r' : ℝ} (hr : 0 < r) (hr' : 0 < r') (f g : Θ X) : dist_{x', r'} f g ≤ ↑(As (↑(defaultA a)) ((r' + dist x' x) / r)) * dist_{x, r} f g

theorem ballsCoverBalls_iterate_nat {X : Type u_1} {a : ℕ} [PseudoMetricSpace X] [CompatibleFunctions ℝ X (defaultA a)] {x : X} {d r : ℝ} {n : ℕ} : BallsCoverBalls (WithFunctionDistance x d) (2 ^ n * r) r (defaultA a ^ n)

theorem ballsCoverBalls_iterate {X : Type u_1} {a : ℕ} [PseudoMetricSpace X] [CompatibleFunctions ℝ X (defaultA a)] {x : X} {d R 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 : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} : Measurable fun (p : X × X) => (Q p.1) p.2

theorem stronglyMeasurable_Q₂ {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} : MeasureTheory.StronglyMeasurable fun (p : X × X) => (Q p.1) p.2

theorem aestronglyMeasurable_Q₂ {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} : MeasureTheory.AEStronglyMeasurable (fun (p : X × X) => (Q p.1) p.2) MeasureTheory.volume

theorem measurable_Q₁ {X : Type u_1} {a : ℕ} {K : X → X → ℂ} [PseudoMetricSpace X] [KernelProofData a K] {Q : MeasureTheory.SimpleFunc X (Θ X)} (x : X) : Measurable ⇑(Q x)