internlm/Lean-Github huggingface dataset:
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝ : k ∈ Finset.univ
⊢ ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i k * B k x * X x_1 x * c x_1 =
    ∑ y : n, ∑ x : m, ∑ x_1 : m, X x_1 y * (B k y * (c x_1 * a x)) * X x k
Tactic:
refine' Finset.sum_congr rfl fun l _ => _
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ x : m, ∑ i : m, a i * X i k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ x : m, ∑ i : m, a i * X i k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k
Tactic:
rw [Finset.sum_comm]
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ y : m, ∑ x : m, a y * X y k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝¹ : k ∈ Finset.univ
l : n
x✝ : l ∈ Finset.univ
⊢ ∑ y : m, ∑ x : m, a y * X y k * B k l * X x l * c x = ∑ x : m, ∑ x_1 : m, X x_1 l * (B k l * (c x_1 * a x)) * X x k
Tactic:
refine' Finset.sum_congr rfl fun kk _ => _
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝² : k ∈ Finset.univ
l : n
x✝¹ : l ∈ Finset.univ
kk : m
x✝ : kk ∈ Finset.univ
⊢ ∑ x : m, a kk * X kk k * B k l * X x l * c x = ∑ x : m, X x l * (B k l * (c x * a kk)) * X kk k
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝² : k ∈ Finset.univ
l : n
x✝¹ : l ∈ Finset.univ
kk : m
x✝ : kk ∈ Finset.univ
⊢ ∑ x : m, a kk * X kk k * B k l * X x l * c x = ∑ x : m, X x l * (B k l * (c x * a kk)) * X kk k
Tactic:
refine' Finset.sum_congr rfl fun ll _ => _
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝³ : k ∈ Finset.univ
l : n
x✝² : l ∈ Finset.univ
kk : m
x✝¹ : kk ∈ Finset.univ
ll : m
x✝ : ll ∈ Finset.univ
⊢ a kk * X kk k * B k l * X ll l * c ll = X ll l * (B k l * (c ll * a kk)) * X kk k
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l✝ : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝³ : k ∈ Finset.univ
l : n
x✝² : l ∈ Finset.univ
kk : m
x✝¹ : kk ∈ Finset.univ
ll : m
x✝ : ll ∈ Finset.univ
⊢ a kk * X kk k * B k l * X ll l * c ll = X ll l * (B k l * (c ll * a kk)) * X kk k
Tactic:
ring
Proof state after:
no goals
Theorem: MatrixCookbook.eq_525
Proof state before:
ι : Type ?u.77109
R : Type ?u.77112
l : Type ?u.77115
m : Type ?u.77118
n : Type u_1
p : Type ?u.77124
q : Type ?u.77127
r : Type ?u.77130
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
⊢ ‖(WithLp.equiv 1 (n → ℂ)).symm x‖ = ∑ i : n, Complex.abs (x i)
Tactic:
simpa using PiLp.norm_eq_of_nat 1 Nat.cast_one.symm ((WithLp.equiv 1 _).symm x)
Proof state after:
no goals
Theorem: MatrixCookbook.eq_526
Proof state before:
ι : Type ?u.87124
R : Type ?u.87127
l : Type ?u.87130
m : Type ?u.87133
n : Type u_1
p : Type ?u.87139
q : Type ?u.87142
r : Type ?u.87145
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
⊢ ↑(‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2) = star x ⬝ᵥ x
Tactic:
rw [← EuclideanSpace.inner_piLp_equiv_symm, inner_self_eq_norm_sq_to_K, Complex.ofReal_pow]
Proof state after:
ι : Type ?u.87124
R : Type ?u.87127
l : Type ?u.87130
m : Type ?u.87133
n : Type u_1
p : Type ?u.87139
q : Type ?u.87142
r : Type ?u.87145
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
⊢ ↑‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2 = ↑‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2
Theorem: MatrixCookbook.eq_526
Proof state before:
ι : Type ?u.87124
R : Type ?u.87127
l : Type ?u.87130
m : Type ?u.87133
n : Type u_1
p : Type ?u.87139
q : Type ?u.87142
r : Type ?u.87145
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
⊢ ↑‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2 = ↑‖(WithLp.equiv 2 (n → ℂ)).symm x‖ ^ 2
Tactic:
rfl
Proof state after:
no goals
Theorem: MatrixCookbook.eq_527
Proof state before:
ι : Type ?u.88920
R : Type ?u.88923
l : Type ?u.88926
m : Type ?u.88929
n : Type u_1
p✝ : Type ?u.88935
q : Type ?u.88938
r : Type ?u.88941
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p✝
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p✝
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
p : ℝ≥0∞
h : 0 < p.toReal
⊢ ‖(WithLp.equiv p (n → ℂ)).symm x‖ = (∑ i : n, Complex.abs (x i) ^ p.toReal) ^ (1 / p.toReal)
Tactic:
simp_rw [PiLp.norm_eq_sum h, WithLp.equiv_symm_pi_apply, Complex.norm_eq_abs]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_528
Proof state before:
ι : Type ?u.91759
R : Type ?u.91762
l : Type ?u.91765
m : Type ?u.91768
n : Type u_1
p : Type ?u.91774
q : Type ?u.91777
r : Type ?u.91780
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
⊢ ‖(WithLp.equiv ⊤ (n → ℂ)).symm x‖ = ⨆ i, Complex.abs (x i)
Tactic:
simp_rw [PiLp.norm_eq_ciSup, WithLp.equiv_symm_pi_apply, Complex.norm_eq_abs]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_531
Proof state before:
ι : Type ?u.93818
R : Type ?u.93821
l : Type ?u.93824
m : Type ?u.93827
n : Type u_1
p : Type ?u.93833
q : Type ?u.93836
r✝ : Type ?u.93839
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r✝
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r✝
inst✝ : Field R
r : ℝ
A : Matrix n n ℝ
⊢ ‖r • A‖ = |r| * ‖A‖
Tactic:
rw [norm_smul r A, Real.norm_eq_abs]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_533
Proof state before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖A‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Tactic:
simp_rw [linfty_opNorm_eq_opNorm]
Proof state after:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Theorem: MatrixCookbook.eq_533
Proof state before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Tactic:
rw [←ContinuousLinearMap.sSup_unit_ball_eq_norm]
Proof state after:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ sSup ((fun x => ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖) '' Metric.ball 0 1) =
    sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Theorem: MatrixCookbook.eq_533
Proof state before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ sSup ((fun x => ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖) '' Metric.ball 0 1) =
    sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: MatrixCookbook.eq_533
Proof state before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
this : ‖A‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
⊢ ‖A‖ = sSup {x | ∃ x_1, ∃ (_ : ‖x_1‖ = 1), ‖A *ᵥ x_1‖ = x}
Tactic:
simpa [Set.image, mem_sphere_zero_iff_norm] using this
Proof state after:
no goals
Theorem: MatrixCookbook.eq_540
Proof state before:
ι : Type ?u.132478
R : Type ?u.132481
l : Type ?u.132484
m : Type u_1
n : Type u_2
p : Type ?u.132493
q : Type ?u.132496
r : Type ?u.132499
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖A‖ = ↑(Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊)
Tactic:
rw [linfty_opNorm_def]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_541
Proof state before:
ι : Type ?u.134840
R : Type ?u.134843
l : Type ?u.134846
m : Type u_1
n : Type u_2
p : Type ?u.134855
q : Type ?u.134858
r : Type ?u.134861
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖A‖ = √(∑ i : m, ∑ j : n, ‖A i j‖ ^ 2)
Tactic:
rw [frobenius_norm_def, Real.sqrt_eq_rpow]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_542
Proof state before:
ι : Type ?u.137142
R : Type ?u.137145
l : Type ?u.137148
m : Type u_1
n : Type u_2
p : Type ?u.137157
q : Type ?u.137160
r : Type ?u.137163
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖A‖ = ↑(Finset.univ.sup fun ij => ‖A ij.1 ij.2‖₊)
Tactic:
simp_rw [← Finset.univ_product_univ, Finset.sup_product_left, ← Pi.nnnorm_def, coe_nnnorm]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_256
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (A.map Complex.ofReal' + B.map fun x => x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x => x • I)⁻¹
Tactic:
rw [eq_255 _ _ h]
Proof state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) • ((A + t • B).map Complex.ofReal' + (B - t • A).map fun x => x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x => x • I)⁻¹
Theorem: MatrixCookbook.eq_256
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) • ((A + t • B).map Complex.ofReal' + (B - t • A).map fun x => x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x => x • I)⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: MatrixCookbook.eq_257
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (A.map Complex.ofReal' + B.map fun x => x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I))
Tactic:
rw [eq_256 _ _ h]
Proof state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x =>
            x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I))
Theorem: MatrixCookbook.eq_257
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' -
          ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (B - t • A) * (A + t • B)).map fun x =>
            x • I)⁻¹ =
    (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I))
Tactic:
sorry
Proof state after:
no goals
Theorem: MatrixCookbook.eq_258
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (A.map Complex.ofReal' + B.map fun x => x • I)⁻¹ =
    (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
      (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal' -
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I)
Tactic:
rw [eq_257 _ _ h]
Proof state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I)) =
    (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
      (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal' -
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I)
Theorem: MatrixCookbook.eq_258
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (1 - t • I) •
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - ((B - t • A) * (A + t • B)⁻¹).map fun x => x • I)) =
    (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
      (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal' -
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I)
Tactic:
sorry
Proof state after:
no goals
Theorem: MatrixCookbook.eq_259
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ (A.map Complex.ofReal' + B.map fun x => x • I)⁻¹ =
    ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (1 - t • ((B - t • A) * (A + t • B)⁻¹))).map
        Complex.ofReal' -
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (t • 1 + (B - t • A) * (A + t • B)⁻¹)).map fun x =>
        x • I
Tactic:
rw [eq_258 _ _ h, mul_sub]
Proof state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal') -
      (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I) =
    ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (1 - t • ((B - t • A) * (A + t • B)⁻¹))).map
        Complex.ofReal' -
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (t • 1 + (B - t • A) * (A + t • B)⁻¹)).map fun x =>
        x • I
Theorem: MatrixCookbook.eq_259
Proof state before:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A B : Matrix m m ℝ
t : ℝ
h : IsUnit (A + t • B)
⊢ ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (1 - t • ((B - t • A) * (A + t • B)⁻¹).map Complex.ofReal') -
      (A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹.map Complex.ofReal' *
        (t • 1 + (B - t • A) * (A + t • B)⁻¹).map fun x => x • I) =
    ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (1 - t • ((B - t • A) * (A + t • B)⁻¹))).map
        Complex.ofReal' -
      ((A + t • B + (B - t • A) * (A + t • B)⁻¹ * (B - t • A))⁻¹ * (t • 1 + (B - t • A) * (A + t • B)⁻¹)).map fun x =>
        x • I
Tactic:
sorry
Proof state after:
no goals
Theorem: MatrixCookbook.eq_399
Proof state before:
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₁ := A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁;
    let i := inst✝;
    (⅟C₁).fromBlocks (-(⅟C₁ * A₁₂ * ⅟A₂₂)) (-(⅟A₂₂ * A₂₁ * ⅟C₁)) (⅟A₂₂ + ⅟A₂₂ * A₂₁ * ⅟C₁ * A₁₂ * ⅟A₂₂)
Tactic:
letI := fromBlocks₂₂Invertible A₁₁ A₁₂ A₂₁ A₂₂
Proof state after:
R : Type u_2
l : Type ?u.19120
m : Type u_1
n : Type u_3
p : Type ?u.19129
q : Type ?u.19132
r : Type ?u.19135
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
A₁₁ : Matrix m m R
A₁₂ : Matrix m n R
A₂₁ : Matrix n m R
A₂₂ : Matrix n n R
inst✝¹ : Invertible A₂₂
inst✝ : Invertible (A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁)
this : Invertible (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂) := A₁₁.fromBlocks₂₂Invertible A₁₂ A₂₁ A₂₂
⊢ (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)⁻¹ =
    let C₁ := A₁₁ - A₁₂ * ⅟A₂₂ * A₂₁;
    let i := inst✝;
    (⅟C₁).fromBlocks (-(⅟C₁ * A₁₂ * ⅟A₂₂)) (-(⅟A₂₂ * A₂₁ * ⅟C₁)) (⅟A₂₂ + ⅟A₂₂ * A₂₁ * ⅟C₁ * A₁₂ * ⅟A₂₂)