This file contains a reformulation of Theorem 10.0.1. It is not officially part of the blueprint.

Reformulations of Theorem 10.0.1

theorem two_sided_metric_carleson_hasRestrictedWeakType {X : Type u_1} {a : ℕ} [MetricSpace X] [d : MeasureTheory.DoublingMeasure X ↑(defaultA a)] {q q' : NNReal} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] [Countable (Θ X)] (ha : 4 ≤ a) (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : MeasureTheory.HasRestrictedWeakType (carlesonOperator K) (↑q) (↑q') MeasureTheory.volume MeasureTheory.volume ↑(C10_0_1 a q)

theorem two_sided_metric_carleson_hasLorentzType {X : Type u_1} {a : ℕ} [MetricSpace X] [d : MeasureTheory.DoublingMeasure X ↑(defaultA a)] {q : NNReal} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] [Countable (Θ X)] (ha : 4 ≤ a) (hq : q ∈ Set.Ioo 1 2) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : MeasureTheory.HasLorentzType (carlesonOperator K) (↑q) 1 ↑q ⊤ MeasureTheory.volume MeasureTheory.volume (4 * ↑(C10_0_1 a q) / ↑q)

noncomputable def interpolation_param (t₀ t₁ t : ℝ) : ℝ

The parameter where linear interpolation between t₀ and t₁ results in t.

Equations

• interpolation_param t₀ t₁ t = (t - t₀) / (t₁ - t₀)

theorem interpolation_param_interpolation {t₀ t₁ t : ℝ} (h : t₀ ≠ t₁) : t = (1 - interpolation_param t₀ t₁ t) * t₀ + interpolation_param t₀ t₁ t * t₁

theorem interpolation_param_mem_Ioo {t₀ t₁ t : ℝ} (h : t ∈ Set.Ioo t₀ t₁) : interpolation_param t₀ t₁ t ∈ Set.Ioo 0 1

noncomputable def C_carleson_hasStrongType (a : ℕ) (q : NNReal) : NNReal

The constant used in two_sided_metric_carleson_hasStrongType.

Equations

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

theorem C_carleson_hasStrongType_pos {a : ℕ} {q : NNReal} : 0 < C_carleson_hasStrongType a q

The constant used in two_sided_metric_carleson_hasStrongType.

theorem two_sided_metric_carleson_hasStrongType {X : Type u_1} {a : ℕ} [MetricSpace X] [d : MeasureTheory.DoublingMeasure X ↑(defaultA a)] {q : NNReal} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] [Countable (Θ X)] (ha : 4 ≤ a) (hq : q ∈ Set.Ioo 1 2) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : MeasureTheory.HasStrongType (carlesonOperator K) (↑q) (↑q) MeasureTheory.volume MeasureTheory.volume ↑(C_carleson_hasStrongType a q)