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' < ⊤
⊢ MeasureTheory.volume.real E ≤ ε
Tactic:
have : ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by
  calc ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E'
  _ = ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' := by
    congr
    rw [← ENNReal.ofReal_ofNat, ← ENNReal.ofReal_div_of_pos (by norm_num)]
    ring_nf
  _ ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by
    rcases h with hE' | hE' <;>
    . apply rcarleson_exceptional_set_estimate_specific hδ  _ measurableSetE' hE'
      intro x
      rw [fdef, ← Fdef]
      simp (config := { failIfUnchanged := false }) only [RCLike.star_def, Function.comp_apply,
        map_mul, norm_mul, RingHomIsometric.is_iso]
      rw [norm_indicator_eq_indicator_norm]
      simp only [norm_eq_abs, Pi.one_apply, norm_one]
      rw [Set.indicator_apply, Set.indicator_apply]
      split_ifs with inF
      . simp
        exact h_bound x inF
      . simp
Proof state after:
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⁻¹
⊢ MeasureTheory.volume.real E ≤ ε