Theorem: control_approximation_effect'
Proof state before:
case h₂.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)‖ ≤
    Real.pi * δ * (2 * Real.pi)
Tactic:
calc ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), h y * (min |x - y| 1) * dirichletKernel' N (x - y)‖
  _ ≤ (δ * Real.pi) * |(x + Real.pi) - (x - Real.pi)| := by
    apply intervalIntegral.norm_integral_le_of_norm_le_const
    intro y hy
    rw [Set.uIoc_of_le (by linarith)] at hy
    rw [mul_assoc, norm_mul]
    gcongr
    . rw [norm_eq_abs]
      apply h_bound
      rw [Fdef]
      simp
      constructor <;> linarith [xIcc.1, xIcc.2, hy.1, hy.2]
    rw [dirichletKernel', mul_add]
    set z := x - y with zdef
    calc ‖  (min |z| 1) * (exp (I * N * z) / (1 - exp (-I * z)))
          + (min |z| 1) * (exp (-I * N * z) / (1 - exp (I * z)))‖
      _ ≤   ‖(min |z| 1) * (exp (I * N * z) / (1 - exp (-I * z)))‖
          + ‖(min |z| 1) * (exp (-I * N * z) / (1 - exp (I * z)))‖ := by
        apply norm_add_le
      _ = min |z| 1 * 1 / ‖1 - exp (I * z)‖ + min |z| 1 * 1 / ‖1 - exp (I * z)‖ := by
        simp
        congr
        . simp only [abs_eq_self, le_min_iff, abs_nonneg, zero_le_one, and_self]
        . rw [mul_assoc I, mul_comm I]
          norm_cast
          rw [abs_exp_ofReal_mul_I, one_div, ←abs_conj, map_sub, map_one, ←exp_conj, ← neg_mul, map_mul,
                conj_neg_I, conj_ofReal]
        . 
          simp only [abs_eq_self, le_min_iff, abs_nonneg, zero_le_one, and_self]
        . rw [mul_assoc I, mul_comm I, ←neg_mul]
          norm_cast
          rw [abs_exp_ofReal_mul_I, one_div]
      _ = 2 * (min |z| 1 / ‖1 - exp (I * z)‖) := by ring
      _ ≤ 2 * (Real.pi / 2) := by
        gcongr 2 * ?_
        . by_cases h : (1 - exp (I * z)) = 0
          . rw [h, norm_zero, div_zero]
            linarith [Real.pi_pos]
          rw [div_le_iff', ←div_le_iff, div_div_eq_mul_div, mul_div_assoc, mul_comm]
          apply lower_secant_bound'
          . apply min_le_left
          . have : |z| ≤ Real.pi := by
              rw [abs_le]
              rw [zdef]
              constructor <;> linarith [hy.1, hy.2]
            rw [min_def]
            split_ifs <;> linarith
          . linarith [Real.pi_pos]
          . rwa [norm_pos_iff]
      _ = Real.pi := by ring
  _ = Real.pi * δ * (2 * Real.pi) := by
    simp
    rw [←two_mul, _root_.abs_of_nonneg Real.two_pi_pos.le]
    ring
Proof state after:
no goals