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

Equations

• One or more equations did not get rendered due to their size.

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 : ℝ → ℂ} (f_measurable : Measurable f) {B : ℝ} (f_bounded : ∀ (x : ℝ), ‖f x‖ ≤ B) : Measurable (carlesonOperatorReal K f)

theorem carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a) : carlesonOperatorReal K f x = ↑a.toNNReal * 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