internlm/Lean-Github huggingface dataset:
Theorem: classical_carleson
Proof 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]
Proof state after:
no goals
Theorem: classical_carleson
Proof 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
Proof state after:
no goals
Theorem: classical_carleson
Proof 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
Proof state after:
no goals
Theorem: classical_carleson
Proof 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
Proof 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
Theorem: classical_carleson
Proof 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
Proof 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
Theorem: classical_carleson
Proof 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
Proof 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
Theorem: classical_carleson
Proof 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]
Proof state after:
no goals
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₀
⊢ ε' + ε / 4 + ε / 4 ≤ ε / 2 + ε / 4 + ε / 4
Tactic:
gcongr
Proof 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
Theorem: classical_carleson
Proof 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]
Proof 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
Theorem: classical_carleson
Proof 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)
Proof 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 ε
Theorem: classical_carleson
Proof 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)]
Proof 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 ε
Theorem: classical_carleson
Proof 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])
Proof state after:
no goals
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₀
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals