Theorem: control_approximation_effect'
Proof state before:
case h₁
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
h_intervalIntegrable : IntervalIntegrable h MeasureTheory.volume (-Real.pi) (3 * Real.pi)
F : Set ℝ := Set.Icc (-Real.pi) (3 * Real.pi)
h_bound : ∀ x ∈ F, Complex.abs (h x) ≤ δ
Fdef : F = Set.Icc (-Real.pi) (3 * Real.pi)
f : ℝ → ℂ := fun x => h x * F.indicator 1 x
fdef : f = fun x => h x * F.indicator 1 x
f_measurable : Measurable f
f_integrable : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
h_intervalIntegrable' : IntervalIntegrable h MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
xIcc : x ∈ Set.Icc 0 (2 * Real.pi)
N : ℕ
hN : ε' < Complex.abs (1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, h y * dirichletKernel' N (x - y))
this : ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≠ ⊤
⊢ ↑‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, h y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x

case h₂
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
h_intervalIntegrable : IntervalIntegrable h MeasureTheory.volume (-Real.pi) (3 * Real.pi)
F : Set ℝ := Set.Icc (-Real.pi) (3 * Real.pi)
h_bound : ∀ x ∈ F, Complex.abs (h x) ≤ δ
Fdef : F = Set.Icc (-Real.pi) (3 * Real.pi)
f : ℝ → ℂ := fun x => h x * F.indicator 1 x
fdef : f = fun x => h x * F.indicator 1 x
f_measurable : Measurable f
f_integrable : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
h_intervalIntegrable' : IntervalIntegrable h MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
xIcc : x ∈ Set.Icc 0 (2 * Real.pi)
N : ℕ
hN : ε' < Complex.abs (1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, h y * dirichletKernel' N (x - y))
this : ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≠ ⊤
⊢ ↑‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, h y * ↑(min |x - y| 1) * dirichletKernel' N (x - y)‖₊ ≤
    ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))
Tactic:
. calc ENNReal.ofNNReal ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), h y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊
    _ = ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ := by
      congr 2
      apply intervalIntegral.integral_congr
      intro y hy
      simp
      rw [Set.uIcc_of_le (by linarith)] at hy
      left
      left
      rw [fdef, ←mul_one (h y)]
      congr
      rw [Set.indicator_apply]
      have : y ∈ F := by
        rw [Fdef]
        simp
        constructor <;> linarith [xIcc.1, xIcc.2, hy.1, hy.2]
      simp [this]
    _ = ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 Real.pi}, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ := by
      congr
      rw [annulus_real_eq (le_refl 0), MeasureTheory.integral_union (by simp), ← MeasureTheory.integral_Ioc_eq_integral_Ioo, ← MeasureTheory.integral_union,
        intervalIntegral.integral_of_le (by linarith), MeasureTheory.integral_Ioc_eq_integral_Ioo]
      congr
      simp
      rw [Set.Ioc_union_Ioo_eq_Ioo (by linarith) (by linarith)]
      . simp
        apply Set.disjoint_of_subset_right Set.Ioo_subset_Ioc_self
        simp
      . exact measurableSet_Ioo
      . apply (integrableOn_mul_dirichletKernel'_max xIcc f_integrable).mono_set
        intro y hy
        constructor <;> linarith [hy.1, hy.2, Real.pi_pos]
      . apply (integrableOn_mul_dirichletKernel'_max xIcc f_integrable).mono_set
        intro y hy
        constructor <;> linarith [hy.1, hy.2, Real.pi_pos]
      . exact measurableSet_Ioo
      . apply (integrableOn_mul_dirichletKernel'_max xIcc f_integrable).mono_set
        intro y hy
        constructor <;> linarith [hy.1, hy.2, Real.pi_pos]
      . apply (integrableOn_mul_dirichletKernel'_max xIcc f_integrable).mono_set
        intro y hy
        constructor <;> linarith [hy.1, hy.2, Real.pi_pos]
    _ = ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ := by
      congr 2
      rw [←MeasureTheory.integral_indicator annulus_measurableSet, ←MeasureTheory.integral_indicator annulus_measurableSet]
      congr
      ext y
      rw [Set.indicator_apply, Set.indicator_apply, mul_assoc, dirichlet_Hilbert_eq, K]
      split_ifs with h₀ h₁ h₂
      . trivial
      . dsimp at h₀
        dsimp at h₁
        rw [Real.dist_eq, Set.mem_Ioo] at h₀
        rw [Real.dist_eq, Set.mem_Ioo] at h₁
        push_neg at h₁
        rw [k_of_one_le_abs (h₁ h₀.1)]
        simp
      . rw [k_of_one_le_abs]
        simp
        dsimp at h₀
        dsimp at h₂
        rw [Real.dist_eq, Set.mem_Ioo] at h₀
        rw [Real.dist_eq, Set.mem_Ioo] at h₂
        push_neg at h₀
        apply le_trans' (h₀ h₂.1)
        linarith [Real.two_le_pi]
      . trivial
    _ ≤ (T' f x + T' ((starRingEnd ℂ) ∘ f) x) := by
      apply le_CarlesonOperatorReal' f_integrable x xIcc
Proof state after:
case h₂
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
h_intervalIntegrable : IntervalIntegrable h MeasureTheory.volume (-Real.pi) (3 * Real.pi)
F : Set ℝ := Set.Icc (-Real.pi) (3 * Real.pi)
h_bound : ∀ x ∈ F, Complex.abs (h x) ≤ δ
Fdef : F = Set.Icc (-Real.pi) (3 * Real.pi)
f : ℝ → ℂ := fun x => h x * F.indicator 1 x
fdef : f = fun x => h x * F.indicator 1 x
f_measurable : Measurable f
f_integrable : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
h_intervalIntegrable' : IntervalIntegrable h MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
xIcc : x ∈ Set.Icc 0 (2 * Real.pi)
N : ℕ
hN : ε' < Complex.abs (1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, h y * dirichletKernel' N (x - y))
this : ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≠ ⊤
⊢ ↑‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, h y * ↑(min |x - y| 1) * dirichletKernel' N (x - y)‖₊ ≤
    ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))