internlm/Lean-Github huggingface dataset:
Theorem: fourierCoeffOn_bound
Proof state before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.I * ↑n * ↑x = Complex.I * ↑n * ↑x
Tactic:
ring
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ↑Real.pi ≠ 0
Tactic:
simp
Proof state after:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ¬Real.pi = 0
Theorem: fourierCoeffOn_bound
Proof state before:
case e_a.e_f.h.e_a.h.e_6.h.e_z
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ¬Real.pi = 0
Tactic:
exact Real.pi_pos.ne.symm
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ‖∫ (x : ℝ) in 0 ..2 * Real.pi, (starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x‖ ≤
    ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x‖
Tactic:
apply intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(starRingEnd ℂ) (Complex.I * ↑n * ↑x).exp * f x‖ =
    ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(Complex.I * ↑n * ↑x).exp * f x‖
Tactic:
simp
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖(Complex.I * ↑n * ↑x).exp * f x‖ = ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖f x‖
Tactic:
congr
Proof state after:
case e_f
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (fun x => ‖(Complex.I * ↑n * ↑x).exp * f x‖) = fun x => ‖f x‖
Theorem: fourierCoeffOn_bound
Proof state before:
case e_f
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (fun x => ‖(Complex.I * ↑n * ↑x).exp * f x‖) = fun x => ‖f x‖
Tactic:
ext x
Proof state after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ‖(Complex.I * ↑n * ↑x).exp * f x‖ = ‖f x‖
Theorem: fourierCoeffOn_bound
Proof state before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ ‖(Complex.I * ↑n * ↑x).exp * f x‖ = ‖f x‖
Tactic:
simp only [norm_mul, Complex.norm_eq_abs]
Proof state after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (Complex.I * ↑n * ↑x).exp * Complex.abs (f x) = Complex.abs (f x)
Theorem: fourierCoeffOn_bound
Proof state before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (Complex.I * ↑n * ↑x).exp * Complex.abs (f x) = Complex.abs (f x)
Tactic:
rw [mul_assoc, mul_comm Complex.I]
Proof state after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑n * ↑x * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)
Theorem: fourierCoeffOn_bound
Proof state before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑n * ↑x * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)
Tactic:
norm_cast
Proof state after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑(↑n * x) * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)
Theorem: fourierCoeffOn_bound
Proof state before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ Complex.abs (↑(↑n * x) * Complex.I).exp * Complex.abs (f x) = Complex.abs (f x)
Tactic:
rw [Complex.abs_exp_ofReal_mul_I]
Proof state after:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.abs (f x) = Complex.abs (f x)
Theorem: fourierCoeffOn_bound
Proof state before:
case e_f.h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
⊢ 1 * Complex.abs (f x) = Complex.abs (f x)
Tactic:
ring
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, ‖f x‖ ≤ ∫ (x : ℝ) in 0 ..2 * Real.pi, C
Tactic:
apply intervalIntegral.integral_mono_on
Proof state after:
case hab
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 0 ≤ 2 * Real.pi

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Theorem: fourierCoeffOn_bound
Proof state before:
case hab
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 0 ≤ 2 * Real.pi

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. exact Real.two_pi_pos.le
Proof state after:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Theorem: fourierCoeffOn_bound
Proof state before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)

case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. rw [IntervalIntegrable.intervalIntegrable_norm_iff]
  
  . apply f_continuous.intervalIntegrable
  . apply f_continuous.aestronglyMeasurable
Proof state after:
case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Theorem: fourierCoeffOn_bound
Proof state before:
case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)

case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. apply intervalIntegrable_const
Proof state after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Theorem: fourierCoeffOn_bound
Proof state before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
. intro x hx
  rw [Complex.norm_eq_abs]
  exact f_bounded x hx
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
case hab
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 0 ≤ 2 * Real.pi
Tactic:
exact Real.two_pi_pos.le
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => ‖f u‖) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
rw [IntervalIntegrable.intervalIntegrable_norm_iff]
Proof state after:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => f u) MeasureTheory.volume 0 (2 * Real.pi)

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Theorem: fourierCoeffOn_bound
Proof state before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => f u) MeasureTheory.volume 0 (2 * Real.pi)

case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Tactic:
. apply f_continuous.intervalIntegrable
Proof state after:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Theorem: fourierCoeffOn_bound
Proof state before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Tactic:
. apply f_continuous.aestronglyMeasurable
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => f u) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply f_continuous.intervalIntegrable
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
case hf
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ MeasureTheory.AEStronglyMeasurable (fun u => f u) (MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)))
Tactic:
apply f_continuous.aestronglyMeasurable
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
case hg
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ IntervalIntegrable (fun u => C) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply intervalIntegrable_const
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x‖ ≤ C
Tactic:
intro x hx
Proof state after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ ‖f x‖ ≤ C
Theorem: fourierCoeffOn_bound
Proof state before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ ‖f x‖ ≤ C
Tactic:
rw [Complex.norm_eq_abs]
Proof state after:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ C
Theorem: fourierCoeffOn_bound
Proof state before:
case h
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
⊢ Complex.abs (f x) ≤ C
Tactic:
exact f_bounded x hx
Proof state after:
no goals
Theorem: fourierCoeffOn_bound
Proof state before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ ∫ (x : ℝ) in 0 ..2 * Real.pi, C = C * (2 * Real.pi)
Tactic:
rw [intervalIntegral.integral_const]
Proof state after:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (2 * Real.pi - 0) • C = C * (2 * Real.pi)
Theorem: fourierCoeffOn_bound
Proof state before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ (2 * Real.pi - 0) • C = C * (2 * Real.pi)
Tactic:
simp
Proof state after:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 2 * Real.pi * C = C * (2 * Real.pi)
Theorem: fourierCoeffOn_bound
Proof state before:
f : ℝ → ℂ
f_continuous : Continuous f
C : ℝ
f_bounded : ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C
n : ℤ
⊢ 2 * Real.pi * C = C * (2 * Real.pi)
Tactic:
ring
Proof state after:
no goals
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
⊢ Function.Periodic (deriv f) T
Tactic:
intro x
Proof state after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
⊢ deriv f (x + T) = deriv f x
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
⊢ deriv f (x + T) = deriv f x
Tactic:
set g : 𝕜 → 𝕜 := fun x ↦ x + T with gdef
Proof state after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
⊢ deriv f (x + T) = deriv f x
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
⊢ deriv f (x + T) = deriv f x
Tactic:
have diff_g : Differentiable 𝕜 g := by
  apply differentiable_id.add_const
Proof state after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv f (x + T) = deriv f x
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv f (x + T) = deriv f x
Tactic:
have : deriv (f ∘ g) x = ((deriv f) ∘ g) x := by
  calc deriv (f ∘ g) x
    _ = deriv g x • deriv f (g x) := deriv.scomp x (diff_f.differentiable (by norm_num)).differentiableAt diff_g.differentiableAt
    _ = deriv f (g x) := by rw [gdef, deriv_add_const, deriv_id'']; simp
Proof state after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ g) x = (deriv f ∘ g) x
⊢ deriv f (x + T) = deriv f x
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ g) x = (deriv f ∘ g) x
⊢ deriv f (x + T) = deriv f x
Tactic:
rw [gdef] at this
Proof state after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = (deriv f ∘ fun x => x + T) x
⊢ deriv f (x + T) = deriv f x
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = (deriv f ∘ fun x => x + T) x
⊢ deriv f (x + T) = deriv f x
Tactic:
simp at this
Proof state after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ deriv f (x + T) = deriv f x
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ deriv f (x + T) = deriv f x
Tactic:
convert this.symm
Proof state after:
case h.e'_3.h.e'_6
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ f = f ∘ fun x => x + T
Theorem: periodic_deriv
Proof state before:
case h.e'_3.h.e'_6
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ f = f ∘ fun x => x + T
Tactic:
ext y
Proof state after:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = (f ∘ fun x => x + T) y
Theorem: periodic_deriv
Proof state before:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = (f ∘ fun x => x + T) y
Tactic:
simp
Proof state after:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = f (y + T)
Theorem: periodic_deriv
Proof state before:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = f (y + T)
Tactic:
exact (periodic_f y).symm
Proof state after:
no goals
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
⊢ Differentiable 𝕜 g
Tactic:
apply differentiable_id.add_const
Proof state after:
no goals
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv (f ∘ g) x = (deriv f ∘ g) x
Tactic:
calc deriv (f ∘ g) x
  _ = deriv g x • deriv f (g x) := deriv.scomp x (diff_f.differentiable (by norm_num)).differentiableAt diff_g.differentiableAt
  _ = deriv f (g x) := by rw [gdef, deriv_add_const, deriv_id'']; simp
Proof state after:
no goals
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ 1 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: periodic_deriv
Proof state before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv g x • deriv f (g x) = deriv f (g x)
Tactic:
rw [gdef, deriv_add_const, deriv_id'']
Proof state after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ (fun x => 1) x • deriv f ((fun x => x + T) x) = deriv f ((fun x => x + T) x)