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 * ↑(min |x - y| 1) * dirichletKernel' N (x - y)‖₊ ≤
    ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))
Tactic:
. rw [ENNReal.ofReal]
  norm_cast
  apply NNReal.le_toNNReal_of_coe_le
  rw [coe_nnnorm]
  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