Theorem: control_approximation_effect'
Proof state before:
case e_a.e_a
ε : ℝ
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 * dirichletKernel' N (x - y) =
    ∫ (x_1 : ℝ) in x - Real.pi..x + Real.pi,
      h x_1 * ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1) +
        h x_1 * ↑(min |x - x_1| 1) * dirichletKernel' N (x - x_1)

case e_a.e_a.hf
ε : ℝ
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)) ≠ ⊤
⊢ IntervalIntegrable (fun y => h y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) MeasureTheory.volume
    (x - Real.pi) (x + Real.pi)

case e_a.e_a.hg
ε : ℝ
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)) ≠ ⊤
⊢ IntervalIntegrable (fun y => h y * ↑(min |x - y| 1) * dirichletKernel' N (x - y)) MeasureTheory.volume (x - Real.pi)
    (x + Real.pi)
Tactic:
. 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
Proof state after:
case e_a.e_a.hf
ε : ℝ
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)) ≠ ⊤
⊢ IntervalIntegrable (fun y => h y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) MeasureTheory.volume
    (x - Real.pi) (x + Real.pi)

case e_a.e_a.hg
ε : ℝ
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)) ≠ ⊤
⊢ IntervalIntegrable (fun y => h y * ↑(min |x - y| 1) * dirichletKernel' N (x - y)) MeasureTheory.volume (x - Real.pi)
    (x + Real.pi)