theorem rcarleson_exceptional_set_estimate {δ C : NNReal} (Cpos : 0 < C) {f : ℝ → ℂ} (hmf : Measurable f) {F : Set ℝ} (measurableSetF : MeasurableSet F) (hf : ∀ (x : ℝ), ‖f x‖ ≤ ↑C * F.indicator 1 x) {E : Set ℝ} (measurableSetE : MeasurableSet E) (hE : ∀ x ∈ E, ↑δ ≤ carlesonOperatorReal K f x) : ↑δ * MeasureTheory.volume E ≤ ↑C * ↑(C10_0_1 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹

theorem rcarleson_exceptional_set_estimate_specific {δ C : NNReal} (Cpos : 0 < C) {f : ℝ → ℂ} (hmf : Measurable f) (hf : ∀ (x : ℝ), ‖f x‖ ≤ ↑C) {E : Set ℝ} (measurableSetE : MeasurableSet E) (E_subset : E ⊆ Set.Icc 0 (2 * Real.pi)) (hE : ∀ x ∈ E, ↑δ ≤ carlesonOperatorReal K f x) : ↑δ * MeasureTheory.volume E ≤ ↑C * ↑(C10_0_1 4 2) * ENNReal.ofReal (2 * Real.pi + 2) ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹

theorem rcarleson_exceptional_set_estimate_specific' {δ C : NNReal} (Cpos : 0 < C) {f : ℝ → ℂ} (hmf : Measurable f) (hf : ∀ (x : ℝ), ‖f x‖ ≤ ↑C) {E : Set ℝ} (measurableSetE : MeasurableSet E) (E_subset : E ⊆ Set.Icc 0 (2 * Real.pi)) (hE : ∀ x ∈ E, ↑δ ≤ carlesonOperatorReal K f x) : ↑δ * MeasureTheory.volume E ^ 2⁻¹ ≤ ↑C * ↑(C10_0_1 4 2) * ENNReal.ofReal (2 * Real.pi + 2) ^ 2⁻¹

theorem rcarleson_exceptional_set_estimate_specific'' {δ C : NNReal} (Cpos : 0 < C) {f : ℝ → ℂ} (hmf : Measurable f) (hf : ∀ (x : ℝ), ‖f x‖ ≤ ↑C) {E : Set ℝ} (measurableSetE : MeasurableSet E) (E_subset : E ⊆ Set.Icc 0 (2 * Real.pi)) (hE : ∀ x ∈ E, ↑δ ≤ carlesonOperatorReal K f x) : MeasureTheory.volume E ≤ ↑C ^ 2 * ↑(C10_0_1 4 2) ^ 2 * ENNReal.ofReal (2 * Real.pi + 2) / ↑δ ^ 2

noncomputable def C_distribution_carlesonOperatorReal_le' (δ ε : NNReal) : NNReal

The constant used in C_distribution_carlesonOperatorReal_le'.

Equations

• C_distribution_carlesonOperatorReal_le' δ ε = (ε / (C10_0_1 4 2 ^ 2 * (2 * Real.pi + 2).toNNReal / δ ^ 2)) ^ 2⁻¹

theorem C_distribution_carlesonOperatorReal_le'_pos {δ ε : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_distribution_carlesonOperatorReal_le' δ ε

theorem C_distribution_carlesonOperatorReal_le'_property {δ ε : NNReal} (δpos : 0 < δ) : ↑ε = ↑(C_distribution_carlesonOperatorReal_le' δ ε) ^ 2 * ↑(C10_0_1 4 2) ^ 2 * ENNReal.ofReal (2 * Real.pi + 2) / ↑δ ^ 2

theorem distribution_carlesonOperatorReal_le' {δ ε : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) {g : ℝ → ℂ} (hmg : Measurable g) (hg : ∀ (x : ℝ), ‖g x‖ ≤ ↑(C_distribution_carlesonOperatorReal_le' δ ε)) : MeasureTheory.distribution (carlesonOperatorReal K g) (↑δ) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ ↑ε

noncomputable def C_control_approximation_effect' (δ ε : NNReal) : NNReal

The constant used in C_control_approximation_effect'.

Equations

• C_control_approximation_effect' δ ε = min (δ / (2 * Real.pi).toNNReal) (C_distribution_carlesonOperatorReal_le' (2 * Real.pi * (↑δ / 2) / 2).toNNReal (ε / 2))

theorem C_control_approximation_effect'_pos {δ ε : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_control_approximation_effect' δ ε

theorem C_control_approximation_effect'_property {δ ε : NNReal} : ↑(C_control_approximation_effect' δ ε) * ENNReal.ofReal (2 * Real.pi) ≤ ↑δ

theorem C_control_approximation_effect'_le {δ ε : NNReal} : C_control_approximation_effect' δ ε ≤ C_distribution_carlesonOperatorReal_le' (2 * Real.pi * (↑δ / 2) / 2).toNNReal (ε / 2)

theorem control_approximation_effect' {δ ε : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) {g : ℝ → ℂ} (g_measurable : Measurable g) (g_periodic : Function.Periodic g (2 * Real.pi)) (g_bound : ∀ (x : ℝ), ‖g x‖ ≤ ↑(C_control_approximation_effect' δ ε)) : MeasureTheory.distribution (fun (x : ℝ) => ⨆ (N : ℕ), ‖partialFourierSum N g x‖ₑ) (↑δ) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ ↑ε