internlm/Lean-Github huggingface dataset:
Theorem: sum_quadForm
Proof 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]
Proof 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
Theorem: sum_quadForm
Proof 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)]
Proof 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
Theorem: sum_quadForm
Proof 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]
Proof 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)
Theorem: sum_quadForm
Proof 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
Proof 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)
Theorem: sum_quadForm
Proof 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
Proof 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)
Theorem: sum_quadForm
Proof 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]
Proof 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)
Theorem: sum_quadForm
Proof 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]
Proof 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
Theorem: sum_quadForm
Proof 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)]
Proof 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
Theorem: sum_quadForm
Proof 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
Proof 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
Theorem: sum_quadForm
Proof 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
Proof 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
Theorem: sum_quadForm
Proof 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]
Proof 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
Theorem: sum_quadForm
Proof 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
Proof 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
Theorem: sum_quadForm
Proof 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
Proof 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
Theorem: sum_quadForm
Proof 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
Proof 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
Theorem: sum_quadForm
Proof 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 _ _)]
Proof 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
Theorem: sum_quadForm
Proof 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
Proof state after:
no goals
Theorem: sum_quadForm
Proof 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
Proof 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
Theorem: sum_quadForm
Proof 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
Proof state after:
no goals
Theorem: sum_quadForm
Proof 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]
Proof state after:
no goals
Theorem: Real.inverse_eq_inv
Proof state before:
a : ℝ
⊢ Ring.inverse a = a⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.toUpperTri_zero
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
⊢ toUpperTri 0 = 0
Tactic:
funext i j
Proof state after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
i j : m
⊢ toUpperTri 0 i j = 0 i j
Theorem: Matrix.toUpperTri_zero
Proof state before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
i j : m
⊢ toUpperTri 0 i j = 0 i j
Tactic:
simp [Matrix.toUpperTri]
Proof state after:
no goals
Theorem: Matrix.toUpperTri_smul
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
κ : ℝ
⊢ κ • A.toUpperTri = (κ • A).toUpperTri
Tactic:
funext i j
Proof state after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • A.toUpperTri) i j = (κ • A).toUpperTri i j
Theorem: Matrix.toUpperTri_smul
Proof state before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • A.toUpperTri) i j = (κ • A).toUpperTri i j
Tactic:
rw [Pi.smul_apply, Pi.smul_apply]
Proof state after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
κ : ℝ
i j : m
⊢ κ • A.toUpperTri i j = (κ • A).toUpperTri i j
Theorem: Matrix.toUpperTri_smul
Proof state before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
κ : ℝ
i j : m
⊢ κ • A.toUpperTri i j = (κ • A).toUpperTri i j
Tactic:
simp only [Matrix.toUpperTri]
Proof state after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • if i ≤ j then A i j else 0) = if i ≤ j then (κ • A) i j else 0
Theorem: Matrix.toUpperTri_smul
Proof state before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
κ : ℝ
i j : m
⊢ (κ • if i ≤ j then A i j else 0) = if i ≤ j then (κ • A) i j else 0
Tactic:
by_cases h : i ≤ j <;> simp [h]
Proof state after:
no goals
Theorem: Matrix.toUpperTri_add
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
⊢ (A + B).toUpperTri = A.toUpperTri + B.toUpperTri
Tactic:
funext i j
Proof state after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = (A.toUpperTri + B.toUpperTri) i j
Theorem: Matrix.toUpperTri_add
Proof state before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = (A.toUpperTri + B.toUpperTri) i j
Tactic:
rw [Pi.add_apply, Pi.add_apply]
Proof state after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = A.toUpperTri i j + B.toUpperTri i j
Theorem: Matrix.toUpperTri_add
Proof state before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (A + B).toUpperTri i j = A.toUpperTri i j + B.toUpperTri i j
Tactic:
simp only [Matrix.toUpperTri]
Proof state after:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (if i ≤ j then (A + B) i j else 0) = (if i ≤ j then A i j else 0) + if i ≤ j then B i j else 0
Theorem: Matrix.toUpperTri_add
Proof state before:
case h.h
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A B : Matrix m m ℝ
i j : m
⊢ (if i ≤ j then (A + B) i j else 0) = (if i ≤ j then A i j else 0) + if i ≤ j then B i j else 0
Tactic:
by_cases h : i ≤ j <;> simp [h]
Proof state after:
no goals
Theorem: Matrix.upperTriangular_toUpperTri
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
⊢ A.toUpperTri.upperTriangular
Tactic:
intros i j hij
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ A.toUpperTri i j = 0
Theorem: Matrix.upperTriangular_toUpperTri
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ A.toUpperTri i j = 0
Tactic:
unfold toUpperTri
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ (if i ≤ j then A i j else 0) = 0
Theorem: Matrix.upperTriangular_toUpperTri
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ (if i ≤ j then A i j else 0) = 0
Tactic:
rw [if_neg]
Proof state after:
case hnc
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ ¬i ≤ j
Theorem: Matrix.upperTriangular_toUpperTri
Proof state before:
case hnc
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
m : Type u_1
inst✝ : LinearOrder m
A : Matrix m m ℝ
i j : m
hij : id j < id i
⊢ ¬i ≤ j
Tactic:
simpa using hij
Proof state after:
no goals
Theorem: Matrix.upperTriangular.toUpperTri_eq
Proof state before:
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
⊢ A.toUpperTri = A
Tactic:
ext i j
Proof state after:
case a
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
⊢ A.toUpperTri i j = A i j
Theorem: Matrix.upperTriangular.toUpperTri_eq
Proof state before:
case a
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
⊢ A.toUpperTri i j = A i j
Tactic:
by_cases h : i ≤ j
Proof state after:
case pos
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : i ≤ j
⊢ A.toUpperTri i j = A i j

case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j
Theorem: Matrix.upperTriangular.toUpperTri_eq
Proof state before:
case pos
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : i ≤ j
⊢ A.toUpperTri i j = A i j

case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j
Tactic:
simp [toUpperTri, h]
Proof state after:
case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j
Theorem: Matrix.upperTriangular.toUpperTri_eq
Proof state before:
case neg
n : Type
inst✝² : Fintype n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.upperTriangular
i j : n
h : ¬i ≤ j
⊢ A.toUpperTri i j = A i j
Tactic:
simp [toUpperTri, h, hA (lt_of_not_ge h)]
Proof state after:
no goals
Theorem: Matrix.BlockTriangular_blockDiagonal'
Proof state before:
α : Type u_1
β : Type ?u.1255
m : Type ?u.1258
n : Type ?u.1261
o : Type ?u.1264
m' : α → Type u_2
n' : α → Type ?u.1274
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
⊢ (blockDiagonal' d).BlockTriangular Sigma.fst
Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
Proof state after:
case mk.mk
α : Type u_1
β : Type ?u.1255
m : Type ?u.1258
n : Type ?u.1261
o : Type ?u.1264
m' : α → Type u_2
n' : α → Type ?u.1274
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst
⊢ blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0
Theorem: Matrix.BlockTriangular_blockDiagonal'
Proof state before:
case mk.mk
α : Type u_1
β : Type ?u.1255
m : Type ?u.1258
n : Type ?u.1261
o : Type ?u.1264
m' : α → Type u_2
n' : α → Type ?u.1274
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst
⊢ blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0
Tactic:
apply blockDiagonal'_apply_ne d i' j' (fun h' => ne_of_lt h h'.symm)
Proof state after:
no goals
Theorem: Matrix.BlockTriangular_blockDiagonal
Proof state before:
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
⊢ (blockDiagonal d).BlockTriangular Prod.snd
Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
Proof state after:
case mk.mk
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0
Theorem: Matrix.BlockTriangular_blockDiagonal
Proof state before:
case mk.mk
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0
Tactic:
rw [blockDiagonal'_eq_blockDiagonal, BlockTriangular_blockDiagonal']
Proof state after:
case mk.mk.a
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst
Theorem: Matrix.BlockTriangular_blockDiagonal
Proof state before:
case mk.mk.a
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst
Tactic:
exact h
Proof state after:
no goals
Theorem: Matrix.toBlock_inverse_mul_toBlock_eq_one_of_BlockTriangular
Proof state before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
Tactic:
let p := (fun i => b i < k)
Proof state after:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
Theorem: Matrix.toBlock_inverse_mul_toBlock_eq_one_of_BlockTriangular
Proof state before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
Tactic:
have h_sum : M⁻¹.toBlock p p * M.toBlock p p +
    M⁻¹.toBlock p (fun i => ¬ p i) * M.toBlock (fun i => ¬ p i) p = 1 := by
  rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
Proof state after:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1