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

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

Equations

• C1_0_2 a q = 2 ^ (450 * a ^ 3) / (q - 1) ^ 6

theorem C1_0_2_pos {a : ℕ} {q : ℝ} (hq : 1 < q) : 0 < C1_0_2 a q

theorem metric_carleson {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {q q' : ℝ} {F G : Set X} {K : X → X → ℂ} [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] [IsOneSidedKernel a K] (ha : 4 ≤ a) (hq : q ∈ Set.Ioc 1 2) (hqq' : q.IsConjExponent q') (hF : MeasurableSet F) (hG : MeasurableSet G) (hT : MeasureTheory.HasBoundedStrongType (fun (x1 : X → ℂ) (x2 : X) => (nontangentialOperator K x1 x2).toReal) 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 (C1_0_2 a q) * MeasureTheory.volume G ^ q'⁻¹ * MeasureTheory.volume F ^ q⁻¹