Theorem: sum_quadForm (CvxLean/Lib/Math/CovarianceEstimation.lean)

State before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace
Tactic:
by_cases h : m = 0
State after:
case pos
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace

case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace

State before:
case pos
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace

case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace
Tactic:
{ subst h; simp }
State after:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace

State before:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace
Tactic:
simp only [Matrix.quadForm, Matrix.trace, covarianceMatrix, diag, mul_apply, Finset.sum_mul,
  Finset.sum_div]
State after:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ x : Fin m, y x ⬝ᵥ R.mulVec (y x) =
    ↑m * ∑ x : Fin n, ∑ x_1 : Fin n, ∑ i : Fin m, y i x * y i x_1 / ↑m * R.transpose x_1 x

State before:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ x : Fin m, y x ⬝ᵥ R.mulVec (y x) =
    ↑m * ∑ x : Fin n, ∑ x_1 : Fin n, ∑ i : Fin m, y i x * y i x_1 / ↑m * R.transpose x_1 x
Tactic:
erw [Finset.sum_comm (γ := Fin m)]
State after:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ y_1 : Fin n, ∑ x : Fin m, y x y_1 * R.mulVec (y x) y_1 =
    ↑m * ∑ x : Fin n, ∑ x_1 : Fin n, ∑ i : Fin m, y i x * y i x_1 / ↑m * R.transpose x_1 x

State before:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ y_1 : Fin n, ∑ x : Fin m, y x y_1 * R.mulVec (y x) y_1 =
    ↑m * ∑ x : Fin n, ∑ x_1 : Fin n, ∑ i : Fin m, y i x * y i x_1 / ↑m * R.transpose x_1 x
Tactic:
simp_rw [Finset.mul_sum]
State after:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ y_1 : Fin n, ∑ x : Fin m, y x y_1 * R.mulVec (y x) y_1 =
    ∑ x : Fin n, ∑ x_1 : Fin n, ∑ i : Fin m, ↑m * (y i x * y i x_1 / ↑m * R.transpose x_1 x)

State before:
case neg
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ ∑ y_1 : Fin n, ∑ x : Fin m, y x y_1 * R.mulVec (y x) y_1 =
    ∑ x : Fin n, ∑ x_1 : Fin n, ∑ i : Fin m, ↑m * (y i x * y i x_1 / ↑m * R.transpose x_1 x)
Tactic:
congr
State after:
case neg.e_f
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ (fun y_1 => ∑ x : Fin m, y x y_1 * R.mulVec (y x) y_1) = fun x =>
    ∑ x_1 : Fin n, ∑ i : Fin m, ↑m * (y i x * y i x_1 / ↑m * R.transpose x_1 x)

State before:
case neg.e_f
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
⊢ (fun y_1 => ∑ x : Fin m, y x y_1 * R.mulVec (y x) y_1) = fun x =>
    ∑ x_1 : Fin n, ∑ i : Fin m, ↑m * (y i x * y i x_1 / ↑m * R.transpose x_1 x)
Tactic:
ext i
State after:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ x : Fin n, ∑ i_1 : Fin m, ↑m * (y i_1 i * y i_1 x / ↑m * R.transpose x i)

State before:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ x : Fin n, ∑ i_1 : Fin m, ↑m * (y i_1 i * y i_1 x / ↑m * R.transpose x i)
Tactic:
have hmnz : (m : ℝ) ≠ 0 := by simp [h]
State after:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ x : Fin n, ∑ i_1 : Fin m, ↑m * (y i_1 i * y i_1 x / ↑m * R.transpose x i)

State before:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ x : Fin n, ∑ i_1 : Fin m, ↑m * (y i_1 i * y i_1 x / ↑m * R.transpose x i)
Tactic:
simp_rw [← mul_assoc, mul_div_cancel₀ _ hmnz]
State after:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ x : Fin n, ∑ x_1 : Fin m, y x_1 i * y x_1 x * R.transpose x i

State before:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ x : Fin n, ∑ x_1 : Fin m, y x_1 i * y x_1 x * R.transpose x i
Tactic:
erw [Finset.sum_comm (α := Fin m)]
State after:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ y_1 : Fin m, ∑ x : Fin n, y y_1 i * y y_1 x * R.transpose x i

State before:
case neg.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ ∑ x : Fin m, y x i * R.mulVec (y x) i = ∑ y_1 : Fin m, ∑ x : Fin n, y y_1 i * y y_1 x * R.transpose x i
Tactic:
congr
State after:
case neg.e_f.h.e_f
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ (fun x => y x i * R.mulVec (y x) i) = fun y_1 => ∑ x : Fin n, y y_1 i * y y_1 x * R.transpose x i

State before:
case neg.e_f.h.e_f
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
⊢ (fun x => y x i * R.mulVec (y x) i) = fun y_1 => ∑ x : Fin n, y y_1 i * y y_1 x * R.transpose x i
Tactic:
ext j
State after:
case neg.e_f.h.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ y j i * R.mulVec (y j) i = ∑ x : Fin n, y j i * y j x * R.transpose x i

State before:
case neg.e_f.h.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ y j i * R.mulVec (y j) i = ∑ x : Fin n, y j i * y j x * R.transpose x i
Tactic:
simp_rw [mul_assoc, ← Finset.mul_sum]
State after:
case neg.e_f.h.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ y j i * R.mulVec (y j) i = y j i * ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i

State before:
case neg.e_f.h.e_f.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ y j i * R.mulVec (y j) i = y j i * ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i
Tactic:
apply congr_arg
State after:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ R.mulVec (y j) i = ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i

State before:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ R.mulVec (y j) i = ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i
Tactic:
unfold Matrix.mulVec
State after:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ (let i := i;
    (fun j => R i j) ⬝ᵥ y j) =
    ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i

State before:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ (let i := i;
    (fun j => R i j) ⬝ᵥ y j) =
    ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i
Tactic:
unfold dotProduct
State after:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ (let i := i;
    ∑ i_1 : Fin n, (fun j => R i j) i_1 * y j i_1) =
    ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i

State before:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ (let i := i;
    ∑ i_1 : Fin n, (fun j => R i j) i_1 * y j i_1) =
    ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i
Tactic:
simp only [mul_comm (R _ _)]
State after:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ ∑ x : Fin n, y j x * R i x = ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i

State before:
case neg.e_f.h.e_f.h.h
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
hmnz : ↑m ≠ 0
j : Fin m
⊢ ∑ x : Fin n, y j x * R i x = ∑ i_1 : Fin n, y j i_1 * R.transpose i_1 i
Tactic:
congr
State after:
no goals

State before:
case pos
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : m = 0
⊢ ∑ i : Fin m, R.quadForm (y i) = ↑m * (covarianceMatrix y * R.transpose).trace
Tactic:
subst h
State after:
case pos
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin 0 → Fin n → ℝ
⊢ ∑ i : Fin 0, R.quadForm (y i) = ↑0 * (covarianceMatrix y * R.transpose).trace

State before:
case pos
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin 0 → Fin n → ℝ
⊢ ∑ i : Fin 0, R.quadForm (y i) = ↑0 * (covarianceMatrix y * R.transpose).trace
Tactic:
simp
State after:
no goals

State before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
m : ℕ
y : Fin m → Fin n → ℝ
h : ¬m = 0
i : Fin n
⊢ ↑m ≠ 0
Tactic:
simp [h]
State after:
no goals