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

The constant used in two_sided_metric_carleson. Has value 2 ^ (474 * a ^ 3) / (q - 1) ^ 6 in the blueprint.

Equations

• C10_0_1 a q = C_K ↑a ^ 2 * C1_0_2 a q

theorem C10_0_1_pos {a : ℕ} {q : NNReal} (hq : 1 < q) : 0 < C10_0_1 a q

Theorem 10.0.1

theorem two_sided_metric_carleson {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {q q' : NNReal} {F G : Set X} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') (hF : MeasurableSet F) (hG : MeasurableSet G) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) {f : X → ℂ} (hmf : Measurable f) (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) : ∫⁻ (x : X) in G, carlesonOperator K f x ≤ ↑(C10_0_1 a q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹