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, ENNReal.ofReal ‖f z.1 - g z.1 - f z.2 + g z.2‖
Instances For
def
localOscillationBall
{𝕜 : Type u_1}
{X : Type u_2}
[RCLike 𝕜]
[PseudoMetricSpace X]
(E : Set X)
(f : C(X, 𝕜))
(r : ℝ)
:
A ball w.r.t. the distance localOscillation
Equations
- localOscillationBall E f r = {g : C(X, 𝕜) | localOscillation E f g < ENNReal.ofReal r}
Instances For
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
Instances
instance
instCoeΘContinuousMap
{𝕜 : Type u_1}
{X : Type u_2}
[RCLike 𝕜]
[PseudoMetricSpace X]
[FunctionDistances 𝕜 X]
:
Equations
- instCoeΘContinuousMap = { coe := coeΘ }
instance
instFunLikeΘ
{𝕜 : Type u_1}
{X : Type u_2}
[RCLike 𝕜]
[PseudoMetricSpace X]
[FunctionDistances 𝕜 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 𝕜
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
Instances For
def
toWithFunctionDistance
{𝕜 : Type u_1}
{X : Type u_2}
[RCLike 𝕜]
[PseudoMetricSpace X]
{x : X}
{r : ℝ}
[FunctionDistances 𝕜 X]
:
Θ X ≃ WithFunctionDistance x r
Equations
Instances For
instance
instPseudoMetricSpaceWithFunctionDistance
{𝕜 : Type u_1}
{X : Type u_2}
[RCLike 𝕜]
[PseudoMetricSpace X]
{x : X}
{r : ℝ}
[d : FunctionDistances 𝕜 X]
:
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty printer defined by notation3 command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
- localOscillation_le_cdist {x : X} {r : ℝ} {f g : Θ X} : localOscillation (Metric.ball x r) (coeΘ f) (coeΘ g) ≤ ENNReal.ofReal (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} (h : Metric.ball x₁ r₁ ⊆ Metric.ball x₂ r₂) : dist f g ≤ dist f g
The distance is monotone in the ball. (1.0.9)
The distance of a ball with large radius is bounded above. (1.0.8)
- le_cdist {x₁ x₂ : X} {r : ℝ} {f g : Θ X} (h1 : 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)
The distance of a ball with large radius is bounded below. (1.0.11)
Instances
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]
:
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)
:
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)
:
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₂)
:
def
cancelPt
{𝕜 : Type u_1}
(X : Type u_2)
{A : ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[CompatibleFunctions 𝕜 X A]
:
X
The point o in the blueprint
Instances For
theorem
cancelPt_eq_zero
{𝕜 : Type u_1}
{X : Type u_2}
{A : ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[CompatibleFunctions 𝕜 X A]
{f : Θ X}
:
theorem
iLipNorm_nonneg
{X : Type u_2}
[PseudoMetricSpace X]
{𝕜 : Type u_3}
[NormedField 𝕜]
{ϕ : X → 𝕜}
{x₀ : X}
{R : ℝ}
(hR : 0 ≤ R)
:
class
IsCancellative
(X : Type u_2)
{A : ℕ}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X ↑A]
(τ : ℝ)
[CompatibleFunctions ℝ X A]
:
Θ is τ-cancellative. τ will usually be 1 / a
- norm_integral_exp_le {x : X} {r : ℝ} {ϕ : X → ℂ} {K : NNReal} (h1 : LipschitzWith K ϕ) (h2 : 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) ^ (-τ)
Instances
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))
Instances For
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 (Metric.ball x r)ᶜ, K x y * f y
Instances For
def
upperRadius
{X : Type u_2}
[PseudoMetricSpace X]
[FunctionDistances ℝ X]
(Q : X → Θ X)
(θ : Θ X)
(x : X)
:
R_Q(θ, x) defined in (1.0.20).
Instances For
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)
:
The linearized maximally truncated nontangential Calderon Zygmund operator T_Q^θ
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
nontangentialOperator
{X : Type u_2}
{A : ℕ}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X ↑A]
(K : X → X → ℂ)
(f : X → ℂ)
(x : X)
:
The maximally truncated nontangential Calderon Zygmund operator T_*
Equations
Instances For
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)
:
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.
Instances For
def
carlesonOperator
{X : Type u_2}
{A : ℕ}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X ↑A]
[FunctionDistances ℝ X]
(K : X → X → ℂ)
(f : X → ℂ)
(x : X)
:
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
Instances For
class
IsOneSidedKernel
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
(a : outParam ℕ)
(K : X → X → ℂ)
:
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)
Instances
theorem
MeasureTheory.stronglyMeasurable_K
{X : Type u_1}
{a : ℕ}
{K : X → X → ℂ}
[PseudoMetricSpace X]
[MeasureSpace X]
[IsOneSidedKernel a K]
:
theorem
MeasureTheory.aestronglyMeasurable_K
{X : Type u_1}
{a : ℕ}
{K : X → X → ℂ}
[PseudoMetricSpace X]
[MeasureSpace X]
[IsOneSidedKernel a K]
:
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 :
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.
Instances
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) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)
- measurableSet_F : MeasurableSet F
- measurableSet_G : MeasurableSet G
- measurable_σ₁ : Measurable σ₁
- measurable_σ₂ : Measurable σ₂
- σ₁_le_σ₂ : σ₁ ≤ σ₂
- Q : MeasureTheory.SimpleFunc X (Θ X)
Instances
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
stronglyMeasurable_Q₂
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
:
MeasureTheory.StronglyMeasurable 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
measurable_Q₁
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
(x : X)
:
Measurable ⇑(Q x)
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]
:
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]
:
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]
:
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]
:
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]
:
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
inv_q_sub_half_nonneg
(X : Type u_1)
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
:
theorem
one_lt_nnq
(X : Type u_1)
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
:
theorem
nnq_le_two
(X : Type u_1)
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
:
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]
:
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)
- 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) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)
- measurable_σ₁ : Measurable σ₁
- measurable_σ₂ : Measurable σ₂
- finite_range_σ₁ : Finite ↑(Set.range σ₁)
- finite_range_σ₂ : Finite ↑(Set.range σ₂)
- Q : MeasureTheory.SimpleFunc X (Θ X)
- volume_F_pos : 0 < MeasureTheory.volume F
- volume_G_pos : 0 < MeasureTheory.volume G
Instances
Equations
- ShortVariables.termD = Lean.ParserDescr.node `ShortVariables.termD 1024 (Lean.ParserDescr.symbol "D")
Instances For
Equations
- ShortVariables.termκ = Lean.ParserDescr.node `ShortVariables.termκ 1024 (Lean.ParserDescr.symbol "κ")
Instances For
Equations
- ShortVariables.termZ = Lean.ParserDescr.node `ShortVariables.termZ 1024 (Lean.ParserDescr.symbol "Z")
Instances For
Equations
- ShortVariables.termτ = Lean.ParserDescr.node `ShortVariables.termτ 1024 (Lean.ParserDescr.symbol "τ")
Instances For
Equations
- ShortVariables.termO = Lean.ParserDescr.node `ShortVariables.termO 1024 (Lean.ParserDescr.symbol "o")
Instances For
Equations
- ShortVariables.termS = Lean.ParserDescr.node `ShortVariables.termS 1024 (Lean.ParserDescr.symbol "S")
Instances For
Equations
- ShortVariables.termNnτ = Lean.ParserDescr.node `ShortVariables.termNnτ 1024 (Lean.ParserDescr.symbol "nnτ")
Instances For
Equations
- ShortVariables.termNnq = Lean.ParserDescr.node `ShortVariables.termNnq 1024 (Lean.ParserDescr.symbol "nnq")
Instances For
Equations
- ShortVariables.termNnD = Lean.ParserDescr.node `ShortVariables.termNnD 1024 (Lean.ParserDescr.symbol "nnD")
Instances For
theorem
isBounded_F
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[h : ProofData a q K σ₁ σ₂ F G]
:
theorem
isBounded_G
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[h : ProofData a q K σ₁ σ₂ F G]
:
the L^∞-normalized τ-Hölder norm. Do we use this for other values of τ?
Equations
Instances For
Lemma 2.1.1
theorem
Θ.finite_and_mk_le_of_le_dist
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[PseudoMetricSpace X]
[h : 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]
[h : 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)
: