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
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 * δ)
⊢ ENNReal.ofReal 2 * MeasureTheory.volume E' ≠ ⊤
Tactic:
apply ENNReal.mul_ne_top ENNReal.ofReal_ne_top E'volume.ne
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' < ⊤
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 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: control_approximation_effect'
Proof state before:
case e_a.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' < ⊤
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 * δ)
⊢ 1 = (1 + -2⁻¹) * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: control_approximation_effect'
Proof state before:
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 * δ)
⊢ 0 ≤ MeasureTheory.volume.real E' ^ 2⁻¹
Tactic:
apply Real.rpow_nonneg MeasureTheory.measureReal_nonneg
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' < ⊤
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 * δ)
⊢ 1 + -2⁻¹ ≠ 0
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' < ⊤
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 ≤ 2⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: control_approximation_effect'
Proof state before:
case hb
ε : ℝ
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 ≠ 0
Tactic:
exact Real.pi_pos.ne.symm
Proof state after:
no goals
Theorem: prop2_2
Proof state before:
X : Type u_1
A : ℝ
inst✝⁶ : MetricSpace X
inst✝⁵ : IsSpaceOfHomogeneousType X A
inst✝⁴ : Inhabited X
τ q D κ ε C₀ C t : ℝ
Θ : Set C(X, ℂ)
inst✝³ : IsCompatible Θ
inst✝² : IsCancellative τ Θ
inst✝¹ : TileStructure Θ D κ C₀
F G : Set X
σ σ' : X → ℤ
Q' : X → C(X, ℂ)
K : X → X → ℂ
inst✝ : IsCZKernel τ K
ψ : ℝ → ℝ
𝔄 : Set (𝔓 X)
hA : 1 < A
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hC₀ : 0 < C₀
hC : C2_2 A τ q C₀ < C
hD : D2_2 A τ q C₀ < D
hκ : κ ∈ Ioo 0 (κ2_2 A τ q C₀)
hε : ε ∈ Ioo 0 (ε2_2 A τ q C₀)
hF : MeasurableSet F
hG : MeasurableSet G
h2F : volume F ∈ Ioo 0 ⊤
h2G : volume G ∈ Ioo 0 ⊤
Q'_mem : ∀ (x : X), Q' x ∈ Θ
m_Q' : Measurable Q'
m_σ : Measurable σ
m_σ' : Measurable σ'
hT : NormBoundedBy (ANCZOperatorLp 2 K) 1
hψ : LipschitzWith (Cψ2_2 A τ q C₀) ψ
h2ψ : support ψ ⊆ Icc (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ᶠ (s : ℤ), ψ (D ^ s * x) = 1
ht : t ∈ Ioc 0 1
h𝔄 : IsAntichain (fun x x_1 => x ≤ x_1) 𝔄
h2𝔄 : 𝔄 ⊆ boundedTiles F t
h3𝔄 : 𝔄.Finite
⊢ ↑‖∑ᶠ (p : 𝔓 X) (_ : p ∈ 𝔄), TL K Q' σ σ' ψ p F‖₊ ≤ C * density G Q' 𝔄 ^ ε * t ^ (1 / q - 1 / 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: fourierCoeffOn_mul
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ fourierCoeffOn hab (fun x => c * f x) n = c * fourierCoeffOn hab f n
Tactic:
simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
  fourier_coe_apply', Complex.ofReal_sub, smul_eq_mul, Complex.real_smul, Complex.ofReal_inv]
Proof state after:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    c * ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
Theorem: fourierCoeffOn_mul
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    c * ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
Tactic:
rw [← mul_assoc, mul_comm c, mul_assoc _ c, mul_comm c, ← intervalIntegral.integral_mul_const]
Proof state after:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Theorem: fourierCoeffOn_mul
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Tactic:
congr
Proof state after:
case e_a.e_f
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Theorem: fourierCoeffOn_mul
Proof state before:
case e_a.e_f
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Tactic:
ext x
Proof state after:
case e_a.e_f.h
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Theorem: fourierCoeffOn_mul
Proof state before:
case e_a.e_f.h
a b : ℝ
hab : a < b
f : ℝ → ℂ
c : ℂ
n : ℤ
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (c * f x) =
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x * c
Tactic:
ring
Proof state after:
no goals
Theorem: fourierCoeffOn_neg
Proof state before:
a b : ℝ
hab : a < b
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeffOn hab (-f) n = -fourierCoeffOn hab f n
Tactic:
simp [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
Proof state after:
no goals
Theorem: fourierCoeffOn_add
Proof state before:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ fourierCoeffOn hab (f + g) n = fourierCoeffOn hab f n + fourierCoeffOn hab g n
Tactic:
simp only [fourierCoeffOn_eq_integral, one_div, fourier_apply, neg_smul, fourier_neg',
  fourier_coe_apply', Complex.ofReal_sub, Pi.add_apply, smul_eq_mul, Complex.real_smul,
  Complex.ofReal_inv]
Proof state after:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x) +
      (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x
Theorem: fourierCoeffOn_add
Proof state before:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    ((↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x) +
      (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x
Tactic:
rw [← mul_add, ← intervalIntegral.integral_add]
Proof state after:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    (↑b - ↑a)⁻¹ *
      ∫ (x : ℝ) in a..b,
        (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Theorem: fourierCoeffOn_add
Proof state before:
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (↑b - ↑a)⁻¹ * ∫ (x : ℝ) in a..b, (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    (↑b - ↑a)⁻¹ *
      ∫ (x : ℝ) in a..b,
        (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
          (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Tactic:
congr
Proof state after:
case e_a.e_f
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
      (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Theorem: fourierCoeffOn_add
Proof state before:
case e_a.e_f
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x)) = fun x =>
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
      (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b
Tactic:
ext x
Proof state after:
case e_a.e_f.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
x : ℝ
⊢ (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * (f x + g x) =
    (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x +
      (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x

case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * f x)
    MeasureTheory.volume a b

case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ IntervalIntegrable (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp * g x)
    MeasureTheory.volume a b