Theorem: control_approximation_effect'
Proof state before:
case e_a.e_a.e_f.h.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 : ℝ
⊢ 1 = max (1 - |x - y|) 0 + if |x - y| ≤ 1 then |x - y| else 1
Tactic:
split_ifs
Proof state after:
case pos
ε : ℝ
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 : ℝ
h✝ : |x - y| ≤ 1
⊢ 1 = max (1 - |x - y|) 0 + |x - y|

case neg
ε : ℝ
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 : ℝ
h✝ : ¬|x - y| ≤ 1
⊢ 1 = max (1 - |x - y|) 0 + 1