Theorem: classical_carleson
Proof 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
Proof 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