theorem ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {f : X → ENNReal} {g : X → ENNReal} {E : Set X} (hE : MeasurableSet E) (hf : Measurable f) (hg : Measurable g) {a : ENNReal} (h : ∀ x ∈ E, a ≤ f x + g x) : ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ ∀ x ∈ E', a / 2 ≤ g x)

theorem Dirichlet_Hilbert_eq {N : ℕ} {x : ℝ} : ↑(max (1 - |x|) 0) * dirichletKernel' N x = Complex.exp (Complex.I * (-↑N * ↑x)) * k x + (starRingEnd ℂ) (Complex.exp (Complex.I * (-↑N * ↑x)) * k x)

theorem Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-Real.pi) Real.pi) : ‖dirichletKernel' N x - (Complex.exp (Complex.I * (-↑N * ↑x)) * k x + (starRingEnd ℂ) (Complex.exp (Complex.I * (-↑N * ↑x)) * k x))‖ ≤ Real.pi

theorem le_iSup_of_tendsto {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) : a ≤ iSup f

theorem integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {r : ℝ} (r_nonneg : 0 ≤ r) (rle1 : r < 1) : MeasureTheory.Integrable (fun (x : ℝ) => f x) (MeasureTheory.volume.restrict {y : ℝ | dist x y ∈ Set.Ioo r 1})

theorem intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} : IntervalIntegrable (fun (y : ℝ) => f y * dirichletKernel' N (x - y)) MeasureTheory.volume (x - Real.pi) (x + Real.pi)

theorem intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} : IntervalIntegrable (fun (y : ℝ) => f y * (↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) MeasureTheory.volume (x - Real.pi) (x + Real.pi)

theorem intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} : IntervalIntegrable (fun (y : ℝ) => f y * (dirichletKernel' N (x - y) - ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) MeasureTheory.volume (x - Real.pi) (x + Real.pi)

theorem domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) : ∫ (y : ℝ) in x - Real.pi..x + Real.pi, g y * (↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) = ∫ (y : ℝ) in {y : ℝ | dist x y ∈ Set.Ioo 0 1}, g y * (↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y))

theorem intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} : MeasureTheory.IntegrableOn (fun (y : ℝ) => f y * (↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) {y : ℝ | dist x y ∈ Set.Ioo 0 1} MeasureTheory.volume

theorem le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) : ↑‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, g y * (↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊ ≤ carlesonOperatorReal K g x + carlesonOperatorReal K (⇑(starRingEnd ℂ) ∘ g) x

theorem partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measurable_g : Measurable g) (periodic_g : Function.Periodic g (2 * Real.pi)) (bound_g : ∀ (x : ℝ), ‖g x‖ ≤ δ) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) : ↑‖partialFourierSum N g x‖₊ ≤ (carlesonOperatorReal K g x + carlesonOperatorReal K (⇑(starRingEnd ℂ) ∘ g) x) / ENNReal.ofReal (2 * Real.pi) + ENNReal.ofReal (Real.pi * δ)

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

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

def C_control_approximation_effect (ε : ℝ) : ℝ

Equations

• C_control_approximation_effect ε = C10_0_1 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi

theorem lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : Real.pi < C_control_approximation_effect ε

theorem C_control_approximation_effect_pos {ε : ℝ} (εpos : 0 < ε) : 0 < C_control_approximation_effect ε

theorem C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) : C_control_approximation_effect ε * δ = δ * C10_0_1 4 2 * (4 * Real.pi) ^ 2⁻¹ * (2 / ε) ^ 2⁻¹ / Real.pi + Real.pi * δ

theorem control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ : 0 < δ) {h : ℝ → ℂ} (h_measurable : Measurable h) (h_periodic : Function.Periodic h (2 * Real.pi)) (h_bound : ∀ (x : ℝ), ‖h x‖ ≤ δ) : ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ MeasureTheory.volume.real E ≤ ε ∧ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), ‖partialFourierSum N h x‖ ≤ C_control_approximation_effect ε * δ