internlm/Lean-Github huggingface dataset:
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
ring_nf
Proof state after:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
rw [neg_div, Real.rpow_neg]
Proof state after:
case e_a.e_a.e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
all_goals linarith [Real.pi_pos]
Proof state after:
no goals
Theorem: C_control_approximation_effect_eq
Proof state before:
case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
linarith [Real.pi_pos]
Proof state after:
no goals
Theorem: control_approximation_effect'
Proof state before:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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 ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
          ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * δ
Tactic:
set ε' := C_control_approximation_effect ε * δ with ε'def
Proof state after:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
set E := {x ∈ Set.Icc 0 (2 * Real.pi) | ∃ N, ε' < abs (partialFourierSum h N x)} with Edef
Proof state after:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
have E_eq: E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N : ℕ, {x | ε' < ‖partialFourierSum h N x‖} := by
    rw [Edef]
    ext x
    simp
Proof state after:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
have measurableSetE : MeasurableSet E := by
  rw [E_eq]
  apply MeasurableSet.inter
  . apply measurableSet_Icc
  apply MeasurableSet.iUnion
  intro N
  apply measurableSet_lt
  . apply measurable_const
  apply Measurable.norm
  apply partialFourierSum_uniformContinuous.continuous.measurable
Proof state after:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ ∃ E ⊆ Set.Icc 0 (2 * Real.pi),
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
use E
Proof state after:
case h
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ E ⊆ Set.Icc 0 (2 * Real.pi) ∧
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
case h
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ E ⊆ Set.Icc 0 (2 * Real.pi) ∧
    MeasurableSet E ∧
      MeasureTheory.volume.real E ≤ ε ∧
        ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
constructor
Proof state after:
case h.left
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ E ⊆ Set.Icc 0 (2 * Real.pi)

case h.right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasurableSet E ∧
    MeasureTheory.volume.real E ≤ ε ∧
      ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
case h.left
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ E ⊆ Set.Icc 0 (2 * Real.pi)

case h.right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasurableSet E ∧
    MeasureTheory.volume.real E ≤ ε ∧
      ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
. intro x hx
  rw [Edef] at hx
  simp at hx
  exact hx.1
Proof state after:
case h.right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasurableSet E ∧
    MeasureTheory.volume.real E ≤ ε ∧
      ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
case h.right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasurableSet E ∧
    MeasureTheory.volume.real E ≤ ε ∧
      ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
use measurableSetE
Proof state after:
case right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasureTheory.volume.real E ≤ ε ∧
    ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Theorem: control_approximation_effect'
Proof state before:
case right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasureTheory.volume.real E ≤ ε ∧
    ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'
Tactic:
rw [and_comm]
Proof state after:
case right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ (∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε') ∧
    MeasureTheory.volume.real E ≤ ε
Theorem: control_approximation_effect'
Proof state before:
case right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ (∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε') ∧
    MeasureTheory.volume.real E ≤ ε
Tactic:
constructor
Proof state after:
case right.left
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'

case right.right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasureTheory.volume.real E ≤ ε
Theorem: control_approximation_effect'
Proof state before:
case right.left
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E, ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ ε'

case right.right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasureTheory.volume.real E ≤ ε
Tactic:
. rw [Edef]
  simp
  exact fun x x_nonneg x_le_two_pi h ↦ h x_nonneg x_le_two_pi
Proof state after:
case right.right
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h : ℝ → ℂ
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) ≤ δ
ε' : ℝ := C_control_approximation_effect ε * δ
ε'def : ε' = C_control_approximation_effect ε * δ
E : Set ℝ := {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
Edef : E = {x | x ∈ Set.Icc 0 (2 * Real.pi) ∧ ∃ N, ε' < Complex.abs (partialFourierSum h N x)}
E_eq : E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N, {x | ε' < ‖partialFourierSum h N x‖}
measurableSetE : MeasurableSet E
⊢ MeasureTheory.volume.real E ≤ ε