theorem Icc_to_ii (f : ℝ → ℝ) : ∫ (x : ℝ) in Set.Icc 0 1, f x = ∫ (x : ℝ) in 0..1, f x

theorem sin_2pi_m (m : ℤ) : Real.sin (↑m * (2 * Real.pi)) = 0

theorem ics (c : ℝ) (hc : c ≠ 0) : ∫ (x : ℝ) in 0..1, Real.cos (c * x) = Real.sin c / c

theorem iss (c : ℝ) (hc : c ≠ 0) : ∫ (x : ℝ) in 0..1, Real.sin (c * x) = (1 - Real.cos c) / c

theorem two_pi_ne (m : ℤ) (hm : m ≠ 0) : 2 * Real.pi * ↑m ≠ 0

theorem ic0 (m : ℤ) (hm : m ≠ 0) : ∫ (x : ℝ) in 0..1, Real.cos (2 * Real.pi * ↑m * x) = 0

theorem is0 (m : ℤ) (hm : m ≠ 0) : ∫ (x : ℝ) in 0..1, Real.sin (2 * Real.pi * ↑m * x) = 0

theorem ics2 (m : ℤ) (hm : m ≠ 0) : ∫ (x : ℝ) in 0..1, Real.cos (2 * Real.pi * ↑m * x) ^ 2 = 1 / 2

theorem iss2 (m : ℤ) (hm : m ≠ 0) : ∫ (x : ℝ) in 0..1, Real.sin (2 * Real.pi * ↑m * x) ^ 2 = 1 / 2

theorem tb_one (x : ℝ) : Chapter3.trigBasis 1 x = 1

theorem tb_even (m : ℕ) (hm : 0 < m) (x : ℝ) : Chapter3.trigBasis (2 * m) x = √2 * Real.cos (2 * Real.pi * ↑m * x)

theorem tb_odd (m : ℕ) (hm : 0 < m) (x : ℝ) : Chapter3.trigBasis (2 * m + 1) x = √2 * Real.sin (2 * Real.pi * ↑m * x)

theorem nat_tri (j : ℕ) (hj : 0 < j) : j = 1 ∨ (∃ (m : ℕ), 0 < m ∧ j = 2 * m) ∨ ∃ (m : ℕ), 0 < m ∧ j = 2 * m + 1

theorem icc0_nat (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmn : m ≠ n) : ∫ (x : ℝ) in 0..1, Real.cos (2 * Real.pi * ↑m * x) * Real.cos (2 * Real.pi * ↑n * x) = 0

theorem iss0_nat (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmn : m ≠ n) : ∫ (x : ℝ) in 0..1, Real.sin (2 * Real.pi * ↑m * x) * Real.sin (2 * Real.pi * ↑n * x) = 0

theorem isc0_nat (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : ∫ (x : ℝ) in 0..1, Real.sin (2 * Real.pi * ↑m * x) * Real.cos (2 * Real.pi * ↑n * x) = 0

theorem trigBasis_L2_orthonormal' (j k : ℕ) (hj : 0 < j) (hk : 0 < k) : ∫ (x : ℝ) in Set.Icc 0 1, Chapter3.trigBasis j x * Chapter3.trigBasis k x = if j = k then 1 else 0