theorem ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {f 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

noncomputable def operatorBound (g : ℝ → ℂ) (x : ℝ) : ENNReal

The function used to bound the partial Fourier sum in partialFourierSum_bound

Equations

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

theorem partialFourierSum_bound {g : ℝ → ℂ} (periodic_g : Function.Periodic g (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) : ‖partialFourierSum N g x‖ₑ ≤ operatorBound g x