theorem instFactLtRealOfNatHMulPi_carleson_4 : Fact (0 < 2 * Real.pi)

theorem rcarleson'_restrict {p : NNReal} (hp : p ∈ Set.Ioo 1 2) {f : ℝ → ℂ} (f_periodic : Function.Periodic f (2 * Real.pi)) (hf : MeasureTheory.MemLp f (↑p) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))) : MeasureTheory.eLpNorm (carlesonOperatorReal K f) (↑p) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ 2 * ↑(C_carleson_hasStrongType 4 p) * MeasureTheory.eLpNorm f (↑p) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi)))

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

The constant used in C_distribution_carlesonOperatorReal_le.

Equations

• C_distribution_carlesonOperatorReal_le δ ε p = (2 * C_carleson_hasStrongType 4 p)⁻¹ * MeasureTheory.C_distribution_le_of_eLpNorm_le δ ε p

theorem C_distribution_carlesonOperatorReal_le_pos {δ ε p : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_distribution_carlesonOperatorReal_le δ ε p

theorem distribution_carlesonOperatorReal_le {δ ε p : NNReal} (δpos : 0 < δ) (hp : p ∈ Set.Ioo 1 2) {g : ℝ → ℂ} (g_periodic : Function.Periodic g (2 * Real.pi)) (g_measurable : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hg : MeasureTheory.eLpNorm g (↑p) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ ↑(C_distribution_carlesonOperatorReal_le δ ε p)) : MeasureTheory.distribution (carlesonOperatorReal K g) (↑δ) (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))) ≤ ↑ε

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

The constant used in C_control_approximation_effect.

Equations

• C_control_approximation_effect δ ε p = min (2 * (δ / 2) * ((2 * Real.pi.toNNReal) ^ (1 - (↑p)⁻¹))⁻¹) (C_distribution_carlesonOperatorReal_le (2 * Real.pi * (↑δ / 2) / 2).toNNReal (ε / 2) p)

theorem C_control_approximation_effect_pos {δ ε p : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_control_approximation_effect δ ε p

theorem C_control_approximation_effect_property {δ ε p : NNReal} (hp : 1 ≤ p) : ↑(C_control_approximation_effect δ ε p) * (2 * ENNReal.ofReal Real.pi) ^ (1 - (↑p)⁻¹) ≤ 2 * (↑δ / 2)

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

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