Theorem: control_approximation_effect'
Proof state before:
case intro.intro
ε : ℝ
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)) ≠ ⊤
⊢ ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≤
    T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))
Tactic:
calc ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))
  _ = ENNReal.ofReal ((2 * Real.pi) * ε') := by
    rw [← ENNReal.ofReal_add]
    . congr
      ring
    . apply mul_nonneg _ Real.two_pi_pos.le
      rw [ε'def, C_control_approximation_effect_eq hε.1.le, add_sub_cancel_right]
      apply div_nonneg _ Real.pi_pos.le
      apply mul_nonneg
      . rw [mul_assoc]
        apply mul_nonneg hδ.le
        rw [C1_2]
        apply mul_nonneg (by norm_num)
        apply Real.rpow_nonneg
        linarith [Real.pi_pos]
      . apply Real.rpow_nonneg (div_nonneg (by norm_num) hε.1.le)
    . apply mul_nonneg (mul_nonneg Real.pi_pos.le hδ.le) Real.two_pi_pos.le
  _ ≤ ENNReal.ofReal ((2 * Real.pi) * abs (1 / (2 * Real.pi) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), h y * dirichletKernel' N (x - y))) := by gcongr
  _ = ‖∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), h y * dirichletKernel' N (x - y)‖₊  := by
    rw [map_mul, map_div₀, ←mul_assoc]
    rw [ENNReal.ofReal, ← norm_toNNReal]
    congr
    conv => rhs; rw [← one_mul ‖_‖]
    congr
    simp
    rw [_root_.abs_of_nonneg Real.pi_pos.le]
    field_simp
    ring
  _ = ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), h y * dirichletKernel' N (x - y)‖₊ := by
    congr 2
    rw [← zero_add (2 * Real.pi), Function.Periodic.intervalIntegral_add_eq _ 0 (x - Real.pi)]
    congr 1
    ring
    apply Function.Periodic.mul h_periodic
    apply Function.Periodic.const_sub dirichletKernel'_periodic
  _ = ‖  (∫ (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), h y * (min |x - y| 1) * dirichletKernel' N (x - y))      ‖₊ := by
    congr
    rw [← intervalIntegral.integral_add]
    . congr
      ext y
      rw [←add_mul, ←mul_add]
      congr
      conv => lhs; rw [←mul_one (h y)]
      congr
      norm_cast
      rw [min_def]
      split_ifs
      . rw [max_eq_left (by linarith)]
        simp
      . rw [max_eq_right (by linarith)]
        simp
    rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith [Real.pi_pos])]
    apply integrableOn_mul_dirichletKernel'_max xIcc h_intervalIntegrable
    rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith [Real.pi_pos])]
    apply integrableOn_mul_dirichletKernel'_min xIcc h_intervalIntegrable
  _ ≤   ‖∫ (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), h y * (min |x - y| 1) * dirichletKernel' N (x - y)‖₊ := by
    norm_cast
    apply nnnorm_add_le
  _ ≤ (T' f x + T' ((starRingEnd ℂ) ∘ f) x) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) := by
    gcongr
    . 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
    . 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