internlm/Lean-Github huggingface dataset:
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)
ε' : ℝ := 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
⊢ MeasureTheory.volume (Set.Icc 0 (2 * Real.pi)) = ENNReal.ofReal (2 * Real.pi)
Tactic:
rw [Real.volume_Icc, sub_zero]
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)
ε' : ℝ := 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' < ⊤
⊢ ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤
    ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E' ^ 2⁻¹
Tactic:
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:
no goals
Theorem: control_approximation_effect'
Proof state before:
case e_a
ε : ℝ
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' < ⊤
⊢ ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) = ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi) / 2)
Tactic:
ring_nf
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)
ε' : ℝ := 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' < ⊤
⊢ 0 < 2
Tactic:
norm_num
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)
ε' : ℝ := 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' < ⊤
⊢ ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' ≤
    ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E' ^ 2⁻¹
Tactic:
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:
no goals
Theorem: control_approximation_effect'
Proof state before:
case inr
ε : ℝ
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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
⊢ ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' ≤
    ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E' ^ 2⁻¹
Tactic:
apply rcarleson_exceptional_set_estimate_specific hδ  _ measurableSetE' hE'
Proof state after:
ε : ℝ
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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
⊢ ∀ (x : ℝ), ‖(star ∘ f) x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 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)
ε' : ℝ := 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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
⊢ ∀ (x : ℝ), ‖(star ∘ f) x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
Tactic:
intro x
Proof state after:
ε : ℝ
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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
x : ℝ
⊢ ‖(star ∘ f) x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 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)
ε' : ℝ := 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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
x : ℝ
⊢ ‖(star ∘ f) x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
Tactic:
rw [fdef, ← Fdef]
Proof state after:
ε : ℝ
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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
x : ℝ
⊢ ‖(star ∘ fun x => h x * F.indicator 1 x) x‖ ≤ δ * F.indicator 1 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)
ε' : ℝ := 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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
x : ℝ
⊢ ‖(star ∘ fun x => h x * F.indicator 1 x) x‖ ≤ δ * F.indicator 1 x
Tactic:
simp (config := { failIfUnchanged := false }) only [RCLike.star_def, Function.comp_apply,
  map_mul, norm_mul, RingHomIsometric.is_iso]
Proof state after:
ε : ℝ
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'
E'volume : MeasureTheory.volume E' < ⊤
hE' : ∀ x ∈ E', ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 ≤ T' (star ∘ f) x
x : ℝ
⊢ ‖h x‖ * ‖F.indicator 1 x‖ ≤ δ * F.indicator 1 x