internlm/Lean-Github huggingface dataset:
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp only [mul_ite, mul_zero, sum_range]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ i : Fin ↑n,
        ∑ i_1 : Fin ↑n, if ↑↑n ∣ m - ↑↑i - ↑↑i_1 then RuesDiff n (↑↑i) z₀ * RuesDiff n (↑↑i_1) z₁ * ↑↑n else 0) /
      ↑↑n =
    ∑ i : Fin ↑n, RuesDiff n (↑↑i) z₀ * RuesDiff n (m - ↑↑i) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ i : Fin ↑n,
        ∑ i_1 : Fin ↑n, if ↑↑n ∣ m - ↑↑i - ↑↑i_1 then RuesDiff n (↑↑i) z₀ * RuesDiff n (↑↑i_1) z₁ * ↑↑n else 0) /
      ↑↑n =
    ∑ i : Fin ↑n, RuesDiff n (↑↑i) z₀ * RuesDiff n (m - ↑↑i) z₁
Tactic:
sorry
Proof state after:
no goals
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
Tactic:
intros a b c
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
a b c : ℕ
⊢ cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
        (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
      cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
    RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
      (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
a b c : ℕ
⊢ cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
        (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
      cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
    RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
      (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
Tactic:
intros x x_1 x_2
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 x_2 : ℕ
⊢ -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
    2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 x_2 : ℕ
⊢ -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
    2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
Tactic:
intros x x_1
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 : ℕ
⊢ ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 : ℕ
⊢ ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: RuesArgumentSumRule
Proof state before:
n : ℕ+
z₀ z₁ : ℂ
⊢ Rues n (z₀ + z₁) = ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
rw [←RuesDiffM0EqualsRues, RuesDiffArgumentSumRule]
Proof state after:
n : ℕ+
z₀ z₁ : ℂ
⊢ ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Theorem: RuesArgumentSumRule
Proof state before:
n : ℕ+
z₀ z₁ : ℂ
⊢ ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
congr
Proof state after:
case e_f
n : ℕ+
z₀ z₁ : ℂ
⊢ (fun k => RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁) = fun k => RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Theorem: RuesArgumentSumRule
Proof state before:
case e_f
n : ℕ+
z₀ z₁ : ℂ
⊢ (fun k => RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁) = fun k => RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
ext k
Proof state after:
case e_f.h
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Theorem: RuesArgumentSumRule
Proof state before:
case e_f.h
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
congr 1
Proof state after:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑↑n - ↑k) z₁
Theorem: RuesArgumentSumRule
Proof state before:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑↑n - ↑k) z₁
Tactic:
rw [RuesDiffMPeriodic n (0 - ↑k) 1]
Proof state after:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k + 1 * ↑↑n) z₁ = RuesDiff n (↑↑n - ↑k) z₁
Theorem: RuesArgumentSumRule
Proof state before:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k + 1 * ↑↑n) z₁ = RuesDiff n (↑↑n - ↑k) z₁
Tactic:
congr 1
Proof state after:
case e_f.h.e_a.e_m
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ 0 - ↑k + 1 * ↑↑n = ↑↑n - ↑k
Theorem: RuesArgumentSumRule
Proof state before:
case e_f.h.e_a.e_m
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ 0 - ↑k + 1 * ↑↑n = ↑↑n - ↑k
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffZ0EqualsIte
Proof state before:
n : ℕ+
m : ℤ
⊢ RuesDiff n m 0 = if ↑↑n ∣ m then 1 else 0
Tactic:
sorry
Proof state after:
no goals
Theorem: EqualsNthDerivRuesDiffSum
Proof state before:
f : ℂ → ℂ
n : ℕ+
⊢ f = iteratedDeriv (↑n) f ↔ f = ∑ k ∈ range ↑n, (fun z => iteratedDeriv k f 0) * RuesDiff n (-↑k)
Tactic:
sorry
Proof state after:
no goals
Theorem: classical_carleson
Proof 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⟩
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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)
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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)
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε
Theorem: classical_carleson
Proof 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
Proof 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) ≤ ε