Theorem: control_approximation_effect'
Proof state before:
case right.right
ε : ℝ
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)
⊢ MeasureTheory.volume.real E ≤ ε
Tactic:
have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T' f x + T' ((starRingEnd ℂ) ∘ f) x := by
  have h_intervalIntegrable' : IntervalIntegrable h MeasureTheory.volume 0 (2 * Real.pi) := by
    apply h_intervalIntegrable.mono_set
    rw [Set.uIcc_of_le (by linarith [Real.pi_pos]), Set.uIcc_of_le (by linarith [Real.pi_pos])]
    intro y hy
    constructor <;> linarith [hy.1, hy.2]
  intro x hx
  obtain ⟨xIcc, N, hN⟩ := hx
  rw [partialFourierSum_eq_conv_dirichletKernel' h_intervalIntegrable'] at hN
  have : ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≠ ⊤ := ENNReal.ofReal_ne_top
  rw [← (ENNReal.add_le_add_iff_right this)]
  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:
case right.right
ε : ℝ
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)
le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
⊢ MeasureTheory.volume.real E ≤ ε