internlm/Lean-Github huggingface dataset:
Theorem: MatrixCookbook.eq_163
Proof state before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
conv_lhs => rw [add_comm]
Proof state after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ + A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Theorem: MatrixCookbook.eq_163
Proof state before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ + A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
rw [Matrix.inv_add_inv (iff_of_true hA hB), Matrix.inv_add_inv (iff_of_true hB hA)]
Proof state after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ * (B + A) * A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ * (A + B) * B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Theorem: MatrixCookbook.eq_163
Proof state before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ (B⁻¹ * (B + A) * A⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ * (A + B) * B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
Tactic:
simp_rw [Matrix.mul_inv_rev, Matrix.inv_inv_of_invertible, mul_assoc, add_comm]
Proof state after:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ True ∧ True
Theorem: MatrixCookbook.eq_163
Proof state before:
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this✝ : Invertible A := hA.invertible
this : Invertible B := hB.invertible
⊢ True ∧ True
Tactic:
simp
Proof state after:
no goals
Theorem: MatrixCookbook.eq_24
Proof state before:
ι : Type ?u.26561
R : Type u_1
m : Type u_2
n : Type ?u.26570
p : Type ?u.26573
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
u v : m → R
⊢ (1 + col u * row v).det = 1 + u ⬝ᵥ v
Tactic:
rw [det_one_add_col_mul_row u v, dotProduct_comm]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_25
Proof state before:
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A).det = 1 + A.det + A.trace
Tactic:
simp [det_fin_two, trace_fin_two]
Proof state after:
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A 0 0) * (1 + A 1 1) - A 0 1 * A 1 0 = 1 + (A 0 0 * A 1 1 - A 0 1 * A 1 0) + (A 0 0 + A 1 1)
Theorem: MatrixCookbook.eq_25
Proof state before:
ι : Type ?u.30876
R : Type u_1
m : Type ?u.30882
n : Type ?u.30885
p : Type ?u.30888
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ (1 + A 0 0) * (1 + A 1 1) - A 0 1 * A 1 0 = 1 + (A 0 0 * A 1 1 - A 0 1 * A 1 0) + (A 0 0 + A 1 1)
Tactic:
ring
Proof state after:
no goals
Theorem: MatrixCookbook.eq_26
Proof state before:
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ (1 + A).det = 1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace
Tactic:
apply mul_left_cancel₀ (isUnit_of_invertible (2 : R)).ne_zero
Proof state after:
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ 2 * (1 + A).det = 2 * (1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace)
Theorem: MatrixCookbook.eq_26
Proof state before:
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ 2 * (1 + A).det = 2 * (1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace)
Tactic:
simp only [det_fin_three, trace_fin_three, pow_two, Matrix.mul_apply,
  Fin.sum_univ_succ, Matrix.one_apply]
Proof state after:
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ 2 *
      ((1 + A) 0 0 * (1 + A) 1 1 * (1 + A) 2 2 - (1 + A) 0 0 * (1 + A) 1 2 * (1 + A) 2 1 -
              (1 + A) 0 1 * (1 + A) 1 0 * (1 + A) 2 2 +
            (1 + A) 0 1 * (1 + A) 1 2 * (1 + A) 2 0 +
          (1 + A) 0 2 * (1 + A) 1 0 * (1 + A) 2 1 -
        (1 + A) 0 2 * (1 + A) 1 1 * (1 + A) 2 0) =
    2 *
      (1 +
              (A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
                  A 0 2 * A 1 0 * A 2 1 -
                A 0 2 * A 1 1 * A 2 0) +
            (A 0 0 + A 1 1 + A 2 2) +
          ⅟2 * ((A 0 0 + A 1 1 + A 2 2) * (A 0 0 + A 1 1 + A 2 2)) -
        ⅟2 *
          (A 0 0 * A 0 0 +
                (A 0 (Fin.succ 0) * A (Fin.succ 0) 0 +
                  (A 0 (Fin.succ 0).succ * A (Fin.succ 0).succ 0 +
                    ∑ i : Fin 0, A 0 i.succ.succ.succ * A i.succ.succ.succ 0)) +
              (A 1 0 * A 0 1 +
                (A 1 (Fin.succ 0) * A (Fin.succ 0) 1 +
                  (A 1 (Fin.succ 0).succ * A (Fin.succ 0).succ 1 +
                    ∑ i : Fin 0, A 1 i.succ.succ.succ * A i.succ.succ.succ 1))) +
            (A 2 0 * A 0 2 +
              (A 2 (Fin.succ 0) * A (Fin.succ 0) 2 +
                (A 2 (Fin.succ 0).succ * A (Fin.succ 0).succ 2 +
                  ∑ i : Fin 0, A 2 i.succ.succ.succ * A i.succ.succ.succ 2)))))
Theorem: MatrixCookbook.eq_26
Proof state before:
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ 2 * (1 + A 0 0 + (1 + A 0 0) * A 1 1) + 2 * ((1 + A 0 0 + (1 + A 0 0) * A 1 1) * A 2 2) -
              2 * ((1 + A 0 0) * A 1 2 * A 2 1) -
            (2 * (A 0 1 * A 1 0) + 2 * (A 0 1 * A 1 0 * A 2 2)) +
          2 * (A 0 1 * A 1 2 * A 2 0) +
        2 * (A 0 2 * A 1 0 * A 2 1) -
      2 * ((A 0 2 + A 0 2 * A 1 1) * A 2 0) =
    2 +
            (2 * (A 0 0 * A 1 1 * A 2 2) - 2 * (A 0 0 * A 1 2 * A 2 1) - 2 * (A 0 1 * A 1 0 * A 2 2) +
                  2 * (A 0 1 * A 1 2 * A 2 0) +
                2 * (A 0 2 * A 1 0 * A 2 1) -
              2 * (A 0 2 * A 1 1 * A 2 0)) +
          (2 * A 0 0 + 2 * A 1 1 + 2 * A 2 2) +
        ((A 0 0 + A 1 1 + A 2 2) * A 0 0 + (A 0 0 + A 1 1 + A 2 2) * A 1 1 + (A 0 0 + A 1 1 + A 2 2) * A 2 2) -
      (A 0 0 * A 0 0 + (A 0 1 * A 1 0 + A 0 2 * A 2 0) + (A 1 0 * A 0 1 + (A 1 1 * A 1 1 + A 1 2 * A 2 1)) +
        (A 2 0 * A 0 2 + (A 2 1 * A 1 2 + A 2 2 * A 2 2)))
Tactic:
ring
Proof state after:
no goals
Theorem: MatrixCookbook.eq_27
Proof state before:
ι : Type ?u.74781
R : Type u_1
m : Type ?u.74787
n : Type ?u.74790
p : Type ?u.74793
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 4) (Fin 4) R
inst✝ : CharZero R
⊢ (1 + A).det =
    1 + A.det + A.trace + 1 / 2 * (A.trace ^ 2 - (A ^ 2).trace) +
      1 / 6 * (A.trace ^ 3 - 3 * A.trace * (A ^ 2).trace + 2 * (A ^ 3).trace)
Tactic:
field_simp
Proof state after:
ι : Type ?u.74781
R : Type u_1
m : Type ?u.74787
n : Type ?u.74790
p : Type ?u.74793
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 4) (Fin 4) R
inst✝ : CharZero R
⊢ (1 + A).det * (2 * 6) =
    ((1 + A.det + A.trace) * 2 + (A.trace ^ 2 - (A ^ 2).trace)) * 6 +
      (A.trace ^ 3 - 3 * A.trace * (A ^ 2).trace + 2 * (A ^ 3).trace) * 2
Theorem: MatrixCookbook.eq_31
Proof state before:
ι : Type ?u.145147
R : Type u_1
m : Type ?u.145153
n : Type ?u.145156
p : Type ?u.145159
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
A : Matrix (Fin 2) (Fin 2) R
⊢ A⁻¹ = A.det⁻¹ • of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]]
Tactic:
rw [inv_def, adjugate_fin_two, Ring.inverse_eq_inv]
Proof state after:
no goals
Theorem: hasDerivAt_matrix
Proof state before:
ι : Type ?u.1410
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.1425
q : Type ?u.1428
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
f' : Matrix m n A
⊢ HasDerivAt f f' r ↔ ∀ (i : m) (j : n), HasDerivAt (fun r => f r i j) (f' i j) r
Tactic:
erw [hasDerivAt_pi]
Proof state after:
ι : Type ?u.1410
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.1425
q : Type ?u.1428
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
f' : Matrix m n A
⊢ (∀ (i : m), HasDerivAt (fun x => f x i) (f' i) r) ↔ ∀ (i : m) (j : n), HasDerivAt (fun r => f r i j) (f' i j) r
Theorem: hasDerivAt_matrix
Proof state before:
ι : Type ?u.1410
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.1425
q : Type ?u.1428
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
f' : Matrix m n A
⊢ (∀ (i : m), HasDerivAt (fun x => f x i) (f' i) r) ↔ ∀ (i : m) (j : n), HasDerivAt (fun r => f r i j) (f' i j) r
Tactic:
simp_rw [hasDerivAt_pi]
Proof state after:
no goals
Theorem: HasDerivAt.matrix_mul
Proof state before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : HasDerivAt X X' r
hY : HasDerivAt Y Y' r
⊢ HasDerivAt (fun a => X a * Y a) (X' * Y r + X r * Y') r
Tactic:
rw [hasDerivAt_matrix] at hX hY ⊢
Proof state after:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m) (j : p), HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r
Theorem: HasDerivAt.matrix_mul
Proof state before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m) (j : p), HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r
Tactic:
intro i j
Proof state after:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r
Theorem: HasDerivAt.matrix_mul
Proof state before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r
Tactic:
simp only [mul_apply, Matrix.add_apply, ← Finset.sum_add_distrib]
Proof state after:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => ∑ j_1 : n, X r i j_1 * Y r j_1 j) (∑ x : n, (X' i x * Y r x j + X r i x * Y' x j)) r
Theorem: HasDerivAt.matrix_mul
Proof state before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => ∑ j_1 : n, X r i j_1 * Y r j_1 j) (∑ x : n, (X' i x * Y r x j + X r i x * Y' x j)) r
Tactic:
exact HasDerivAt.sum fun k _hk => (hX _ _).mul (hY _ _)
Proof state after:
no goals
Theorem: HasDerivAt.matrix_kronecker
Proof state before:
ι : Type ?u.12157
R : Type u_6
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type u_5
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix p q A
X' : Matrix m n A
Y' : Matrix p q A
r : R
hX : HasDerivAt X X' r
hY : HasDerivAt Y Y' r
⊢ HasDerivAt (fun a => kroneckerMap (fun x x_1 => x * x_1) (X a) (Y a))
    (kroneckerMap (fun x x_1 => x * x_1) X' (Y r) + kroneckerMap (fun x x_1 => x * x_1) (X r) Y') r
Tactic:
rw [hasDerivAt_matrix] at hX hY ⊢
Proof state after:
ι : Type ?u.12157
R : Type u_6
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type u_5
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix p q A
X' : Matrix m n A
Y' : Matrix p q A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : p) (j : q), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m × p) (j : n × q),
    HasDerivAt (fun r => kroneckerMap (fun x x_1 => x * x_1) (X r) (Y r) i j)
      ((kroneckerMap (fun x x_1 => x * x_1) X' (Y r) + kroneckerMap (fun x x_1 => x * x_1) (X r) Y') i j) r
Theorem: HasDerivAt.matrix_kronecker
Proof state before:
ι : Type ?u.12157
R : Type u_6
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type u_5
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix p q A
X' : Matrix m n A
Y' : Matrix p q A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : p) (j : q), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m × p) (j : n × q),
    HasDerivAt (fun r => kroneckerMap (fun x x_1 => x * x_1) (X r) (Y r) i j)
      ((kroneckerMap (fun x x_1 => x * x_1) X' (Y r) + kroneckerMap (fun x x_1 => x * x_1) (X r) Y') i j) r
Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩
Proof state after:
case mk.mk
ι : Type ?u.12157
R : Type u_6
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type u_5
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix p q A
X' : Matrix m n A
Y' : Matrix p q A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : p) (j : q), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
i' : p
j : n
j' : q
⊢ HasDerivAt (fun r => kroneckerMap (fun x x_1 => x * x_1) (X r) (Y r) (i, i') (j, j'))
    ((kroneckerMap (fun x x_1 => x * x_1) X' (Y r) + kroneckerMap (fun x x_1 => x * x_1) (X r) Y') (i, i') (j, j')) r
Theorem: HasDerivAt.matrix_kronecker
Proof state before:
case mk.mk
ι : Type ?u.12157
R : Type u_6
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type u_5
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X : R → Matrix m n A
Y : R → Matrix p q A
X' : Matrix m n A
Y' : Matrix p q A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : p) (j : q), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
i' : p
j : n
j' : q
⊢ HasDerivAt (fun r => kroneckerMap (fun x x_1 => x * x_1) (X r) (Y r) (i, i') (j, j'))
    ((kroneckerMap (fun x x_1 => x * x_1) X' (Y r) + kroneckerMap (fun x x_1 => x * x_1) (X r) Y') (i, i') (j, j')) r
Tactic:
exact (hX _ _).mul (hY _ _)
Proof state after:
no goals
Theorem: HasDerivAt.matrix_hadamard
Proof state before:
ι : Type ?u.17223
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.17238
q : Type ?u.17241
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X Y : R → Matrix m n A
X' Y' : Matrix m n A
r : R
hX : HasDerivAt X X' r
hY : HasDerivAt Y Y' r
⊢ HasDerivAt (fun a => X a ⊙ Y a) (X' ⊙ Y r + X r ⊙ Y') r
Tactic:
rw [hasDerivAt_matrix] at hX hY ⊢
Proof state after:
ι : Type ?u.17223
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.17238
q : Type ?u.17241
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X Y : R → Matrix m n A
X' Y' : Matrix m n A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : m) (j : n), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m) (j : n), HasDerivAt (fun r => (X r ⊙ Y r) i j) ((X' ⊙ Y r + X r ⊙ Y') i j) r
Theorem: HasDerivAt.matrix_hadamard
Proof state before:
ι : Type ?u.17223
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.17238
q : Type ?u.17241
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X Y : R → Matrix m n A
X' Y' : Matrix m n A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : m) (j : n), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m) (j : n), HasDerivAt (fun r => (X r ⊙ Y r) i j) ((X' ⊙ Y r + X r ⊙ Y') i j) r
Tactic:
rintro i j
Proof state after:
ι : Type ?u.17223
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.17238
q : Type ?u.17241
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X Y : R → Matrix m n A
X' Y' : Matrix m n A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : m) (j : n), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : n
⊢ HasDerivAt (fun r => (X r ⊙ Y r) i j) ((X' ⊙ Y r + X r ⊙ Y') i j) r