[GOAL]
R : Type u
inst✝¹ : AddMonoid R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
⊢ ↑ψ 0 = 1
[PROOFSTEP]
rw [coe_to_fun_apply, ofAdd_zero, map_one]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
x y : R
⊢ ↑ψ (x + y) = ↑ψ x * ↑ψ y
[PROOFSTEP]
rw [coe_to_fun_apply, coe_to_fun_apply _ x, coe_to_fun_apply _ y, ofAdd_add, map_mul]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
n : ℕ
x : R
⊢ ↑ψ (n • x) = ↑ψ x ^ n
[PROOFSTEP]
rw [coe_to_fun_apply, coe_to_fun_apply _ x, ofAdd_nsmul, map_pow]
[GOAL]
R : Type u
inst✝² : AddCommGroup R
R'✝ : Type v
inst✝¹ : CommMonoid R'✝
R' : Type v
inst✝ : CommGroup R'
ψ : AddChar R R'
n : ℤ
x : R
⊢ ↑ψ (n • x) = ↑ψ x ^ n
[PROOFSTEP]
rw [coe_to_fun_apply, coe_to_fun_apply _ x, ofAdd_zsmul, map_zpow]
[GOAL]
R : Type u
inst✝¹ : AddCommGroup R
R' : Type v
inst✝ : CommMonoid R'
src✝ : CommMonoid (Multiplicative R →* R') := MonoidHom.commMonoid
ψ : AddChar R R'
⊢ ψ⁻¹ * ψ = 1
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : AddCommGroup R
R' : Type v
inst✝ : CommMonoid R'
src✝ : CommMonoid (Multiplicative R →* R') := MonoidHom.commMonoid
ψ : AddChar R R'
x : R
⊢ ↑(ψ⁻¹ * ψ) x = ↑1 x
[PROOFSTEP]
rw [AddChar.mul_apply, AddChar.one_apply, inv_apply, ← map_add_mul, add_left_neg, map_zero_one]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ IsNontrivial ψ ↔ ψ ≠ 1
[PROOFSTEP]
refine' not_forall.symm.trans (Iff.not _)
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ (∀ (x : R), ↑ψ x = 1) ↔ ψ = 1
[PROOFSTEP]
rw [FunLike.ext_iff]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ (∀ (x : R), ↑ψ x = 1) ↔ ∀ (x : Multiplicative R), ↑ψ x = ↑1 x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ ψ⁻¹ = mulShift ψ (-1)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
x✝ : R
⊢ ↑ψ⁻¹ x✝ = ↑(mulShift ψ (-1)) x✝
[PROOFSTEP]
rw [inv_apply, mulShift_apply, neg_mul, one_mul]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
n : ℕ
x : R
⊢ ↑(mulShift ψ ↑n) x = ↑ψ x ^ n
[PROOFSTEP]
rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_pow]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
n : ℕ
⊢ ψ ^ n = mulShift ψ ↑n
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
n : ℕ
x : R
⊢ ↑(ψ ^ n) x = ↑(mulShift ψ ↑n) x
[PROOFSTEP]
rw [show (ψ ^ n) x = ψ x ^ n from rfl, ← mulShift_spec']
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
a b : R
⊢ mulShift ψ a * mulShift ψ b = mulShift ψ (a + b)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
a b x✝ : R
⊢ ↑(mulShift ψ a * mulShift ψ b) x✝ = ↑(mulShift ψ (a + b)) x✝
[PROOFSTEP]
rw [mulShift_apply, right_distrib, map_add_mul]
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
a b x✝ : R
⊢ ↑(mulShift ψ a * mulShift ψ b) x✝ = ↑ψ (a * x✝) * ↑ψ (b * x✝)
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ mulShift ψ 0 = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
x✝ : R
⊢ ↑(mulShift ψ 0) x✝ = ↑1 x✝
[PROOFSTEP]
rw [mulShift_apply, zero_mul, map_zero_one]
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
x✝ : R
⊢ 1 = ↑1 x✝
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ Function.Injective (mulShift ψ)
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ a = mulShift ψ b
⊢ a = b
[PROOFSTEP]
apply_fun fun x => x * mulShift ψ (-b) at h
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ a * mulShift ψ (-b) = mulShift ψ b * mulShift ψ (-b)
⊢ a = b
[PROOFSTEP]
simp only [mulShift_mul, mulShift_zero, add_right_neg] at h
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ (a + -b) = 1
⊢ a = b
[PROOFSTEP]
have h₂ := hψ (a + -b)
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ (a + -b) = 1
h₂ : a + -b ≠ 0 → IsNontrivial (mulShift ψ (a + -b))
⊢ a = b
[PROOFSTEP]
rw [h, isNontrivial_iff_ne_trivial, ← sub_eq_add_neg, sub_ne_zero] at h₂
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ (a + -b) = 1
h₂ : a ≠ b → 1 ≠ 1
⊢ a = b
[PROOFSTEP]
exact not_not.mp fun h => h₂ h rfl
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
hψ : IsNontrivial ψ
⊢ IsPrimitive ψ
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
hψ : IsNontrivial ψ
a : F
ha : a ≠ 0
⊢ IsNontrivial (mulShift ψ a)
[PROOFSTEP]
cases' hψ with x h
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
a : F
ha : a ≠ 0
x : F
h : ↑ψ x ≠ 1
⊢ IsNontrivial (mulShift ψ a)
[PROOFSTEP]
use a⁻¹ * x
[GOAL]
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
a : F
ha : a ≠ 0
x : F
h : ↑ψ x ≠ 1
⊢ ↑(mulShift ψ a) (a⁻¹ * x) ≠ 1
[PROOFSTEP]
rwa [mulShift_apply, mul_inv_cancel_left₀ ha]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
⊢ (fun a => ζ ^ ZMod.val (↑toAdd a)) 1 = 1
[PROOFSTEP]
simp only [toAdd_one, ZMod.val_zero, pow_zero]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
x y : Multiplicative (ZMod ↑n)
⊢ OneHom.toFun { toFun := fun a => ζ ^ ZMod.val (↑toAdd a), map_one' := (_ : ζ ^ ZMod.val 0 = 1) } (x * y) =
    OneHom.toFun { toFun := fun a => ζ ^ ZMod.val (↑toAdd a), map_one' := (_ : ζ ^ ZMod.val 0 = 1) } x *
      OneHom.toFun { toFun := fun a => ζ ^ ZMod.val (↑toAdd a), map_one' := (_ : ζ ^ ZMod.val 0 = 1) } y
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
x y : Multiplicative (ZMod ↑n)
⊢ ζ ^ ZMod.val (↑toAdd (x * y)) = ζ ^ ZMod.val (↑toAdd x) * ζ ^ ZMod.val (↑toAdd y)
[PROOFSTEP]
rw [toAdd_mul, ← pow_add, ZMod.val_add (toAdd x) (toAdd y), ← pow_eq_pow_mod _ hζ]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
a : ℕ
⊢ ↑(zmodChar n hζ) ↑a = ζ ^ a
[PROOFSTEP]
rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_nat_cast a]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
⊢ IsNontrivial ψ ↔ ↑ψ 1 ≠ 1
[PROOFSTEP]
refine' ⟨_, fun h => ⟨1, h⟩⟩
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
⊢ IsNontrivial ψ → ↑ψ 1 ≠ 1
[PROOFSTEP]
contrapose!
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
⊢ ↑ψ 1 = 1 → ¬IsNontrivial ψ
[PROOFSTEP]
rintro h₁ ⟨a, ha⟩
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
⊢ False
[PROOFSTEP]
have ha₁ : a = a.val • (1 : ZMod ↑n) := by rw [nsmul_eq_mul, mul_one]; exact (ZMod.nat_cast_zmod_val a).symm
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
⊢ a = ZMod.val a • 1
[PROOFSTEP]
rw [nsmul_eq_mul, mul_one]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
⊢ a = ↑(ZMod.val a)
[PROOFSTEP]
exact (ZMod.nat_cast_zmod_val a).symm
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
ha₁ : a = ZMod.val a • 1
⊢ False
[PROOFSTEP]
rw [ha₁, map_nsmul_pow, h₁, one_pow] at ha
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : 1 ≠ 1
ha₁ : a = ZMod.val a • 1
⊢ False
[PROOFSTEP]
exact ha rfl
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
hψ : IsPrimitive ψ
a : ZMod ↑n
⊢ ↑ψ a = 1 ↔ a = 0
[PROOFSTEP]
refine' ⟨fun h => not_imp_comm.mp (hψ a) _, fun ha => by rw [ha, map_zero_one]⟩
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
hψ : IsPrimitive ψ
a : ZMod ↑n
ha : a = 0
⊢ ↑ψ a = 1
[PROOFSTEP]
rw [ha, map_zero_one]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
hψ : IsPrimitive ψ
a : ZMod ↑n
h : ↑ψ a = 1
⊢ ¬IsNontrivial (mulShift ψ a)
[PROOFSTEP]
rw [zmod_char_isNontrivial_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
⊢ IsPrimitive ψ
[PROOFSTEP]
refine' fun a ha => (isNontrivial_iff_ne_trivial _).mpr fun hf => _
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
⊢ False
[PROOFSTEP]
have h : mulShift ψ a 1 = (1 : AddChar (ZMod n) C) (1 : ZMod n) := congr_fun (congr_arg (↑) hf) 1
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
h : ↑(mulShift ψ a) 1 = ↑1 1
⊢ False
[PROOFSTEP]
rw [mulShift_apply, mul_one] at h
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
h : ↑ψ a = ↑1 1
⊢ False
[PROOFSTEP]
norm_cast at h
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
h : ↑ψ a = ↑1 1
⊢ False
[PROOFSTEP]
exact ha (hψ a h)
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
⊢ IsPrimitive (zmodChar n (_ : ζ ^ ↑n = 1))
[PROOFSTEP]
apply zmod_char_primitive_of_eq_one_only_at_zero
[GOAL]
case hψ
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
⊢ ∀ (a : ZMod ↑n), ↑(zmodChar n (_ : ζ ^ ↑n = 1)) a = 1 → a = 0
[PROOFSTEP]
intro a ha
[GOAL]
case hψ
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
a : ZMod ↑n
ha : ↑(zmodChar n (_ : ζ ^ ↑n = 1)) a = 1
⊢ a = 0
[PROOFSTEP]
rw [zmodChar_apply, ← pow_zero ζ] at ha
[GOAL]
case hψ
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
a : ZMod ↑n
ha : ζ ^ ZMod.val a = ζ ^ 0
⊢ a = 0
[PROOFSTEP]
exact (ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) n.pos ha)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let p := ringChar F
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime F _⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let pp := p.toPNat hp.1.pos
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
have hp₂ : ¬ringChar F' ∣ p :=
  by
  cases' CharP.char_is_prime_or_zero F' (ringChar F') with hq hq
  · exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm
  · rw [hq]
    exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
⊢ ¬ringChar F' ∣ p
[PROOFSTEP]
cases' CharP.char_is_prime_or_zero F' (ringChar F') with hq hq
[GOAL]
case inl
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hq : Nat.Prime (ringChar F')
⊢ ¬ringChar F' ∣ p
[PROOFSTEP]
exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm
[GOAL]
case inr
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hq : ringChar F' = 0
⊢ ¬ringChar F' ∣ p
[PROOFSTEP]
rw [hq]
[GOAL]
case inr
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hq : ringChar F' = 0
⊢ ¬0 ∣ p
[PROOFSTEP]
exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let ψ := primitiveZModChar pp F' (neZero_iff.mp (NeZero.of_not_dvd F' hp₂))
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
letI : Algebra (ZMod p) F := ZMod.algebra _ _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let ψ' := ψ.char.comp (AddMonoidHom.toMultiplicative (Algebra.trace (ZMod p) F).toAddMonoidHom)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
have hψ' : IsNontrivial ψ' :=
  by
  obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero
  rw [one_mul] at ha
  exact ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
⊢ IsNontrivial ψ'
[PROOFSTEP]
obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero
[GOAL]
case intro
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
a : F
ha : ↑(Algebra.trace (ZMod (ringChar F)) F) (1 * a) ≠ 0
⊢ IsNontrivial ψ'
[PROOFSTEP]
rw [one_mul] at ha
[GOAL]
case intro
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
a : F
ha : ↑(Algebra.trace (ZMod (ringChar F)) F) a ≠ 0
⊢ IsNontrivial ψ'
[PROOFSTEP]
exact ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
hψ' : IsNontrivial ψ'
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
exact ⟨ψ.n, ψ', hψ'.isPrimitive⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : IsNontrivial ψ
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
rcases hψ with ⟨b, hb⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
have h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a := Fintype.sum_bijective _ (AddGroup.addLeft_bijective b) _ _ fun x => rfl
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ∑ a : R, ↑ψ (b + a) = ∑ a : R, ↑ψ a
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
simp_rw [map_add_mul] at h₁
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ∑ x : R, ↑ψ b * ↑ψ x = ∑ a : R, ↑ψ a
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
have h₂ : ∑ a : R, ψ a = Finset.univ.sum ↑ψ := rfl
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ∑ x : R, ↑ψ b * ↑ψ x = ∑ a : R, ↑ψ a
h₂ : ∑ a : R, ↑ψ a = Finset.sum Finset.univ ↑ψ
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
rw [← Finset.mul_sum, h₂] at h₁
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ↑ψ b * Finset.sum Finset.univ ↑ψ = Finset.sum Finset.univ ↑ψ
h₂ : ∑ a : R, ↑ψ a = Finset.sum Finset.univ ↑ψ
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
exact eq_zero_of_mul_eq_self_left hb h₁
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ¬IsNontrivial ψ
⊢ ∑ a : R, ↑ψ a = ↑(Fintype.card R)
[PROOFSTEP]
simp only [IsNontrivial] at hψ
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ¬∃ a, ↑ψ a ≠ 1
⊢ ∑ a : R, ↑ψ a = ↑(Fintype.card R)
[PROOFSTEP]
push_neg at hψ
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ∀ (a : R), ↑ψ a = 1
⊢ ∑ a : R, ↑ψ a = ↑(Fintype.card R)
[PROOFSTEP]
simp only [hψ, Finset.sum_const, Nat.smul_one_eq_coe]
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ∀ (a : R), ↑ψ a = 1
⊢ ↑(Finset.card Finset.univ) = ↑(Fintype.card R)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
⊢ ∑ x : R, ↑ψ (x * b) = ↑(if b = 0 then Fintype.card R else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : b = 0
⊢ ∑ x : R, ↑ψ (x * b) = ↑(Fintype.card R)
[PROOFSTEP]
simp only [h, mul_zero, map_zero_one, Finset.sum_const, Nat.smul_one_eq_coe]
[GOAL]
case pos
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : b = 0
⊢ ↑(Finset.card Finset.univ) = ↑(Fintype.card R)
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : ¬b = 0
⊢ ∑ x : R, ↑ψ (x * b) = ↑0
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
case neg
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : ¬b = 0
⊢ ∑ x : R, ↑ψ (b * x) = ↑0
[PROOFSTEP]
exact_mod_cast sum_eq_zero_of_isNontrivial (hψ b h)


[GOAL]
k : ℕ
⊢ bernoulliFun k 0 = ↑(bernoulli k)
[PROOFSTEP]
rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
[GOAL]
k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = bernoulliFun k 0
[PROOFSTEP]
rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
  bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]
[GOAL]
k : ℕ
⊢ bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0
[PROOFSTEP]
rw [bernoulliFun, bernoulliFun_eval_zero, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one]
[GOAL]
k : ℕ
⊢ ↑(algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + if k = 1 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
k : ℕ
h : k = 1
⊢ ↑(algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 1
[PROOFSTEP]
rw [h, bernoulli_one, bernoulli'_one, eq_ratCast]
[GOAL]
case pos
k : ℕ
h : k = 1
⊢ ↑(1 / 2) = ↑(-1 / 2) + 1
[PROOFSTEP]
push_cast
[GOAL]
case pos
k : ℕ
h : k = 1
⊢ 1 / ↑2 = -1 / ↑2 + 1
[PROOFSTEP]
ring
[GOAL]
case neg
k : ℕ
h : ¬k = 1
⊢ ↑(algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 0
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one h, add_zero, eq_ratCast]
[GOAL]
k : ℕ
x : ℝ
⊢ HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x
[PROOFSTEP]
convert ((Polynomial.bernoulli k).map <| algebraMap ℚ ℝ).hasDerivAt x using 1
[GOAL]
case h.e'_7
k : ℕ
x : ℝ
⊢ ↑k * bernoulliFun (k - 1) x =
    Polynomial.eval x (↑Polynomial.derivative (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))
[PROOFSTEP]
simp only [bernoulliFun, Polynomial.derivative_map, Polynomial.derivative_bernoulli k, Polynomial.map_mul,
  Polynomial.map_nat_cast, Polynomial.eval_mul, Polynomial.eval_nat_cast]
[GOAL]
k : ℕ
x : ℝ
⊢ HasDerivAt (fun x => bernoulliFun (k + 1) x / (↑k + 1)) (bernoulliFun k x) x
[PROOFSTEP]
convert (hasDerivAt_bernoulliFun (k + 1) x).div_const _ using 1
[GOAL]
case h.e'_7
k : ℕ
x : ℝ
⊢ bernoulliFun k x = ↑(k + 1) * bernoulliFun (k + 1 - 1) x / (↑k + 1)
[PROOFSTEP]
field_simp [Nat.cast_add_one_ne_zero k]
[GOAL]
case h.e'_7
k : ℕ
x : ℝ
⊢ bernoulliFun k x * (↑k + 1) = (↑k + 1) * bernoulliFun k x
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ ∫ (x : ℝ) in 0 ..1, bernoulliFun k x = 0
[PROOFSTEP]
rw [integral_eq_sub_of_hasDerivAt (fun x _ => antideriv_bernoulliFun k x)
    ((Polynomial.continuous _).intervalIntegrable _ _)]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ bernoulliFun (k + 1) 1 / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
rw [bernoulliFun_eval_one]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ (bernoulliFun (k + 1) 0 + if k + 1 = 1 then 1 else 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 1) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ False
[PROOFSTEP]
exact hk (Nat.succ_inj'.mp h)
[GOAL]
case neg
k : ℕ
hk : k ≠ 0
h : ¬k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
[PROOFSTEP]
simp
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)
[PROOFSTEP]
unfold bernoulliFourierCoeff
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun k x)) n =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
rw [fourierCoeffOn_of_hasDerivAt zero_lt_one hn (fun x _ => (hasDerivAt_bernoulliFun k x).ofReal_comp)
    ((continuous_ofReal.comp <| continuous_const.mul <| Polynomial.continuous _).intervalIntegrable _ _)]
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        (↑1 - ↑0) * fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
simp_rw [ofReal_one, ofReal_zero, sub_zero, one_mul]
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      (↑(fourier (-n)) ↑0 * (↑(bernoulliFun k 1) - ↑(bernoulliFun k 0)) -
        fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
rw [QuotientAddGroup.mk_zero, fourier_eval_zero, one_mul, ← ofReal_sub, bernoulliFun_eval_one, add_sub_cancel']
[GOAL]
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) *
      (↑(if k = 1 then 1 else 0) - fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ ↑(if k = 1 then 1 else 0) = if k = 1 then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : k = 1
⊢ ↑1 = 1
[PROOFSTEP]
simp only [ofReal_one, ofReal_zero, one_mul]
[GOAL]
case neg
k : ℕ
n : ℤ
hn : n ≠ 0
h✝ : ¬k = 1
⊢ ↑0 = 0
[PROOFSTEP]
simp only [ofReal_one, ofReal_zero, one_mul]
[GOAL]
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn (_ : 0 < 1) (fun x => ↑(↑k * bernoulliFun (k - 1) x)) n =
    ↑k * fourierCoeffOn bernoulliFourierCoeff.proof_1 (fun x => ↑(bernoulliFun (k - 1) x)) n
[PROOFSTEP]
simp_rw [ofReal_mul, ofReal_nat_cast, fourierCoeffOn.const_mul]
[GOAL]
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0
[PROOFSTEP]
simpa using bernoulliFourierCoeff_recurrence 0 hn
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = 0
[PROOFSTEP]
simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero, div_one, one_smul,
  intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk, ofReal_zero]
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = -↑k ! / (2 * ↑π * I * ↑0) ^ k
[PROOFSTEP]
rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow' _ hk, div_zero]
[GOAL]
case inr
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
refine' Nat.le_induction _ (fun k hk h'k => _) k (Nat.one_le_iff_ne_zero.mpr hk)
[GOAL]
case inr.refine'_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 1 n = -↑1! / (2 * ↑π * I * ↑n) ^ 1
[PROOFSTEP]
rw [bernoulliFourierCoeff_recurrence 1 hn]
[GOAL]
case inr.refine'_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if 1 = 1 then 1 else 0) - ↑1 * bernoulliFourierCoeff (1 - 1) n) =
    -↑1! / (2 * ↑π * I * ↑n) ^ 1
[PROOFSTEP]
simp only [Nat.cast_one, tsub_self, neg_mul, one_mul, eq_self_iff_true, if_true, Nat.factorial_one, pow_one, inv_I,
  mul_neg]
[GOAL]
case inr.refine'_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / -(2 * ↑π * I * ↑n) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * ↑π * I * ↑n)
[PROOFSTEP]
rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
[GOAL]
case inr.refine'_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ bernoulliFourierCoeff (k + 1) n = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
rw [bernoulliFourierCoeff_recurrence (k + 1) hn, Nat.add_sub_cancel k 1]
[GOAL]
case inr.refine'_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if k + 1 = 1 then 1 else 0) - ↑(k + 1) * bernoulliFourierCoeff k n) =
    -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (1 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : k + 1 = 1
⊢ False
[PROOFSTEP]
exact (ne_of_gt (Nat.lt_succ_iff.mpr hk)) h
[GOAL]
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ 1 / (-2 * ↑π * I * ↑n) * (0 - ↑(k + 1) * bernoulliFourierCoeff k n) = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)
[PROOFSTEP]
rw [h'k, Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add, pow_one, neg_div, mul_neg, mul_neg, mul_neg, neg_neg,
  neg_mul, neg_mul, neg_mul, div_neg]
[GOAL]
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -(1 / (2 * ↑π * I * ↑n)) * (↑(k + 1) * (↑k ! / (2 * ↑π * I * ↑n) ^ k)) =
    -(↑(k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))
[PROOFSTEP]
field_simp [Int.cast_ne_zero.mpr hn, I_ne_zero]
[GOAL]
case neg
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
h : ¬k + 1 = 1
⊢ -((↑k + 1) * ↑k !) / (2 * ↑π * I * ↑n * (2 * ↑π * I * ↑n) ^ k) =
    -((↑k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n))
[PROOFSTEP]
ring_nf
[GOAL]
k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 0 = bernoulliFun k 1
[PROOFSTEP]
exact_mod_cast (bernoulliFun_endpoints_eq_of_ne_one hk).symm
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ fourierCoeff (ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
have : ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) = AddCircle.liftIco 1 0 ((↑) ∘ bernoulliFun k) := by ext1 x; rfl
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
⊢ ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)
[PROOFSTEP]
ext1 x
[GOAL]
case h
k : ℕ
hk : k ≠ 0
n : ℤ
x : 𝕌
⊢ (ofReal' ∘ periodizedBernoulli k) x = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k) x
[PROOFSTEP]
rfl
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)
⊢ fourierCoeff (ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
rw [this, fourierCoeff_liftIco_eq]
[GOAL]
k : ℕ
hk : k ≠ 0
n : ℤ
this : ofReal' ∘ periodizedBernoulli k = AddCircle.liftIco 1 0 (ofReal' ∘ bernoulliFun k)
⊢ fourierCoeffOn (_ : 0 < 0 + 1) (ofReal' ∘ bernoulliFun k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
simpa only [zero_add] using bernoulliFourierCoeff_eq hk n
[GOAL]
k : ℕ
hk : 2 ≤ k
⊢ Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
have : ∀ n : ℤ, -(k ! : ℂ) / (2 * π * I * n) ^ k = -k ! / (2 * π * I) ^ k * (1 / (n : ℂ) ^ k) := by intro n;
  rw [mul_one_div, div_div, ← mul_pow]
[GOAL]
k : ℕ
hk : 2 ≤ k
⊢ ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
[PROOFSTEP]
intro n
[GOAL]
k : ℕ
hk : 2 ≤ k
n : ℤ
⊢ -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
[PROOFSTEP]
rw [mul_one_div, div_div, ← mul_pow]
[GOAL]
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
simp_rw [this]
[GOAL]
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n => -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
[PROOFSTEP]
apply Summable.mul_left
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun i => 1 / ↑i ^ k
[PROOFSTEP]
rw [← summable_norm_iff]
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun x => ‖1 / ↑x ^ k‖
[PROOFSTEP]
have : (fun x : ℤ => ‖1 / (x : ℂ) ^ k‖) = fun x : ℤ => |1 / (x : ℝ) ^ k| :=
  by
  ext1 x
  rw [norm_eq_abs, ← Complex.abs_ofReal]
  congr 1
  norm_cast
[GOAL]
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
[PROOFSTEP]
ext1 x
[GOAL]
case h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ ‖1 / ↑x ^ k‖ = |1 / ↑x ^ k|
[PROOFSTEP]
rw [norm_eq_abs, ← Complex.abs_ofReal]
[GOAL]
case h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ ↑Complex.abs (1 / ↑x ^ k) = ↑Complex.abs ↑(1 / ↑x ^ k)
[PROOFSTEP]
congr 1
[GOAL]
case h.h.e_6.h
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
x : ℤ
⊢ 1 / ↑x ^ k = ↑(1 / ↑x ^ k)
[PROOFSTEP]
norm_cast
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => ‖1 / ↑x ^ k‖
[PROOFSTEP]
simp_rw [this]
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => |1 / ↑x ^ k|
[PROOFSTEP]
rw [summable_abs_iff]
[GOAL]
case hf
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|
⊢ Summable fun x => 1 / ↑x ^ k
[PROOFSTEP]
exact Real.summable_one_div_int_pow.mpr (one_lt_two.trans_le hk)
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
suffices
  ∀ {y : ℝ},
    y ∈ Ico (0 : ℝ) 1 →
      HasSum (λ (n : ℤ) => 1 / (n : ℂ) ^ k * fourier n y) (-(2 * (π : ℂ) * I) ^ k / k ! * bernoulliFun k y)
  by
  rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx
  rcases hx with (hx | rfl)
  · exact this hx
  · convert this (left_mem_Ico.mpr zero_lt_one) using 1
    · rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
    · rw [bernoulliFun_endpoints_eq_of_ne_one (by linarith : k ≠ 1)]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx✝ : x ∈ Icc 0 1
hx : x ∈ Ico 0 1 ∨ x = 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
rcases hx with (hx | rfl)
[GOAL]
case inl
k : ℕ
hk : 2 ≤ k
x : ℝ
hx✝ : x ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
hx : x ∈ Ico 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
exact this hx
[GOAL]
case inr
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑1) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1))
[PROOFSTEP]
convert this (left_mem_Ico.mpr zero_lt_one) using 1
[GOAL]
case h.e'_5
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑1) = fun n => 1 / ↑n ^ k * ↑(fourier n) ↑0
[PROOFSTEP]
rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
[GOAL]
case h.e'_6
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 0)
[PROOFSTEP]
rw [bernoulliFun_endpoints_eq_of_ne_one (by linarith : k ≠ 1)]
[GOAL]
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ k ≠ 1
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ ∀ {y : ℝ},
    y ∈ Ico 0 1 → HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
intro y hy
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
let B : C(𝕌, ℂ) :=
  ContinuousMap.mk ((↑) ∘ periodizedBernoulli k) (continuous_ofReal.comp (periodizedBernoulli.continuous (by linarith)))
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
⊢ k ≠ 1
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
have step1 : ∀ n : ℤ, fourierCoeff B n = -k ! / (2 * π * I * n) ^ k := by rw [ContinuousMap.coe_mk];
  exact fourierCoeff_bernoulli_eq (by linarith : k ≠ 0)
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
rw [ContinuousMap.coe_mk]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ ∀ (n : ℤ), fourierCoeff (ofReal' ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
[PROOFSTEP]
exact fourierCoeff_bernoulli_eq (by linarith : k ≠ 0)
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
⊢ k ≠ 0
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
have step2 :=
  has_pointwise_sum_fourier_series_of_summable ((summable_bernoulli_fourier hk).congr fun n => (step1 n).symm) y
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i => fourierCoeff (↑B) i • ↑(fourier i) ↑y) (↑B ↑y)
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
simp_rw [step1] at step2
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ HasSum (fun n => 1 / ↑n ^ k * ↑(fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
[PROOFSTEP]
convert step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ 1 / ↑n ^ k * ↑(fourier n) ↑y = -(2 * ↑π * I) ^ k / ↑k ! * (-↑k ! / (2 * ↑π * I * ↑n) ^ k) • ↑(fourier n) ↑y
case h.e'_6.h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ ↑(bernoulliFun k y) = ↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y
[PROOFSTEP]
rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel, neg_neg, mul_pow _ (n : ℂ), ← div_div, div_self]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ (2 * ↑π * I) ^ k ≠ 0
[PROOFSTEP]
rw [Ne.def, pow_eq_zero_iff', not_and_or]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ ¬2 * ↑π * I = 0 ∨ ¬k ≠ 0
[PROOFSTEP]
exact Or.inl two_pi_I_ne_zero
[GOAL]
case h.e'_5.h.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
n : ℤ
⊢ ↑k ! ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
[GOAL]
case h.e'_6.h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ ↑(bernoulliFun k y) = ↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y
[PROOFSTEP]
rw [ContinuousMap.coe_mk, Function.comp_apply, ofReal_inj, periodizedBernoulli,
  AddCircle.liftIco_coe_apply (by rwa [zero_add])]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)
step1 : ∀ (n : ℤ), fourierCoeff (↑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 :
  HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • ↑(fourier i) ↑y)
    (↑(ContinuousMap.mk (ofReal' ∘ periodizedBernoulli k)) ↑y)
⊢ y ∈ Ico 0 (0 + 1)
[PROOFSTEP]
rwa [zero_add]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ k * (↑(fourier ↑n) ↑x + (-1) ^ k * ↑(fourier (-↑n)) ↑x))
    (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))
[PROOFSTEP]
convert (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).sum_nat_of_sum_int using 1
[GOAL]
case h.e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n => 1 / ↑n ^ k * (↑(fourier ↑n) ↑x + (-1) ^ k * ↑(fourier (-↑n)) ↑x)) = fun n =>
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (↑(fourier ↑n) ↑x + (-1) ^ k * ↑(fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [Int.cast_neg, mul_add, ← mul_assoc]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * ↑(fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
conv_rhs => rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
[GOAL]
case h.e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ↑(fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * ↑(fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * ↑(fourier ↑n) ↑x + 1 / (-1) ^ k / ↑↑n ^ k * ↑(fourier (-↑n)) ↑x
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (-1) ^ k = 1 / (-1) ^ k / ↑↑n ^ k
[PROOFSTEP]
rw [div_mul_eq_mul_div₀, one_mul]
[GOAL]
case h.e'_5.h.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k / ↑n ^ k = 1 / (-1) ^ k / ↑↑n ^ k
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k = 1 / (-1) ^ k
[PROOFSTEP]
rw [eq_div_iff, ← mul_pow, ← neg_eq_neg_one_mul, neg_neg, one_pow]
[GOAL]
case h.e'_5.h.e_a.e_a.e_a
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ (-1) ^ k ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ -1 ≠ 0
[PROOFSTEP]
rw [neg_ne_zero]
[GOAL]
case h.e'_5.h.e_a.e_a.e_a.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case h.e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) =
    -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 1 / ↑0 ^ k * ↑(fourier 0) ↑x
[PROOFSTEP]
rw [Int.cast_zero, zero_pow (by linarith : 0 < k), div_zero, zero_mul, add_zero]
[GOAL]
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ 0 < k
[PROOFSTEP]
linarith
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
have :
  HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k) * (fourier n (x : 𝕌) + fourier (-n) (x : 𝕌)))
    ((-1 : ℂ) ^ (k + 1) * (2 * (π : ℂ)) ^ (2 * k) / (2 * k)! * bernoulliFun (2 * k) x) :=
  by
  convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k) hx using 3
  · rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
  · rw [pow_add, pow_one]
    conv_rhs =>
      rw [mul_pow]
      congr
      congr
      ·skip
      ·rw [pow_mul, I_sq]
    ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
[PROOFSTEP]
convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k) hx using 3
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 2 ≤ 2 * k
[PROOFSTEP]
linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
case h.e'_5.h.h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
x✝ : ℕ
⊢ ↑(fourier ↑x✝) ↑x + ↑(fourier (-↑x✝)) ↑x = ↑(fourier ↑x✝) ↑x + (-1) ^ (2 * k) * ↑(fourier (-↑x✝)) ↑x
[PROOFSTEP]
rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
[GOAL]
case h.e'_6.h.e'_5.h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
rw [pow_add, pow_one]
[GOAL]
case h.e'_6.h.e'_5.h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
conv_rhs =>
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k)
[PROOFSTEP]
rw [mul_pow]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -((2 * ↑π) ^ (2 * k) * I ^ (2 * k))
[PROOFSTEP]
congr
[GOAL]
case a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k) * I ^ (2 * k)
[PROOFSTEP]
congr
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
case a.a k : ℕ hk : k ≠ 0 x : ℝ hx : x ∈ Icc 0 1 | I ^ (2 * k)
[PROOFSTEP]
·skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
·rw [pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
rw [pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
rw [pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)
[PROOFSTEP]
rw [pow_mul, I_sq]
[GOAL]
case h.e'_6.h.e'_5.h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * (2 * ↑π) ^ (2 * k) = -((2 * ↑π) ^ (2 * k) * (-1) ^ k)
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
⊢ ↑2 = 2
[PROOFSTEP]
norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
convert ((hasSum_iff _ _).mp (this.div_const 2)).1 with n
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x) = (1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2 = ↑(1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
rw [ofReal_mul]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2 = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
rw [← mul_div]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * ((↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2) = ↑(1 / ↑n ^ (2 * k)) * ↑(Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = ↑(1 / ↑n ^ (2 * k))
[PROOFSTEP]
rw [ofReal_div, ofReal_one, ofReal_pow]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑↑n ^ (2 * k)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x) / 2 = ↑(Real.cos (2 * π * ↑n * x))
[PROOFSTEP]
rw [ofReal_cos, ofReal_mul, fourier_coe_apply, fourier_coe_apply, cos, ofReal_one, div_one, div_one, ofReal_mul,
  ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_ofNat, ofReal_nat_cast]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (exp (2 * ↑π * I * ↑n * ↑x) + exp (2 * ↑π * I * -↑n * ↑x)) / 2 =
    (exp (2 * ↑π * ↑n * ↑x * I) + exp (-(2 * ↑π * ↑n * ↑x) * I)) / 2
[PROOFSTEP]
congr 3
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 2 * ↑π * I * ↑n * ↑x = 2 * ↑π * ↑n * ↑x * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 2 * ↑π * I * -↑n * ↑x = -(2 * ↑π * ↑n * ↑x) * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))) =
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg, ofReal_nat_cast, ofReal_mul,
  ofReal_two, ofReal_one]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
rw [bernoulliFun]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k) * (↑(fourier ↑n) ↑x + ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! *
        ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) /
      2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
have :
  HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k + 1) * (fourier n (x : 𝕌) - fourier (-n) (x : 𝕌)))
    ((-1 : ℂ) ^ (k + 1) * I * (2 * π : ℂ) ^ (2 * k + 1) / (2 * k + 1)! * bernoulliFun (2 * k + 1) x) :=
  by
  convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k + 1) hx using 1
  · ext1 n
    rw [pow_add (-1 : ℂ), pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul, pow_one, ← neg_eq_neg_one_mul, ←
      sub_eq_add_neg]
  · congr
    rw [pow_add, pow_one]
    conv_rhs =>
      rw [mul_pow]
      congr
      congr
      ·skip
      ·rw [pow_add, pow_one, pow_mul, I_sq]
    ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
[PROOFSTEP]
convert hasSum_one_div_nat_pow_mul_fourier (by linarith [Nat.one_le_iff_ne_zero.mpr hk] : 2 ≤ 2 * k + 1) hx using 1
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 2 ≤ 2 * k + 1
[PROOFSTEP]
linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
case h.e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x)) = fun n =>
    1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x + (-1) ^ (2 * k + 1) * ↑(fourier (-↑n)) ↑x)
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x + (-1) ^ (2 * k + 1) * ↑(fourier (-↑n)) ↑x)
[PROOFSTEP]
rw [pow_add (-1 : ℂ), pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul, pow_one, ← neg_eq_neg_one_mul, ← sub_eq_add_neg]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) =
    -(2 * ↑π * I) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x)
[PROOFSTEP]
congr
[GOAL]
case h.e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one]
[GOAL]
case h.e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * I * (2 * ↑π) ^ (2 * k + 1) = -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
conv_rhs =>
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
  rw [mul_pow]
  congr
  congr
  ·skip
  ·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k + 1)
[PROOFSTEP]
rw [mul_pow]
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -((2 * ↑π) ^ (2 * k + 1) * I ^ (2 * k + 1))
[PROOFSTEP]
congr
[GOAL]
case a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1) * I ^ (2 * k + 1)
[PROOFSTEP]
congr
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
case a.a k : ℕ hk : k ≠ 0 x : ℝ hx : x ∈ Icc 0 1 | I ^ (2 * k + 1)
[PROOFSTEP]
·skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
·rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)
[PROOFSTEP]
rw [pow_add, pow_one, pow_mul, I_sq]
[GOAL]
case h.e'_6.e_a.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ k * -1 * I * (2 * ↑π) ^ (2 * k + 1) = -((2 * ↑π) ^ (2 * k + 1) * ((-1) ^ k * I))
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
⊢ ↑2 = 2
[PROOFSTEP]
norm_cast
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
convert ((hasSum_iff _ _).mp (this.div_const (2 * I))).1
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * Real.sin (2 * π * ↑x✝ * x) =
    (1 / ↑x✝ ^ (2 * k + 1) * (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I)).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I) =
    ↑(1 / ↑x✝ ^ (2 * k + 1) * Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
rw [ofReal_mul]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
rw [← mul_div]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) * ((↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I)) =
    ↑(1 / ↑x✝ ^ (2 * k + 1)) * ↑(Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) = ↑(1 / ↑x✝ ^ (2 * k + 1))
[PROOFSTEP]
rw [ofReal_div, ofReal_one, ofReal_pow]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) = 1 / ↑↑x✝ ^ (2 * k + 1)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (↑(fourier ↑x✝) ↑x - ↑(fourier (-↑x✝)) ↑x) / (2 * I) = ↑(Real.sin (2 * π * ↑x✝ * x))
[PROOFSTEP]
rw [ofReal_sin, ofReal_mul, fourier_coe_apply, fourier_coe_apply, sin, ofReal_one, div_one, div_one, ofReal_mul,
  ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_ofNat, ofReal_nat_cast, ← div_div, div_I, div_mul_eq_mul_div₀, ←
  neg_div, ← neg_mul, neg_sub]
[GOAL]
case h.e'_3.h.e'_1.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (exp (2 * ↑π * I * -↑x✝ * ↑x) - exp (2 * ↑π * I * ↑x✝ * ↑x)) * I / 2 =
    (exp (-(2 * ↑π * ↑x✝ * ↑x) * I) - exp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2
[PROOFSTEP]
congr 4
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 2 * ↑π * I * -↑x✝ * ↑x = -(2 * ↑π * ↑x✝ * ↑x) * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_1.e_a.e_a.e_a.e_a.e_z
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 2 * ↑π * I * ↑x✝ * ↑x = 2 * ↑π * ↑x✝ * ↑x * I
[PROOFSTEP]
ring
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))) =
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I)).re
[PROOFSTEP]
convert (ofReal_re _).symm
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I) =
    ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg, ofReal_nat_cast, ofReal_mul,
  ofReal_two, ofReal_one, ← div_div, div_I, div_mul_eq_mul_div₀]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) * I / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
have : ∀ α β γ δ : ℂ, α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ := by intros; ring
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
[PROOFSTEP]
intros
[GOAL]
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
α✝ β✝ γ✝ δ✝ : ℂ
⊢ α✝ * I * β✝ / γ✝ * δ✝ * I = I ^ 2 * α✝ * β✝ / γ✝ * δ✝
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this✝ :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) * I / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
rw [this, I_sq]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this✝ :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -(-1 * (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
rw [bernoulliFun]
[GOAL]
case h.e'_3.h.e'_1
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this✝ :
  HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * (↑(fourier ↑n) ↑x - ↑(fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -(-1 * (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! *
          ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) /
        2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
[PROOFSTEP]
ring
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)
[PROOFSTEP]
convert hasSum_one_div_nat_pow_mul_cos hk (left_mem_Icc.mpr zero_le_one) using 1
[GOAL]
case h.e'_5
k : ℕ
hk : k ≠ 0
⊢ (fun n => 1 / ↑n ^ (2 * k)) = fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_5.h
k : ℕ
hk : k ≠ 0
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)
[PROOFSTEP]
rw [mul_zero, Real.cos_zero, mul_one]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
[PROOFSTEP]
rw [Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
[PROOFSTEP]
have : (2 : ℝ) ^ (2 * k - 1) = (2 : ℝ) ^ (2 * k) / 2 :=
  by
  rw [eq_div_iff (two_ne_zero' ℝ)]
  conv_lhs =>
    congr
    ·skip
    ·rw [← pow_one (2 : ℝ)]
  rw [← pow_add, Nat.sub_add_cancel]
  linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
[PROOFSTEP]
rw [eq_div_iff (two_ne_zero' ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 = 2 ^ (2 * k)
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  ·rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1) * 2
[PROOFSTEP]
  congr
  ·skip
  ·rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1) * 2
[PROOFSTEP]
  congr
  ·skip
  ·rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1) * 2
[PROOFSTEP]
congr
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
case a k : ℕ hk : k ≠ 0 | 2
[PROOFSTEP]
·skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
[PROOFSTEP]
skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
[PROOFSTEP]
skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
[PROOFSTEP]
skip
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
·rw [← pow_one (2 : ℝ)]
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
rw [← pow_one (2 : ℝ)]
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
rw [← pow_one (2 : ℝ)]
[GOAL]
case a
k : ℕ
hk : k ≠ 0
| 2
[PROOFSTEP]
rw [← pow_one (2 : ℝ)]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 ^ 1 = 2 ^ (2 * k)
[PROOFSTEP]
rw [← pow_add, Nat.sub_add_cancel]
[GOAL]
k : ℕ
hk : k ≠ 0
⊢ 1 ≤ 2 * k
[PROOFSTEP]
linarith [Nat.one_le_iff_ne_zero.mpr hk]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
[PROOFSTEP]
rw [this, mul_pow]
[GOAL]
case h.e'_6
k : ℕ
hk : k ≠ 0
this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
⊢ (-1) ^ (k + 1) * (2 ^ (2 * k) / 2) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 ^ (2 * k) * π ^ (2 * k)) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
[PROOFSTEP]
ring
[GOAL]
⊢ HasSum (fun n => 1 / ↑n ^ 2) (π ^ 2 / 6)
[PROOFSTEP]
convert hasSum_zeta_nat one_ne_zero using 1
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 * 1 - 1) * π ^ (2 * 1) * ↑(bernoulli (2 * 1)) / ↑(2 * 1)!
[PROOFSTEP]
rw [mul_one]
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two]
[GOAL]
⊢ 2 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(1 / 6) / ↑2!
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6
⊢ π ^ 2 / 6 = 2 * π ^ 2 * (1 / 6) / 2
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6
⊢ π ^ 2 * (6 * 2) = 2 * π ^ 2 * 6
[PROOFSTEP]
ring
[GOAL]
⊢ HasSum (fun n => 1 / ↑n ^ 4) (π ^ 4 / 90)
[PROOFSTEP]
convert hasSum_zeta_nat two_ne_zero using 1
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = (-1) ^ (2 + 1) * 2 ^ (2 * 2 - 1) * π ^ (2 * 2) * ↑(bernoulli (2 * 2)) / ↑(2 * 2)!
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(bernoulli 4)) / 24
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four]
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = -(8 * π ^ 4 * ↑(-1 / 30)) / 24
case h.e'_6 ⊢ 4 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_6
⊢ π ^ 4 / 90 = 8 * π ^ 4 * (1 / 30) / 24
case h.e'_6 ⊢ 4 ≠ 1
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_6
⊢ π ^ 4 * (30 * 24) = 8 * π ^ 4 * 90
case h.e'_6 ⊢ 4 ≠ 1
[PROOFSTEP]
ring
[GOAL]
case h.e'_6
⊢ 4 ≠ 1
[PROOFSTEP]
decide
[GOAL]
⊢ eval (1 / 4) (bernoulli 3) = 3 / 64
[PROOFSTEP]
simp_rw [Polynomial.bernoulli, Finset.sum_range_succ, Polynomial.eval_add, Polynomial.eval_monomial]
[GOAL]
⊢ eval (1 / 4) (Finset.sum (Finset.range 0) fun x => ↑(monomial (3 - x)) (_root_.bernoulli x * ↑(Nat.choose 3 x))) +
            _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) +
          _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
[PROOFSTEP]
rw [Finset.sum_range_zero, Polynomial.eval_zero, zero_add, bernoulli_one]
[GOAL]
⊢ _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
[PROOFSTEP]
rw [bernoulli_eq_bernoulli'_of_ne_one zero_ne_one, bernoulli'_zero,
  bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two,
  bernoulli_eq_bernoulli'_of_ne_one (by decide : 3 ≠ 1), bernoulli'_three]
[GOAL]
⊢ 2 ≠ 1
[PROOFSTEP]
decide
[GOAL]
⊢ 3 ≠ 1
[PROOFSTEP]
decide
[GOAL]
⊢ 1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        1 / 6 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      0 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
[PROOFSTEP]
norm_num
[GOAL]
⊢ HasSum (fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)) (π ^ 3 / 32)
[PROOFSTEP]
apply (congr_arg₂ HasSum ?_ ?_).to_iff.mp <| hasSum_one_div_nat_pow_mul_sin one_ne_zero (?_ : 1 / 4 ∈ Icc (0 : ℝ) 1)
[GOAL]
⊢ (fun n => 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4))) = fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)
[PROOFSTEP]
ext1 n
[GOAL]
case h
n : ℕ
⊢ 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4)) = 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)
[PROOFSTEP]
norm_num
[GOAL]
case h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2) ∨ n = 0
[PROOFSTEP]
left
[GOAL]
case h.h
n : ℕ
⊢ Real.sin (2 * π * ↑n * (1 / 4)) = Real.sin (π * ↑n / 2)
[PROOFSTEP]
congr 1
[GOAL]
case h.h.e_x
n : ℕ
⊢ 2 * π * ↑n * (1 / 4) = π * ↑n / 2
[PROOFSTEP]
ring
[GOAL]
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32
[PROOFSTEP]
have : (1 / 4 : ℝ) = (algebraMap ℚ ℝ) (1 / 4 : ℚ) := by norm_num
[GOAL]
⊢ 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
[PROOFSTEP]
norm_num
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32
[PROOFSTEP]
rw [this, mul_pow, Polynomial.eval_map, Polynomial.eval₂_at_apply, (by decide : 2 * 1 + 1 = 3),
  Polynomial.bernoulli_three_eval_one_quarter]
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ 2 * 1 + 1 = 3
[PROOFSTEP]
decide
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 ^ 3 * π ^ 3) / 2 / ↑3! * ↑(algebraMap ℚ ℝ) (3 / 64) = π ^ 3 / 32
[PROOFSTEP]
norm_num
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 / 2 / 6 * (3 / 64) = π ^ 3 / 32
[PROOFSTEP]
field_simp
[GOAL]
this : 1 / 4 = ↑(algebraMap ℚ ℝ) (1 / 4)
⊢ 8 * π ^ 3 * 3 * 32 = π ^ 3 * (2 * 6 * 64)
[PROOFSTEP]
ring
[GOAL]
⊢ 1 / 4 ∈ Icc 0 1
[PROOFSTEP]
rw [mem_Icc]
[GOAL]
⊢ 0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ 0 ≤ 1 / 4
case right ⊢ 1 / 4 ≤ 1
[PROOFSTEP]
linarith
[GOAL]
case right
⊢ 1 / 4 ≤ 1
[PROOFSTEP]
linarith