Theorem: classical_carleson (Carleson/Theorem1_1/ClassicalCarleson.lean)

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
hε : ε ∈ Set.Ioc 0 (2 * Real.pi)
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
rcases hε with ⟨εpos, εle⟩
State after:
case intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
set ε' := ε / 4 / C_control_approximation_effect ε with ε'def
State after:
case intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have ε'pos : ε' > 0 := by
  rw [ε'def]
  apply div_pos _ (C_control_approximation_effect_pos εpos)
  apply div_pos εpos (by norm_num)
State after:
case intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
obtain ⟨f₀, contDiff_f₀, periodic_f₀, hf₀⟩ := closeSmoothApproxPeriodic unicontf periodicf ε'pos
State after:
case intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have ε4pos : ε / 4 > 0 := by linarith
State after:
case intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
obtain ⟨N₀, hN₀⟩ := fourierConv_ofTwiceDifferentiable periodic_f₀ ((contDiff_top.mp (contDiff_f₀)) 2) ε4pos
State after:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
set h := f₀ - f with hdef
State after:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have h_measurable : Measurable h := Continuous.measurable (Continuous.sub contDiff_f₀.continuous unicontf.continuous)
State after:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have h_periodic : Function.Periodic h (2 * Real.pi) := Function.Periodic.sub periodic_f₀ periodicf
State after:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
have h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε' := by
  intro x _
  simp [hdef]
  rw [←Complex.dist_eq, dist_comm, Complex.dist_eq]
  exact hf₀ x
State after:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
obtain ⟨E, Esubset, Emeasurable, Evolume, hE⟩ := control_approximation_effect' ⟨εpos, εle⟩ ε'pos h_measurable h_periodic h_bound
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∃ N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
use E, Esubset, Emeasurable, Evolume, N₀
State after:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ N > N₀, Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
intro x hx N NgtN₀
State after:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε

State before:
case h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - partialFourierSum f N x) ≤ ε
Tactic:
calc Complex.abs (f x - partialFourierSum f N x)
_ = Complex.abs ((f x - f₀ x) + (f₀ x - partialFourierSum f₀ N x) + (partialFourierSum f₀ N x - partialFourierSum f N x)) := by congr; ring
_ ≤ Complex.abs ((f x - f₀ x) + (f₀ x - partialFourierSum f₀ N x)) + Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) := by
  apply AbsoluteValue.add_le
_ ≤ Complex.abs (f x - f₀ x) + Complex.abs (f₀ x - partialFourierSum f₀ N x) + Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) := by
  apply add_le_add_right
  apply AbsoluteValue.add_le
_ ≤ ε' + (ε / 4) + (ε / 4) := by
  gcongr
  . exact hf₀ x
  . exact hN₀ N NgtN₀ x hx.1
  . have := hE x hx N
    rw [hdef, partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable 0 (2 * Real.pi)) (unicontf.continuous.intervalIntegrable 0 (2 * Real.pi))] at this
    apply le_trans this
    rw [ε'def, mul_div_cancel₀ _ (C_control_approximation_effect_pos εpos).ne.symm]
_ ≤ (ε / 2) + (ε / 4) + (ε / 4) := by
  gcongr
  rw [ε'def, div_div]
  apply div_le_div_of_nonneg_left εpos.le (by norm_num)
  rw [← div_le_iff' (by norm_num)]
  apply le_trans' (lt_C_control_approximation_effect εpos).le (by linarith [Real.two_le_pi])
_ ≤ ε := by linarith
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ ε' > 0
Tactic:
rw [ε'def]
State after:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ ε / 4 / C_control_approximation_effect ε > 0

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ ε / 4 / C_control_approximation_effect ε > 0
Tactic:
apply div_pos _ (C_control_approximation_effect_pos εpos)
State after:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ 0 < ε / 4

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ 0 < ε / 4
Tactic:
apply div_pos εpos (by norm_num)
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
⊢ ε / 4 > 0
Tactic:
linarith
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
⊢ ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
Tactic:
intro x _
State after:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
x : ℝ
a✝ : x ∈ Set.Icc (-Real.pi) (3 * Real.pi)
⊢ Complex.abs (h x) ≤ ε'

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
x : ℝ
a✝ : x ∈ Set.Icc (-Real.pi) (3 * Real.pi)
⊢ Complex.abs (h x) ≤ ε'
Tactic:
simp [hdef]
State after:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
x : ℝ
a✝ : x ∈ Set.Icc (-Real.pi) (3 * Real.pi)
⊢ Complex.abs (f₀ x - f x) ≤ ε'

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
x : ℝ
a✝ : x ∈ Set.Icc (-Real.pi) (3 * Real.pi)
⊢ Complex.abs (f₀ x - f x) ≤ ε'
Tactic:
rw [←Complex.dist_eq, dist_comm, Complex.dist_eq]
State after:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
x : ℝ
a✝ : x ∈ Set.Icc (-Real.pi) (3 * Real.pi)
⊢ Complex.abs (f x - f₀ x) ≤ ε'

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
x : ℝ
a✝ : x ∈ Set.Icc (-Real.pi) (3 * Real.pi)
⊢ Complex.abs (f x - f₀ x) ≤ ε'
Tactic:
exact hf₀ x
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - partialFourierSum f N x) =
    Complex.abs (f x - f₀ x + (f₀ x - partialFourierSum f₀ N x) + (partialFourierSum f₀ N x - partialFourierSum f N x))
Tactic:
congr
State after:
case h.e_6.h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ f x - partialFourierSum f N x =
    f x - f₀ x + (f₀ x - partialFourierSum f₀ N x) + (partialFourierSum f₀ N x - partialFourierSum f N x)

State before:
case h.e_6.h
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ f x - partialFourierSum f N x =
    f x - f₀ x + (f₀ x - partialFourierSum f₀ N x) + (partialFourierSum f₀ N x - partialFourierSum f N x)
Tactic:
ring
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x + (f₀ x - partialFourierSum f₀ N x) + (partialFourierSum f₀ N x - partialFourierSum f N x)) ≤
    Complex.abs (f x - f₀ x + (f₀ x - partialFourierSum f₀ N x)) +
      Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x)
Tactic:
apply AbsoluteValue.add_le
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x + (f₀ x - partialFourierSum f₀ N x)) +
      Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤
    Complex.abs (f x - f₀ x) + Complex.abs (f₀ x - partialFourierSum f₀ N x) +
      Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x)
Tactic:
apply add_le_add_right
State after:
case bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x + (f₀ x - partialFourierSum f₀ N x)) ≤
    Complex.abs (f x - f₀ x) + Complex.abs (f₀ x - partialFourierSum f₀ N x)

State before:
case bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x + (f₀ x - partialFourierSum f₀ N x)) ≤
    Complex.abs (f x - f₀ x) + Complex.abs (f₀ x - partialFourierSum f₀ N x)
Tactic:
apply AbsoluteValue.add_le
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x) + Complex.abs (f₀ x - partialFourierSum f₀ N x) +
      Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤
    ε' + ε / 4 + ε / 4
Tactic:
gcongr
State after:
case h₁.h₁
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x) ≤ ε'

case h₁.h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4

case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4

State before:
case h₁.h₁
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x) ≤ ε'

case h₁.h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4

case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4
Tactic:
. exact hf₀ x
State after:
case h₁.h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4

case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4

State before:
case h₁.h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4

case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4
Tactic:
. exact hN₀ N NgtN₀ x hx.1
State after:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4

State before:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4
Tactic:
. have := hE x hx N
  rw [hdef, partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable 0 (2 * Real.pi)) (unicontf.continuous.intervalIntegrable 0 (2 * Real.pi))] at this
  apply le_trans this
  rw [ε'def, mul_div_cancel₀ _ (C_control_approximation_effect_pos εpos).ne.symm]
State after:
no goals

State before:
case h₁.h₁
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f x - f₀ x) ≤ ε'
Tactic:
exact hf₀ x
State after:
no goals

State before:
case h₁.h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
Tactic:
exact hN₀ N NgtN₀ x hx.1
State after:
no goals

State before:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4
Tactic:
have := hE x hx N
State after:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
this : Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4

State before:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
this : Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4
Tactic:
rw [hdef, partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable 0 (2 * Real.pi)) (unicontf.continuous.intervalIntegrable 0 (2 * Real.pi))] at this
State after:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
this : Complex.abs ((partialFourierSum f₀ N - partialFourierSum f N) x) ≤ C_control_approximation_effect ε * ε'
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4

State before:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
this : Complex.abs ((partialFourierSum f₀ N - partialFourierSum f N) x) ≤ C_control_approximation_effect ε * ε'
⊢ Complex.abs (partialFourierSum f₀ N x - partialFourierSum f N x) ≤ ε / 4
Tactic:
apply le_trans this
State after:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
this : Complex.abs ((partialFourierSum f₀ N - partialFourierSum f N) x) ≤ C_control_approximation_effect ε * ε'
⊢ C_control_approximation_effect ε * ε' ≤ ε / 4

State before:
case h₂
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
this : Complex.abs ((partialFourierSum f₀ N - partialFourierSum f N) x) ≤ C_control_approximation_effect ε * ε'
⊢ C_control_approximation_effect ε * ε' ≤ ε / 4
Tactic:
rw [ε'def, mul_div_cancel₀ _ (C_control_approximation_effect_pos εpos).ne.symm]
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ ε' + ε / 4 + ε / 4 ≤ ε / 2 + ε / 4 + ε / 4
Tactic:
gcongr
State after:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ ε' ≤ ε / 2

State before:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ ε' ≤ ε / 2
Tactic:
rw [ε'def, div_div]
State after:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ ε / (4 * C_control_approximation_effect ε) ≤ ε / 2

State before:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ ε / (4 * C_control_approximation_effect ε) ≤ ε / 2
Tactic:
apply div_le_div_of_nonneg_left εpos.le (by norm_num)
State after:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 2 ≤ 4 * C_control_approximation_effect ε

State before:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 2 ≤ 4 * C_control_approximation_effect ε
Tactic:
rw [← div_le_iff' (by norm_num)]
State after:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 2 / 4 ≤ C_control_approximation_effect ε

State before:
case bc.bc
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 2 / 4 ≤ C_control_approximation_effect ε
Tactic:
apply le_trans' (lt_C_control_approximation_effect εpos).le (by linarith [Real.two_le_pi])
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 2 / 4 ≤ Real.pi
Tactic:
linarith [Real.two_le_pi]
State after:
no goals

State before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ ε / 2 + ε / 4 + ε / 4 ≤ ε
Tactic:
linarith
State after:
no goals