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
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 < 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
- metric : X → ℝ → PseudoMetricSpace (Θ X)
Instances
theorem
FunctionDistances.coeΘ_injective
{𝕜 : outParam (Type u_3)}
{X : Type u}
[NormedField 𝕜]
[TopologicalSpace X]
[self : FunctionDistances 𝕜 X]
{f : Θ X}
{g : Θ X}
(h : ∀ (x : X), (coeΘ f) x = (coeΘ g) x)
:
f = g
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]
:
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
Instances For
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)
Instances For
instance
instPseudoMetricSpaceWithFunctionDistance
{𝕜 : Type u_1}
{X : Type u_2}
[RCLike 𝕜]
[PseudoMetricSpace X]
{x : X}
{r : ℝ}
[d : FunctionDistances 𝕜 X]
:
Equations
- instPseudoMetricSpaceWithFunctionDistance = FunctionDistances.metric x r
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
:
Type (max (u + 1) u_3)
A set Θ of (continuous) functions is compatible. A will usually be 2 ^ a.
- Θ : Type u
- metric : X → ℝ → PseudoMetricSpace (Θ X)
- 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)
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)
Instances
theorem
CompatibleFunctions.eq_zero
{𝕜 : outParam (Type u_3)}
{X : Type u}
{A : outParam ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[self : CompatibleFunctions 𝕜 X A]
:
theorem
CompatibleFunctions.localOscillation_le_cdist
{𝕜 : outParam (Type u_3)}
{X : Type u}
{A : outParam ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[self : CompatibleFunctions 𝕜 X A]
{x : X}
{r : ℝ}
{f : Θ X}
{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)
theorem
CompatibleFunctions.cdist_mono
{𝕜 : outParam (Type u_3)}
{X : Type u}
{A : outParam ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[self : CompatibleFunctions 𝕜 X A]
{x₁ : X}
{x₂ : X}
{r₁ : ℝ}
{r₂ : ℝ}
{f : Θ X}
{g : Θ X}
(h : Metric.ball x₁ r₁ ⊆ Metric.ball x₂ r₂)
:
The distance is monotone in the ball. (1.0.9)
theorem
CompatibleFunctions.cdist_le
{𝕜 : outParam (Type u_3)}
{X : Type u}
{A : outParam ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[self : CompatibleFunctions 𝕜 X A]
{x₁ : X}
{x₂ : X}
{r : ℝ}
{f : Θ X}
{g : Θ X}
(h : dist x₁ x₂ < 2 * r)
:
The distance of a ball with large radius is bounded above. (1.0.8)
theorem
CompatibleFunctions.le_cdist
{𝕜 : outParam (Type u_3)}
{X : Type u}
{A : outParam ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[self : CompatibleFunctions 𝕜 X A]
{x₁ : X}
{x₂ : X}
{r : ℝ}
{f : Θ X}
{g : Θ X}
(h1 : Metric.ball x₁ r ⊆ Metric.ball x₂ (↑A * r))
:
The distance of a ball with large radius is bounded below. (1.0.10)
theorem
CompatibleFunctions.ballsCoverBalls
{𝕜 : outParam (Type u_3)}
{X : Type u}
{A : outParam ℕ}
[RCLike 𝕜]
[PseudoMetricSpace X]
[self : CompatibleFunctions 𝕜 X A]
{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]
:
Equations
- inhabited_Space = { default := ⋯.some }
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}, 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) ^ (-τ)
Instances
theorem
IsCancellative.norm_integral_exp_le
{X : Type u_2}
{A : ℕ}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X ↑A]
{τ : ℝ}
[CompatibleFunctions ℝ X A]
[self : IsCancellative X τ]
{x : X}
{r : ℝ}
{ϕ : X → ℂ}
{K : NNReal}
(h1 : LipschitzWith K ϕ)
(h2 : tsupport ϕ ⊆ Metric.ball x r)
{f : Θ X}
{g : Θ 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))
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
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
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_right : Measurable (Function.uncurry K)
- measurable_K_left : ∀ (y : X), Measurable fun (x : X) => K x y
Instances
theorem
IsOneSidedKernel.measurable_K_right
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
{a : outParam ℕ}
{K : X → X → ℂ}
[self : IsOneSidedKernel a K]
:
theorem
IsOneSidedKernel.measurable_K_left
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
{a : outParam ℕ}
{K : X → X → ℂ}
[self : IsOneSidedKernel a K]
(y : X)
:
Measurable fun (x : X) => K x y
theorem
IsOneSidedKernel.norm_K_le_vol_inv
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
{a : outParam ℕ}
{K : X → X → ℂ}
[self : IsOneSidedKernel a K]
(x : X)
(y : X)
:
theorem
IsOneSidedKernel.norm_K_sub_le
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
{a : outParam ℕ}
{K : X → X → ℂ}
[self : IsOneSidedKernel a K]
{x : X}
{y : X}
{y' : X}
(h : 2 * dist y y' ≤ dist x y)
:
class
IsTwoSidedKernel
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
(a : outParam ℕ)
(K : X → X → ℂ)
extends
IsOneSidedKernel
:
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_right : Measurable (Function.uncurry K)
- measurable_K_left : ∀ (y : X), Measurable fun (x : X) => K x y
Instances
theorem
IsTwoSidedKernel.norm_K_sub_le'
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
{a : outParam ℕ}
{K : X → X → ℂ}
[self : IsTwoSidedKernel a K]
{x : X}
{x' : X}
{y : X}
(h : 2 * dist x x' ≤ dist x y)
:
class
PreProofData
{X : Type u_1}
(a : outParam ℕ)
(q : outParam ℝ)
(K : outParam (X → X → ℂ))
(σ₁ : outParam (X → ℤ))
(σ₂ : outParam (X → ℤ))
(F : outParam (Set X))
(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 σ₂
- σ₁_le_σ₂ : σ₁ ≤ σ₂
- Q : MeasureTheory.SimpleFunc X (Θ X)
Instances
theorem
PreProofData.hcz
{X : Type u_1}
{a : outParam ℕ}
{q : outParam ℝ}
{K : outParam (X → X → ℂ)}
{σ₁ : outParam (X → ℤ)}
{σ₂ : outParam (X → ℤ)}
{F : outParam (Set X)}
{G : outParam (Set X)}
[PseudoMetricSpace X]
[self : PreProofData a q K σ₁ σ₂ F G]
:
IsOneSidedKernel a K
theorem
PreProofData.hasBoundedStrongType_Tstar
{X : Type u_1}
{a : outParam ℕ}
{q : outParam ℝ}
{K : outParam (X → X → ℂ)}
{σ₁ : outParam (X → ℤ)}
{σ₂ : outParam (X → ℤ)}
{F : outParam (Set X)}
{G : outParam (Set X)}
[PseudoMetricSpace X]
[self : PreProofData a q K σ₁ σ₂ F G]
:
MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => (nontangentialOperator K x1 x2).toReal) 2 2
MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)
theorem
PreProofData.measurable_σ₁
{X : Type u_1}
{a : outParam ℕ}
{q : outParam ℝ}
{K : outParam (X → X → ℂ)}
{σ₁ : outParam (X → ℤ)}
{σ₂ : outParam (X → ℤ)}
{F : outParam (Set X)}
{G : outParam (Set X)}
[PseudoMetricSpace X]
[self : PreProofData a q K σ₁ σ₂ F G]
:
Measurable σ₁
theorem
PreProofData.measurable_σ₂
{X : Type u_1}
{a : outParam ℕ}
{q : outParam ℝ}
{K : outParam (X → X → ℂ)}
{σ₁ : outParam (X → ℤ)}
{σ₂ : outParam (X → ℤ)}
{F : outParam (Set X)}
{G : outParam (Set X)}
[PseudoMetricSpace X]
[self : PreProofData a q K σ₁ σ₂ F G]
:
Measurable σ₂
theorem
twentyfive_le_realD
(X : Type u_1)
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
:
theorem
range_σ₁_subset
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
[PreProofData a q K σ₁ σ₂ F G]
:
theorem
range_σ₂_subset
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
[PreProofData a q K σ₁ σ₂ F G]
:
theorem
cast_a_pos
(X : Type u_1)
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[PseudoMetricSpace X]
[PreProofData a q K σ₁ σ₂ F G]
:
0 < ↑a
theorem
nnq_mem_Ioc
(X : Type u_1)
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 → ℤ))
(σ₂ : outParam (X → ℤ))
(F : outParam (Set X))
(G : outParam (Set X))
[PseudoMetricSpace X]
extends
PreProofData
:
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 σ₂
- σ₁_le_σ₂ : σ₁ ≤ σ₂
- 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
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 → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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)
: