[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
⊢ Injective circulant
[PROOFSTEP]
intro v w h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
⊢ v = w
[PROOFSTEP]
ext k
[GOAL]
case h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k
[PROOFSTEP]
rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
⊢ Injective fun v => circulant v
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v : n → α
⊢ (circulant v)ᵀ = circulant fun i => v (-i)
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v : n → α
i✝ x✝ : n
⊢ (circulant v)ᵀ i✝ x✝ = circulant (fun i => v (-i)) i✝ x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝¹ : Star α
inst✝ : AddGroup n
v : n → α
⊢ (circulant v)ᴴ = circulant (star fun i => v (-i))
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝¹ : Star α
inst✝ : AddGroup n
v : n → α
i✝ x✝ : n
⊢ (circulant v)ᴴ i✝ x✝ = circulant (star fun i => v (-i)) i✝ x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
⊢ ∀ (v : Fin 0 → α), (circulant v)ᵀ = circulant fun i => v (-i)
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : Star α
⊢ ∀ (v : Fin 0 → α), (circulant v)ᴴ = circulant (star fun i => v (-i))
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
⊢ circulant v * circulant w = circulant (mulVec (circulant v) w)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = circulant (mulVec (circulant v) w) i j
[PROOFSTEP]
simp only [mul_apply, mulVec, circulant_apply, dotProduct]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, v (i - j - x) * w x
[PROOFSTEP]
refine' Fintype.sum_equiv (Equiv.subRight j) _ _ _
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∀ (x : n), v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
[PROOFSTEP]
intro x
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
[PROOFSTEP]
simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : Semiring α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant (mulVec (circulant v) w)
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
⊢ circulant v * circulant w = circulant w * circulant v
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j
[PROOFSTEP]
simp only [mul_apply, circulant_apply, mul_comm]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, w (i - x) * v (x - j)
[PROOFSTEP]
refine' Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ _
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∀ (x : n),
    v (i - x) * w (x - j) =
      w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
[PROOFSTEP]
intro x
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) =
    w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
[PROOFSTEP]
congr 2
[GOAL]
case a.h.e_a.e_a
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)
[PROOFSTEP]
abel
[GOAL]
case a.h.e_a.e_a
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝¹ : CommSemigroup α
inst✝ : AddCommMonoid α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant w * circulant v
[PROOFSTEP]
simp [Injective]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
n : Type u_7
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
⊢ circulant (Pi.single 0 1) = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
n : Type u_7
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = OfNat.ofNat 1 i j
[PROOFSTEP]
simp [one_apply, Pi.single_apply, sub_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
n : Type u_6
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
⊢ circulant (Pi.single 0 a) = ↑(scalar n) a
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
n : Type u_6
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
i j : n
⊢ circulant (Pi.single 0 a) i j = ↑(scalar n) a i j
[PROOFSTEP]
simp [Pi.single_apply, one_apply, sub_eq_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1
[PROOFSTEP]
simp [Injective]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1
[PROOFSTEP]
rw [← circulant_single_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = circulant (Pi.single 0 1)
[PROOFSTEP]
congr with j
[GOAL]
case a.h
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
j x✝ : Fin (n + 1)
⊢ circulant (fun i => if ↑i = 0 then 1 else 0) j x✝ = circulant (Pi.single 0 1) j x✝
[PROOFSTEP]
simp [Pi.single_apply, Fin.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v : n → α
⊢ IsSymm (circulant v) ↔ ∀ (i : n), v (-i) = v i
[PROOFSTEP]
rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
v✝ : Fin 0 → α
⊢ IsSymm (circulant v✝) ↔ ∀ (i : Fin 0), v✝ (-i) = v✝ i
[PROOFSTEP]
simp [IsSymm.ext_iff, IsEmpty.forall_iff]
