instance
MetricΘ.instPseudoMetricSpaceΘReal
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[CompatibleFunctions ℝ X (defaultA a)]
:
PseudoMetricSpace (Θ X)
We choose as metric space instance on Θ one given by an arbitrary ball.
The metric given by all other balls are equivalent.
Equations
theorem
MetricΘ.dist_eq_cdist
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[CompatibleFunctions ℝ X (defaultA a)]
{f g : Θ X}
:
The following two lemmas state that the distance could be equivalently given by any other cdist.
instance
MetricΘ.instSecondCountableTopologyΘReal
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[CompatibleFunctions ℝ X (defaultA a)]
:
theorem
measurable_carlesonOperatorIntegrand
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{Q : MeasureTheory.SimpleFunc X (Θ X)}
{R₁ R₂ : ℝ}
{f : X → ℂ}
(mf : Measurable f)
:
Measurable fun (x : X) => carlesonOperatorIntegrand K (Q x) R₁ R₂ f x
theorem
rightContinuous_integral_annulus
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(iof : MeasureTheory.IntegrableOn f (Set.Annulus.oo x R₁ R₂) MeasureTheory.volume)
:
ContinuousWithinAt (fun (R : ℝ) => ∫ (y : X) in Set.Annulus.oo x R R₂, f y) (Set.Ici R₁) R₁
Let f be integrable over an annulus with fixed radii R₁, R₂.
Then fun R ↦ ∫ y in oo x R R₂, f y is right-continuous at R₁.
theorem
leftContinuous_integral_annulus
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(iof : MeasureTheory.IntegrableOn f (Set.Annulus.oo x R₁ R₂) MeasureTheory.volume)
:
ContinuousWithinAt (fun (R : ℝ) => ∫ (y : X) in Set.Annulus.oo x R₁ R, f y) (Set.Iic R₂) R₂
Let f be integrable over an annulus with fixed radii R₁, R₂.
Then fun R ↦ ∫ y in oo x R₁ R, f y is left-continuous at R₂.
theorem
integrableOn_annulus_of_bounded
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
:
theorem
integrableOn_coi_inner_annulus'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(nf : MeasureTheory.IntegrableOn f (Set.Annulus.oo x R₁ R₂) MeasureTheory.volume)
(hR₁ : 0 < R₁)
:
MeasureTheory.IntegrableOn (fun (y : X) => K x y * f y * Complex.exp (Complex.I * ↑(θ y))) (Set.Annulus.oo x R₁ R₂)
MeasureTheory.volume
The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.
theorem
integrableOn_coi_inner_annulus₀
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
MeasureTheory.IntegrableOn (fun (y : X) => K x y * f y * Complex.exp (Complex.I * ↑(θ y))) (Set.Annulus.oo x R₁ R₂)
MeasureTheory.volume
The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.
theorem
integrableOn_coi_inner_annulus
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
MeasureTheory.IntegrableOn (fun (y : X) => K x y * f y * Complex.exp (Complex.I * ↑(θ y))) (Set.Annulus.oo x R₁ R₂)
MeasureTheory.volume
The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.
theorem
rightContinuous_carlesonOperatorIntegrand'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : MeasureTheory.IntegrableOn f (Set.Annulus.oo x R₁ R₂) MeasureTheory.volume)
(hR₁ : 0 < R₁)
:
ContinuousWithinAt (fun (x_1 : ℝ) => carlesonOperatorIntegrand K θ x_1 R₂ f x) (Set.Ici R₁) R₁
theorem
rightContinuous_carlesonOperatorIntegrand
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
ContinuousWithinAt (fun (x_1 : ℝ) => carlesonOperatorIntegrand K θ x_1 R₂ f x) (Set.Ici R₁) R₁
theorem
leftContinuous_carlesonOperatorIntegrand'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : MeasureTheory.IntegrableOn f (Set.Annulus.oo x R₁ R₂) MeasureTheory.volume)
(hR₁ : 0 < R₁)
:
ContinuousWithinAt (fun (x_1 : ℝ) => carlesonOperatorIntegrand K θ R₁ x_1 f x) (Set.Iic R₂) R₂
theorem
leftContinuous_carlesonOperatorIntegrand
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
ContinuousWithinAt (fun (x_1 : ℝ) => carlesonOperatorIntegrand K θ R₁ x_1 f x) (Set.Iic R₂) R₂
theorem
exists_rat_near_carlesonOperatorIntegrand'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(θ : Θ X)
{R₁ R₂ : ℝ}
{f : X → ℂ}
(x : X)
(mf : MeasureTheory.IntegrableOn f (Set.Annulus.oo x R₁ R₂) MeasureTheory.volume)
(hR₁ : 0 < R₁)
(hR₂ : R₁ < R₂)
{ε : ℝ}
(εpos : 0 < ε)
:
Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂
and the norm of carlesonOperatorIntegrand changes by at most ε.
theorem
exists_rat_near_carlesonOperatorIntegrand
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
(θ : Θ X)
{R₁ R₂ : ℝ}
{f : X → ℂ}
(x : X)
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
(hR₂ : R₁ < R₂)
{ε : ℝ}
(εpos : 0 < ε)
:
Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂
and the norm of carlesonOperatorIntegrand changes by at most ε.
theorem
lintegral_inv_vol_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{x : X}
{R₁ R₂ : NNReal}
(hR₁ : 0 < R₁)
(hR₂ : R₁ < R₂)
:
theorem
edist_carlesonOperatorIntegrand_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ ϑ : Θ X}
{f : X → ℂ}
{x : X}
{R₁ R₂ : NNReal}
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
theorem
dist_carlesonOperatorIntegrand_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ ϑ : Θ X}
{f : X → ℂ}
{x : X}
{R₁ R₂ : NNReal}
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
theorem
continuous_carlesonOperatorIntegrand
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(mf : Measurable f)
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
Continuous fun (x_1 : Θ X) => carlesonOperatorIntegrand K x_1 R₁ R₂ f x
theorem
enorm_carlesonOperatorIntegrand_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{f : X → ℂ}
{x : X}
{R₁ R₂ : NNReal}
(nf : (fun (x : X) => ‖f x‖) ≤ 1)
(hR₁ : 0 < R₁)
:
theorem
carlesonOperatorIntegrand_measurable
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{R₁ R₂ : ℝ}
{f : X → ℂ}
{θ : Θ X}
(mf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
:
Measurable (carlesonOperatorIntegrand K θ R₁ R₂ f)
theorem
linearizedCarlesonOperator_measurable
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{f : X → ℂ}
{θ : Θ X}
(hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume)
:
Measurable (linearizedCarlesonOperator (fun (x : X) => θ) K f)
theorem
carlesonOperator_measurable
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{f : X → ℂ}
(hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume)
[Countable (Θ X)]
:
Measurable (carlesonOperator K f)
theorem
enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{x : X}
{f g : X → ℂ}
(hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume)
(hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume)
{θ : Θ X}
{R₁ R₂ : ℝ}
(R₁_pos : 0 < R₁)
:
‖carlesonOperatorIntegrand K θ R₁ R₂ (f + g) x‖ₑ ≤ ‖carlesonOperatorIntegrand K θ R₁ R₂ f x‖ₑ + ‖carlesonOperatorIntegrand K θ R₁ R₂ g x‖ₑ
theorem
linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{x : X}
{f g : X → ℂ}
(hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume)
(hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume)
{θ : Θ X}
:
linearizedCarlesonOperator (fun (x : X) => θ) K (f + g) x ≤ linearizedCarlesonOperator (fun (x : X) => θ) K f x + linearizedCarlesonOperator (fun (x : X) => θ) K g x
theorem
carlesonOperator_add_le_add_carlesonOperator
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{x : X}
{f g : X → ℂ}
(hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume)
(hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume)
:
theorem
tendsto_carlesonOperatorIntegrand_of_dominated_convergence
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{θ : Θ X}
{R₁ R₂ : ℝ}
{f : X → ℂ}
{x : X}
(hR₁ : 0 < R₁)
{l : Filter ℕ}
[l.IsCountablyGenerated]
{F : ℕ → X → ℂ}
(bound : X → ℝ)
(hF_meas : ∀ᶠ (n : ℕ) in l, MeasureTheory.AEStronglyMeasurable (F n) MeasureTheory.volume)
(h_bound : ∀ᶠ (n : ℕ) in l, ∀ᵐ (a : X), ‖F n a‖ ≤ bound a)
(bound_integrable : MeasureTheory.IntegrableOn (fun (y : X) => bound y) (Set.Annulus.oo x R₁ R₂) MeasureTheory.volume)
(h_lim : ∀ᵐ (a : X), Filter.Tendsto (fun (n : ℕ) => F n a) l (nhds (f a)))
:
Filter.Tendsto (fun (n : ℕ) => carlesonOperatorIntegrand K θ R₁ R₂ (F n) x) l
(nhds (carlesonOperatorIntegrand K θ R₁ R₂ f x))
theorem
linearizedCarlesonOperator_le_liminf_linearizedCarlesonOperator_of_tendsto
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{f : X → ℂ}
{x : X}
{Q : X → Θ X}
{l : Filter ℕ}
[l.IsCountablyGenerated]
[l.NeBot]
{F : ℕ → X → ℂ}
(bound : X → ℝ)
(hF_meas : ∀ᶠ (n : ℕ) in l, MeasureTheory.AEStronglyMeasurable (F n) MeasureTheory.volume)
(h_bound : ∀ᶠ (n : ℕ) in l, ∀ᵐ (a : X), ‖F n a‖ ≤ bound a)
(bound_integrable : MeasureTheory.LocallyIntegrable bound MeasureTheory.volume)
(h_lim : ∀ᵐ (a : X), Filter.Tendsto (fun (n : ℕ) => F n a) l (nhds (f a)))
:
linearizedCarlesonOperator Q K f x ≤ Filter.liminf (fun (n : ℕ) => linearizedCarlesonOperator Q K (F n) x) l
theorem
carlesonOperator_le_liminf_carlesonOperator_of_tendsto
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{K : X → X → ℂ}
[KernelProofData a K]
{f : X → ℂ}
{x : X}
{l : Filter ℕ}
[l.IsCountablyGenerated]
[l.NeBot]
{F : ℕ → X → ℂ}
(bound : X → ℝ)
(hF_meas : ∀ᶠ (n : ℕ) in l, MeasureTheory.AEStronglyMeasurable (F n) MeasureTheory.volume)
(h_bound : ∀ᶠ (n : ℕ) in l, ∀ᵐ (a : X), ‖F n a‖ ≤ bound a)
(bound_integrable : MeasureTheory.LocallyIntegrable bound MeasureTheory.volume)
(h_lim : ∀ᵐ (a : X), Filter.Tendsto (fun (n : ℕ) => F n a) l (nhds (f a)))
: