Theorem: control_approximation_effect'
Proof state before:
case right.right.intro.intro.intro.intro
ε : ℝ
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 * δ)
⊢ MeasureTheory.volume.real E ≤ ε
Tactic:
calc MeasureTheory.volume.real E
  _ ≤ 2 * MeasureTheory.volume.real E' := by
    rwa [MeasureTheory.measureReal_def, MeasureTheory.measureReal_def, ←@ENNReal.toReal_ofReal 2 (by norm_num),
      ←ENNReal.toReal_mul, ENNReal.toReal_le_toReal Evolume.ne, ENNReal.ofReal_ofNat]
    apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top E'volume.ne
  _ = 2 * MeasureTheory.volume.real E' ^ ((1 + -(2 : ℝ)⁻¹) * 2) := by
    conv => lhs; rw [←Real.rpow_one (MeasureTheory.volume.real E')]
    congr
    norm_num
  _ ≤ 2 * (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - Real.pi * δ))) ^ (2 : ℝ) := by
    gcongr
    rw [Real.rpow_mul MeasureTheory.measureReal_nonneg]
    gcongr
    rw [Real.rpow_add' MeasureTheory.measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff' ε'_δ_expression_pos, ← mul_assoc]
    apply mul_le_of_nonneg_of_le_div δ_mul_const_pos.le
    apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg
    rw[Real.rpow_neg MeasureTheory.measureReal_nonneg, div_inv_eq_mul]
    rw [← ENNReal.ofReal_le_ofReal_iff, ENNReal.ofReal_mul ε'_δ_expression_pos.le, MeasureTheory.measureReal_def, ENNReal.ofReal_toReal E'volume.ne]
    apply le_trans this
    rw [ENNReal.ofReal_mul δ_mul_const_pos.le, ← ENNReal.ofReal_rpow_of_nonneg ENNReal.toReal_nonneg (by norm_num), ENNReal.ofReal_toReal E'volume.ne]
    apply mul_nonneg δ_mul_const_pos.le
    apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg
  _ = ε := by
    rw [ε'def, C_control_approximation_effect_eq hε.1.le, add_sub_cancel_right, mul_div_cancel₀,
        div_mul_eq_div_div, div_self, one_div, Real.inv_rpow, ← Real.rpow_mul, inv_mul_cancel, Real.rpow_one, inv_div]
    ring
    norm_num
    apply div_nonneg <;> linarith [hε.1]
    apply Real.rpow_nonneg
    apply div_nonneg <;> linarith [hε.1]
    exact δ_mul_const_pos.ne.symm
    exact Real.pi_pos.ne.symm
Proof state after:
no goals