noncomputable def carlesonOperatorReal (K : ℝ → ℝ → ℂ) (f : ℝ → ℂ) (x : ℝ) : ENNReal

Equations

• carlesonOperatorReal K f x = ⨆ (n : ℤ), ⨆ (r : ℝ), ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ‖∫ (y : ℝ) in {y : ℝ | dist x y ∈ Set.Ioo r 1}, f y * K x y * Complex.exp (Complex.I * ↑n * ↑y)‖ₑ

theorem annulus_real_eq {x r R : ℝ} (r_nonneg : 0 ≤ r) : {y : ℝ | dist x y ∈ Set.Ioo r R} = Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R)

theorem annulus_real_volume {x r R : ℝ} (hr : r ∈ Set.Icc 0 R) : MeasureTheory.volume {y : ℝ | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r))

theorem annulus_measurableSet {x r R : ℝ} : MeasurableSet {y : ℝ | dist x y ∈ Set.Ioo r R}

theorem sup_eq_sup_dense_of_continuous {f : ℝ → ENNReal} {S : Set ℝ} (D : Set ℝ) (hS : IsOpen S) (hD : Dense D) (hf : ContinuousOn f S) : ⨆ r ∈ S, f r = ⨆ r ∈ S ∩ D, f r

theorem measurable_mul_kernel {n : ℤ} {f : ℝ → ℂ} (hf : Measurable f) : Measurable (Function.uncurry fun (x y : ℝ) => f y * K x y * Complex.exp (Complex.I * ↑n * ↑y))

theorem carlesonOperatorReal_measurable {f : ℝ → ℂ} (meas_f : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hf : ∀ (x : ℝ), MeasureTheory.IntegrableOn f (Set.Ioo x (x + 2)) MeasureTheory.volume) : Measurable (carlesonOperatorReal K f)

theorem carlesonOperatorReal_mul {f : ℝ → ℂ} {x a : ℝ} (ha : 0 < a) : carlesonOperatorReal K f x = ENNReal.ofReal a * carlesonOperatorReal K (fun (x : ℝ) => 1 / ↑a * f x) x

theorem carlesonOperatorReal_eq_of_restrict_interval {f : ℝ → ℂ} {a b x : ℝ} (hx : x ∈ Set.Icc a b) : carlesonOperatorReal K f x = carlesonOperatorReal K ((Set.Ioo (a - 1) (b + 1)).indicator f) x