internlm/Lean-Github huggingface dataset:
Theorem: fourierCoeffOn_add
Proof state before:
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
Tactic:
ring
Proof state after:
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 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:
. apply hf.continuousOn_mul
  apply Continuous.continuousOn
  continuity
Proof state after:
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 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:
. apply hg.continuousOn_mul
  apply Continuous.continuousOn
  continuity
Proof state after:
no goals
Theorem: fourierCoeffOn_add
Proof state before:
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
Tactic:
apply hf.continuousOn_mul
Proof state after:
case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)
Theorem: fourierCoeffOn_add
Proof state before:
case hf
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)
Tactic:
apply Continuous.continuousOn
Proof state after:
case hf.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp
Theorem: fourierCoeffOn_add
Proof state before:
case hf.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp
Tactic:
continuity
Proof state after:
no goals
Theorem: fourierCoeffOn_add
Proof state before:
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:
apply hg.continuousOn_mul
Proof state after:
case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)
Theorem: fourierCoeffOn_add
Proof state before:
case hg
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ ContinuousOn (fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp) (Set.uIcc a b)
Tactic:
apply Continuous.continuousOn
Proof state after:
case hg.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp
Theorem: fourierCoeffOn_add
Proof state before:
case hg.h
a b : ℝ
hab : a < b
f g : ℝ → ℂ
n : ℤ
hf : IntervalIntegrable f MeasureTheory.volume a b
hg : IntervalIntegrable g MeasureTheory.volume a b
⊢ Continuous fun x => (starRingEnd ℂ) (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (↑b - ↑a)).exp
Tactic:
continuity
Proof state after:
no goals
Theorem: fourierCoeffOn_sub
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:
rw [sub_eq_add_neg, fourierCoeffOn_add hf hg.neg, fourierCoeffOn_neg, ← sub_eq_add_neg]
Proof state after:
no goals
Theorem: partialFourierSum_add
Proof state before:
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
⊢ partialFourierSum (f + g) N = partialFourierSum f N + partialFourierSum g N
Tactic:
ext x
Proof state after:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f + g) N x = (partialFourierSum f N + partialFourierSum g N) x
Theorem: partialFourierSum_add
Proof state before:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f + g) N x = (partialFourierSum f N + partialFourierSum g N) x
Tactic:
simp [partialFourierSum, partialFourierSum, partialFourierSum, ← sum_add_distrib]
Proof state after:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ ∑ x_1 ∈ Icc (-↑N) ↑N,
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp =
    ∑ x_1 ∈ Icc (-↑N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
        fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp)
Theorem: partialFourierSum_add
Proof state before:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ ∑ x_1 ∈ Icc (-↑N) ↑N,
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp =
    ∑ x_1 ∈ Icc (-↑N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
        fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp)
Tactic:
congr
Proof state after:
case h.e_f
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ (fun x_1 =>
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp) =
    fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp
Theorem: partialFourierSum_add
Proof state before:
case h.e_f
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ (fun x_1 =>
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp) =
    fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp
Tactic:
ext n
Proof state after:
case h.e_f.h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (f + g) n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp =
    fourierCoeffOn Real.two_pi_pos f n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp
Theorem: partialFourierSum_add
Proof state before:
case h.e_f.h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (f + g) n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp =
    fourierCoeffOn Real.two_pi_pos f n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp
Tactic:
rw [fourierCoeffOn_add hf hg, add_mul]
Proof state after:
no goals
Theorem: partialFourierSum_sub
Proof state before:
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
⊢ partialFourierSum (f - g) N = partialFourierSum f N - partialFourierSum g N
Tactic:
ext x
Proof state after:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f - g) N x = (partialFourierSum f N - partialFourierSum g N) x
Theorem: partialFourierSum_sub
Proof state before:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f - g) N x = (partialFourierSum f N - partialFourierSum g N) x
Tactic:
simp only [Pi.sub_apply]
Proof state after:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f - g) N x = partialFourierSum f N x - partialFourierSum g N x
Theorem: partialFourierSum_sub
Proof state before:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f - g) N x = partialFourierSum f N x - partialFourierSum g N x
Tactic:
rw [partialFourierSum, partialFourierSum, partialFourierSum, ←sum_sub_distrib]
Proof state after:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x =
    ∑ x_1 ∈ Icc (-Int.ofNat N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x -
        fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑x)
Theorem: partialFourierSum_sub
Proof state before:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x =
    ∑ x_1 ∈ Icc (-Int.ofNat N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x -
        fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑x)
Tactic:
congr
Proof state after:
case h.e_f
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x) = fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x - fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑x
Theorem: partialFourierSum_sub
Proof state before:
case h.e_f
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x) = fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x - fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑x
Tactic:
ext n
Proof state after:
case h.e_f.h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x =
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x - fourierCoeffOn Real.two_pi_pos g n * (fourier n) ↑x
Theorem: partialFourierSum_sub
Proof state before:
case h.e_f.h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x =
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x - fourierCoeffOn Real.two_pi_pos g n * (fourier n) ↑x
Tactic:
rw [fourierCoeffOn_sub hf hg, sub_mul]
Proof state after:
no goals
Theorem: partialFourierSum_mul
Proof state before:
f : ℝ → ℂ
a : ℂ
N : ℕ
⊢ partialFourierSum (fun x => a * f x) N = fun x => a * partialFourierSum f N x
Tactic:
ext x
Proof state after:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum (fun x => a * f x) N x = a * partialFourierSum f N x
Theorem: partialFourierSum_mul
Proof state before:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum (fun x => a * f x) N x = a * partialFourierSum f N x
Tactic:
rw [partialFourierSum, partialFourierSum, mul_sum]
Proof state after:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    ∑ i ∈ Icc (-Int.ofNat N) ↑N, a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)
Theorem: partialFourierSum_mul
Proof state before:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    ∑ i ∈ Icc (-Int.ofNat N) ↑N, a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)
Tactic:
congr
Proof state after:
case h.e_f
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x) = fun i =>
    a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)
Theorem: partialFourierSum_mul
Proof state before:
case h.e_f
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x) = fun i =>
    a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)
Tactic:
ext n
Proof state after:
case h.e_f.h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    a * (fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x)
Theorem: partialFourierSum_mul
Proof state before:
case h.e_f.h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    a * (fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x)
Tactic:
rw [fourierCoeffOn_mul, mul_assoc]
Proof state after:
no goals
Theorem: fourier_periodic
Proof state before:
n : ℤ
⊢ Function.Periodic (fun x => (fourier n) ↑x) (2 * Real.pi)
Tactic:
simp
Proof state after:
no goals
Theorem: partialFourierSum_periodic
Proof state before:
f : ℝ → ℂ
N : ℕ
⊢ Function.Periodic (partialFourierSum f N) (2 * Real.pi)
Tactic:
rw [Function.Periodic]
Proof state after:
f : ℝ → ℂ
N : ℕ
⊢ ∀ (x : ℝ), partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x
Theorem: partialFourierSum_periodic
Proof state before:
f : ℝ → ℂ
N : ℕ
⊢ ∀ (x : ℝ), partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x
Tactic:
intro x
Proof state after:
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x
Theorem: partialFourierSum_periodic
Proof state before:
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x
Tactic:
rw [partialFourierSum, partialFourierSum]
Proof state after:
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi) =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x
Theorem: partialFourierSum_periodic
Proof state before:
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi) =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x
Tactic:
congr
Proof state after:
case e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi)) = fun n =>
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x
Theorem: partialFourierSum_periodic
Proof state before:
case e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi)) = fun n =>
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x
Tactic:
ext n
Proof state after:
case e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi) =
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x
Theorem: partialFourierSum_periodic
Proof state before:
case e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi) =
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x
Tactic:
congr 1
Proof state after:
case e_f.h.e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ (fourier n) ↑(x + 2 * Real.pi) = (fourier n) ↑x
Theorem: partialFourierSum_periodic
Proof state before:
case e_f.h.e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ (fourier n) ↑(x + 2 * Real.pi) = (fourier n) ↑x
Tactic:
exact fourier_periodic x
Proof state after:
no goals
Theorem: fourier_uniformContinuous
Proof state before:
n : ℤ
⊢ UniformContinuous fun x => (fourier n) ↑x
Tactic:
simp [fourier]
Proof state after:
n : ℤ
⊢ UniformContinuous fun x => (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp
Theorem: fourier_uniformContinuous
Proof state before:
n : ℤ
⊢ UniformContinuous fun x => (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp
Tactic:
sorry
Proof state after:
no goals
Theorem: partialFourierSum_uniformContinuous
Proof state before:
f : ℝ → ℂ
N : ℕ
⊢ UniformContinuous (partialFourierSum f N)
Tactic:
sorry
Proof state after:
no goals
Theorem: strictConvexOn_cos_Icc
Proof state before:
⊢ StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)) Real.cos
Tactic:
apply strictConvexOn_of_deriv2_pos (convex_Icc _ _) Real.continuousOn_cos fun x hx => ?_
Proof state after:
x : ℝ
hx : x ∈ interior (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2))
⊢ 0 < deriv^[2] Real.cos x
Theorem: strictConvexOn_cos_Icc
Proof state before:
x : ℝ
hx : x ∈ interior (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2))
⊢ 0 < deriv^[2] Real.cos x
Tactic:
rw [interior_Icc] at hx
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo (Real.pi / 2) (Real.pi + Real.pi / 2)
⊢ 0 < deriv^[2] Real.cos x
Theorem: strictConvexOn_cos_Icc
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo (Real.pi / 2) (Real.pi + Real.pi / 2)
⊢ 0 < deriv^[2] Real.cos x
Tactic:
simp [Real.cos_neg_of_pi_div_two_lt_of_lt hx.1 hx.2]
Proof state after:
no goals
Theorem: lower_secant_bound'
Proof state before:
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
by_cases ηpos : η ≤ 0
Proof state after:
case pos
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : ¬η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
case pos
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : ¬η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
. calc (2 / Real.pi) * η
  _ ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (div_nonneg zero_le_two Real.pi_pos.le) ηpos
  _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg
Proof state after:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : ¬η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : ¬η ≤ 0
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
push_neg at ηpos
Proof state after:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
case neg
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
wlog x_nonneg : 0 ≤ x generalizing x
Proof state after:
case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
case neg.inr
η x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
ηpos : 0 < η
this : ∀ {x : ℝ}, η ≤ |x| → |x| ≤ 2 * Real.pi - η → 0 ≤ x → 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
x_nonneg : ¬0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖

η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
. convert (@this (-x) _ (by simpa) (by linarith)) using 1
  . rw [Complex.norm_eq_abs, ←Complex.abs_conj, map_sub, map_one, Complex.ofReal_neg, mul_neg, Complex.norm_eq_abs,
        ←Complex.exp_conj, map_mul, Complex.conj_I, neg_mul, Complex.conj_ofReal]
  . rwa [abs_neg]
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Theorem: lower_secant_bound'
Proof state before:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ |x|
abs_x_le : |x| ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖
Tactic:
rw [abs_of_nonneg x_nonneg] at *
Proof state after:
η : ℝ
ηpos : 0 < η
x : ℝ
le_abs_x : η ≤ x
abs_x_le : x ≤ 2 * Real.pi - η
x_nonneg : 0 ≤ x
⊢ 2 / Real.pi * η ≤ ‖1 - (Complex.I * ↑x).exp‖