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
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:
no goals