def C10_0_1 (a : ℕ) (q : ℝ) : ℝ

The constant used in two_sided_metric_carleson. Has value 2 ^ (450 * 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 : ℝ} (hq : 1 < q) : 0 < C10_0_1 a q

theorem two_sided_metric_carleson {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {q : ℝ} {q' : ℝ} {F : Set X} {G : Set X} {K : X → X → ℂ} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] [IsTwoSidedKernel a K] (ha : 4 ≤ a) (hq : q ∈ Set.Ioc 1 2) (hqq' : q.IsConjExponent 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 ≤ ENNReal.ofReal (C10_0_1 a q) * MeasureTheory.volume G ^ q'⁻¹ * MeasureTheory.volume F ^ q⁻¹