theorem rcarleson_general {q q' : NNReal} (hq : q ∈ Set.Ioc 1 2) (hqq' : q.HolderConjugate q') {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G) (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x) : ∫⁻ (x : ℝ) in G, carlesonOperatorReal K f x ≤ ↑(C10_0_1 4 q) * MeasureTheory.volume G ^ (↑q')⁻¹ * MeasureTheory.volume F ^ (↑q)⁻¹

theorem rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G) (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x) : ∫⁻ (x : ℝ) in G, carlesonOperatorReal K f x ≤ ↑(C10_0_1 4 2) * MeasureTheory.volume G ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹