internlm/Lean-Github huggingface dataset:
Theorem: Matrix.det_add_det_le_det_add'
Proof state before:
case h
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
this : IsUnit sqrtA
IsHermitian_sqrtA : sqrtA⁻¹.IsHermitian
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ sqrtA * sqrtA * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (sqrtA * sqrtA + B) * sqrtA⁻¹
Tactic:
rw [Matrix.mul_add, Matrix.mul_one, Matrix.mul_add, Matrix.add_mul,
  Matrix.mul_assoc, Matrix.mul_assoc, Matrix.mul_assoc, Matrix.mul_assoc,
  ← Matrix.mul_assoc _ _ (B * _),
  Matrix.mul_nonsing_inv _ isUnit_det_sqrtA, Matrix.one_mul, Matrix.mul_one,
  hA.posSemidef.sqrt_mul_sqrt, Matrix.mul_assoc]
Proof state after:
no goals
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
⊢ A.det + B.det ≤ (A + B).det
Tactic:
by_cases hA' : A.det = 0
Proof state after:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ by_cases hB' : B.det = 0
  { simp [hA', hB']
    apply (hA.add hB).det_nonneg }
  { rw [add_comm A B, add_comm A.det B.det]
    apply det_add_det_le_det_add' _ _ (hB.PosDef_iff_det_ne_zero.2 hB') hA } }
Proof state after:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ apply det_add_det_le_det_add' _ _ (hA.PosDef_iff_det_ne_zero.2 hA') hB }
Proof state after:
no goals
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
by_cases hB' : B.det = 0
Proof state after:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ A.det + B.det ≤ (A + B).det

case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ simp [hA', hB']
  apply (hA.add hB).det_nonneg }
Proof state after:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
{ rw [add_comm A B, add_comm A.det B.det]
  apply det_add_det_le_det_add' _ _ (hB.PosDef_iff_det_ne_zero.2 hB') hA }
Proof state after:
no goals
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
simp [hA', hB']
Proof state after:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ 0 ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case pos
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : B.det = 0
⊢ 0 ≤ (A + B).det
Tactic:
apply (hA.add hB).det_nonneg
Proof state after:
no goals
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
rw [add_comm A B, add_comm A.det B.det]
Proof state after:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ B.det + A.det ≤ (B + A).det
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : A.det = 0
hB' : ¬B.det = 0
⊢ B.det + A.det ≤ (B + A).det
Tactic:
apply det_add_det_le_det_add' _ _ (hB.PosDef_iff_det_ne_zero.2 hB') hA
Proof state after:
no goals
Theorem: Matrix.det_add_det_le_det_add
Proof state before:
case neg
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosSemidef
hB : B.PosSemidef
hA' : ¬A.det = 0
⊢ A.det + B.det ≤ (A + B).det
Tactic:
apply det_add_det_le_det_add' _ _ (hA.PosDef_iff_det_ne_zero.2 hA') hB
Proof state after:
no goals
Theorem: Real.abs_le_of_sqrt_sq_add_nonneg_le
Proof state before:
a b c : ℝ
hb : 0 ≤ b
h : (a ^ 2 + b).sqrt ≤ c
⊢ |a| ≤ c
Tactic:
rw [sqrt_le_iff] at h
Proof state after:
a b c : ℝ
hb : 0 ≤ b
h : 0 ≤ c ∧ a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c
Theorem: Real.abs_le_of_sqrt_sq_add_nonneg_le
Proof state before:
a b c : ℝ
hb : 0 ≤ b
h : 0 ≤ c ∧ a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c
Tactic:
replace ⟨hc, h⟩ := h
Proof state after:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c
Theorem: Real.abs_le_of_sqrt_sq_add_nonneg_le
Proof state before:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 + b ≤ c ^ 2
⊢ |a| ≤ c
Tactic:
replace h := le_trans (le_add_of_nonneg_right hb) h
Proof state after:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 ≤ c ^ 2
⊢ |a| ≤ c
Theorem: Real.abs_le_of_sqrt_sq_add_nonneg_le
Proof state before:
a b c : ℝ
hb : 0 ≤ b
hc : 0 ≤ c
h : a ^ 2 ≤ c ^ 2
⊢ |a| ≤ c
Tactic:
rwa [rpow_two, sq_le_sq, abs_of_nonneg hc] at h
Proof state after:
no goals
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x = y
⊢ x.log = y.log
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
⊢ x = y
Tactic:
have hxmem := Set.mem_Ioi.2 hx
Proof state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
⊢ x = y
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
⊢ x = y
Tactic:
have hymem := Set.mem_Ioi.2 hy
Proof state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
⊢ x = y
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
⊢ x = y
Tactic:
have heq : Set.restrict (Set.Ioi 0) log ⟨x, hxmem⟩ =
  Set.restrict (Set.Ioi 0) log ⟨y, hymem⟩ := by
  simp [h]
Proof state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
⊢ x = y
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
⊢ x = y
Tactic:
have h := log_injOn_pos.injective heq
Proof state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : ⟨x, hxmem⟩ = ⟨y, hymem⟩
⊢ x = y
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : ⟨x, hxmem⟩ = ⟨y, hymem⟩
⊢ x = y
Tactic:
simp [Subtype.eq] at h
Proof state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : x = y
⊢ x = y
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h✝ : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
heq : (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
h : x = y
⊢ x = y
Tactic:
exact h
Proof state after:
no goals
Theorem: Real.log_eq_log
Proof state before:
x y : ℝ
hx : 0 < x
hy : 0 < y
h : x.log = y.log
hxmem : x ∈ Set.Ioi 0
hymem : y ∈ Set.Ioi 0
⊢ (Set.Ioi 0).restrict log ⟨x, hxmem⟩ = (Set.Ioi 0).restrict log ⟨y, hymem⟩
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Real.div_pow_eq_mul_pow_neg
Proof state before:
a b c : ℝ
hb : 0 ≤ b
⊢ a / b ^ c = a * b ^ (-c)
Tactic:
rw [div_eq_mul_inv, ← rpow_neg hb]
Proof state after:
no goals
Theorem: Real.one_div_eq_pow_neg_one
Proof state before:
a : ℝ
ha : 0 < a
⊢ 1 / a = a ^ (-1)
Tactic:
rw [rpow_neg (le_of_lt ha), rpow_one, div_eq_mul_inv, one_mul]
Proof state after:
no goals
Theorem: Real.inv_eq_pow_neg_one
Proof state before:
a : ℝ
ha : 0 < a
⊢ a⁻¹ = a ^ (-1)
Tactic:
rw [inv_eq_one_div, one_div_eq_pow_neg_one ha]
Proof state after:
no goals
Theorem: Real.pow_half_two
Proof state before:
x : ℝ
hx : 0 ≤ x
⊢ (x ^ (1 / 2)) ^ 2 = x
Tactic:
show rpow (rpow _ _) _ = _
Proof state after:
x : ℝ
hx : 0 ≤ x
⊢ (x.rpow (1 / 2)).rpow 2 = x
Theorem: Real.pow_half_two
Proof state before:
x : ℝ
hx : 0 ≤ x
⊢ (x.rpow (1 / 2)).rpow 2 = x
Tactic:
rw [rpow_eq_pow, rpow_eq_pow, ← rpow_mul hx]
Proof state after:
x : ℝ
hx : 0 ≤ x
⊢ x ^ (1 / 2 * 2) = x
Theorem: Real.pow_half_two
Proof state before:
x : ℝ
hx : 0 ≤ x
⊢ x ^ (1 / 2 * 2) = x
Tactic:
norm_num
Proof state after:
no goals
Theorem: Real.pow_two_le_pow_two
Proof state before:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ^ 2 ≤ y ^ 2 ↔ x ≤ y
Tactic:
rw [rpow_two, rpow_two, sq_le_sq, abs_of_nonneg hx, abs_of_nonneg hy]
Proof state after:
no goals
Theorem: Real.binomial_two
Proof state before:
x y : ℝ
⊢ (x + y) ^ 2 = x ^ 2 + (2 * (x * y) + y ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: Real.rpow_eq_mul_rpow_pred
Proof state before:
x y : ℝ
hx : x ≠ 0
⊢ x ^ y = x * x ^ (y - 1)
Tactic:
conv => left; rw [(by ring : y = (y - 1) + 1), rpow_add_one hx, mul_comm]
Proof state after:
no goals
Theorem: Real.rpow_eq_mul_rpow_pred
Proof state before:
x y : ℝ
hx : x ≠ 0
⊢ y = y - 1 + 1
Tactic:
ring
Proof state after:
no goals
Theorem: Real.exp_neg_eq_one_div
Proof state before:
x : ℝ
⊢ (-x).exp = 1 / x.exp
Tactic:
rw [exp_neg, inv_eq_one_div]
Proof state after:
no goals
Theorem: Minimization.Relaxation.induces_original_problem_optimality
Proof state before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
⊢ p.optimal (phi_inv y)
Tactic:
refine ⟨h_feas_y, ?_⟩
Proof state after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
⊢ ∀ (y_1 : D), p.feasible y_1 → p.objFun (phi_inv y) ≤ p.objFun y_1
Theorem: Minimization.Relaxation.induces_original_problem_optimality
Proof state before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
⊢ ∀ (y_1 : D), p.feasible y_1 → p.objFun (phi_inv y) ≤ p.objFun y_1
Tactic:
intros x h_feas_x
Proof state after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ p.objFun (phi_inv y) ≤ p.objFun x
Theorem: Minimization.Relaxation.induces_original_problem_optimality
Proof state before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ p.objFun (phi_inv y) ≤ p.objFun x
Tactic:
rw [h_objFun _ h_feas_y, phi_left_inv]
Proof state after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ q.objFun y ≤ p.objFun x
Theorem: Minimization.Relaxation.induces_original_problem_optimality
Proof state before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ q.objFun y ≤ p.objFun x
Tactic:
have h_bound := h_opt_y.2 (Rx.phi x) (Rx.phi_feasibility x h_feas_x)
Proof state after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
h_bound : q.objFun y ≤ q.objFun (Rx.phi x)
⊢ q.objFun y ≤ p.objFun x
Theorem: Minimization.Relaxation.induces_original_problem_optimality
Proof state before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
h_bound : q.objFun y ≤ q.objFun (Rx.phi x)
⊢ q.objFun y ≤ p.objFun x
Tactic:
rwa [← h_objFun _ h_feas_x] at h_bound
Proof state after:
no goals
Theorem: Matrix.PosSemidef_zero
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
⊢ PosSemidef 0
Tactic:
simp [PosSemidef]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
have h_D_eq : D = Z * A⁻¹ * Zᴴ :=
  calc D
    = D * D⁻¹ * D := by
        rw [hD, Matrix.mul_inv_of_invertible, Matrix.one_mul]
  _ = D * (LDL.lowerInv hA * A * (LDL.lowerInv hA)ᵀ)⁻¹ * Dᵀ := by
        erw [hD, LDL.diag, diagonal_transpose, ← LDL.diag, LDL.diag_eq_lowerInv_conj]
        rfl
  _ = D * (LDL.lower hA)ᵀ * A⁻¹ * (D * (LDL.lower hA)ᵀ)ᵀ := by
        simp only [hD, LDL.lower, transpose_mul, transpose_transpose, transpose_nonsing_inv,
          Matrix.mul_assoc, Matrix.mul_inv_rev]
  _ = Z * A⁻¹ * Zᴴ := by
        rw [hZ, hD]; rfl
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
haveI := hA.Invertible
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
this : Invertible A
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
this : Invertible A
⊢ (D.fromBlocks Z Z.transpose A).PosSemidef
Tactic:
erw [PosSemidef.fromBlocks₂₂ _ _ hA]
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
this : Invertible A
⊢ (D - Z * A⁻¹ * Z.conjTranspose).PosSemidef
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
h_D_eq : D = Z * A⁻¹ * Z.conjTranspose
this : Invertible A
⊢ (D - Z * A⁻¹ * Z.conjTranspose).PosSemidef
Tactic:
simp [h_D_eq]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D = D * D⁻¹ * D
Tactic:
rw [hD, Matrix.mul_inv_of_invertible, Matrix.one_mul]
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D * D⁻¹ * D = D * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ * D.transpose
Tactic:
erw [hD, LDL.diag, diagonal_transpose, ← LDL.diag, LDL.diag_eq_lowerInv_conj]
Proof state after:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose) =
    LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose) =
    LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ *
      (LDL.lowerInv hA * A * (LDL.lowerInv hA).conjTranspose)
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.LogDetAtom.feasibility_PosDef
Proof state before:
n : Type
inst✝³ : Fintype n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
𝕜 : Type
inst✝ : RCLike 𝕜
A : Matrix n n ℝ
hA : A.PosDef
D Z : Matrix n n ℝ
hD : D = LDL.diag hA
hZ : Z = LDL.diag hA * (LDL.lower hA).transpose
⊢ D * (LDL.lowerInv hA * A * (LDL.lowerInv hA).transpose)⁻¹ * D.transpose =
    D * (LDL.lower hA).transpose * A⁻¹ * (D * (LDL.lower hA).transpose).transpose
Tactic:
simp only [hD, LDL.lower, transpose_mul, transpose_transpose, transpose_nonsing_inv,
  Matrix.mul_assoc, Matrix.mul_inv_rev]
Proof state after:
no goals