Theorem: control_approximation_effect'
Proof state before:
case h.h₁.hc
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h✝ : ℝ → ℂ
h_measurable : Measurable h✝
h_periodic : Function.Periodic h✝ (2 * Real.pi)
ε' : ℝ := 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
h_intervalIntegrable : IntervalIntegrable h✝ MeasureTheory.volume (-Real.pi) (3 * Real.pi)
F : Set ℝ := Set.Icc (-Real.pi) (3 * Real.pi)
h_bound : ∀ x ∈ F, Complex.abs (h✝ x) ≤ δ
Fdef : F = Set.Icc (-Real.pi) (3 * Real.pi)
f : ℝ → ℂ := fun x => h✝ x * F.indicator 1 x
fdef : f = fun x => h✝ x * F.indicator 1 x
f_measurable : Measurable f
f_integrable : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Evolume : MeasureTheory.volume E < ⊤
E' : Set ℝ
E'subset : E' ⊆ E
measurableSetE' : MeasurableSet E'
E'measure : MeasureTheory.volume E ≤ 2 * MeasureTheory.volume E'
h :
  (∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' f x) ∨
    ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
E'volume : MeasureTheory.volume E' < ⊤
this :
  ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤
    ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E' ^ 2⁻¹
δ_mul_const_pos : 0 < δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹
ε'_δ_expression_pos : 0 < Real.pi * (ε' - Real.pi * δ)
⊢ 0 ≤ MeasureTheory.volume.real E' ^ (-2⁻¹)

case h.h₁.h
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h✝ : ℝ → ℂ
h_measurable : Measurable h✝
h_periodic : Function.Periodic h✝ (2 * Real.pi)
ε' : ℝ := 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
h_intervalIntegrable : IntervalIntegrable h✝ MeasureTheory.volume (-Real.pi) (3 * Real.pi)
F : Set ℝ := Set.Icc (-Real.pi) (3 * Real.pi)
h_bound : ∀ x ∈ F, Complex.abs (h✝ x) ≤ δ
Fdef : F = Set.Icc (-Real.pi) (3 * Real.pi)
f : ℝ → ℂ := fun x => h✝ x * F.indicator 1 x
fdef : f = fun x => h✝ x * F.indicator 1 x
f_measurable : Measurable f
f_integrable : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Evolume : MeasureTheory.volume E < ⊤
E' : Set ℝ
E'subset : E' ⊆ E
measurableSetE' : MeasurableSet E'
E'measure : MeasureTheory.volume E ≤ 2 * MeasureTheory.volume E'
h :
  (∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' f x) ∨
    ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
E'volume : MeasureTheory.volume E' < ⊤
this :
  ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤
    ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E' ^ 2⁻¹
δ_mul_const_pos : 0 < δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹
ε'_δ_expression_pos : 0 < Real.pi * (ε' - Real.pi * δ)
⊢ Real.pi * (ε' - Real.pi * δ) * MeasureTheory.volume.real E' ≤
    δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ / MeasureTheory.volume.real E' ^ (-2⁻¹)
Tactic:
apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg
Proof state after:
case h.h₁.h
ε : ℝ
hε : 0 < ε ∧ ε ≤ 2 * Real.pi
δ : ℝ
hδ : 0 < δ
h✝ : ℝ → ℂ
h_measurable : Measurable h✝
h_periodic : Function.Periodic h✝ (2 * Real.pi)
ε' : ℝ := 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
h_intervalIntegrable : IntervalIntegrable h✝ MeasureTheory.volume (-Real.pi) (3 * Real.pi)
F : Set ℝ := Set.Icc (-Real.pi) (3 * Real.pi)
h_bound : ∀ x ∈ F, Complex.abs (h✝ x) ≤ δ
Fdef : F = Set.Icc (-Real.pi) (3 * Real.pi)
f : ℝ → ℂ := fun x => h✝ x * F.indicator 1 x
fdef : f = fun x => h✝ x * F.indicator 1 x
f_measurable : Measurable f
f_integrable : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T' f x + T' (⇑(starRingEnd ℂ) ∘ f) x
Evolume : MeasureTheory.volume E < ⊤
E' : Set ℝ
E'subset : E' ⊆ E
measurableSetE' : MeasurableSet E'
E'measure : MeasureTheory.volume E ≤ 2 * MeasureTheory.volume E'
h :
  (∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' f x) ∨
    ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
E'volume : MeasureTheory.volume E' < ⊤
this :
  ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤
    ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E' ^ 2⁻¹
δ_mul_const_pos : 0 < δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹
ε'_δ_expression_pos : 0 < Real.pi * (ε' - Real.pi * δ)
⊢ Real.pi * (ε' - Real.pi * δ) * MeasureTheory.volume.real E' ≤
    δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ / MeasureTheory.volume.real E' ^ (-2⁻¹)