Theorem: FittingSphere.optimal_convex_implies_optimal_t (CvxLean/Examples/FittingSphere.lean)

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt : (fittingSphereConvex n m x).optimal (c, t)
⊢ (fittingSphereT n m x).optimal (c, t)
Tactic:
simp [fittingSphereT, fittingSphereConvex, optimal, feasible] at h_opt ⊢
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
⊢ 0 ≤ t + ‖c‖ ^ 2 ∧
    ∀ (a : Fin n → ℝ) (b : ℝ),
      0 ≤ b + ‖a‖ ^ 2 →
        Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
          Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
⊢ 0 ≤ t + ‖c‖ ^ 2 ∧
    ∀ (a : Fin n → ℝ) (b : ℝ),
      0 ≤ b + ‖a‖ ^ 2 →
        Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
          Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
Tactic:
constructor
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
⊢ 0 ≤ t + ‖c‖ ^ 2

case right
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
⊢ ∀ (a : Fin n → ℝ) (b : ℝ),
    0 ≤ b + ‖a‖ ^ 2 →
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
        Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
let a := Vec.norm x ^ 2 - 2 * mulVec x c
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
⊢ 0 ≤ t + ‖c‖ ^ 2

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
have h_ls : optimal (leastSquaresVec a) t := by
  refine ⟨trivial, ?_⟩
  intros y _
  simp [objFun, leastSquaresVec]
  exact h_opt c y
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
⊢ 0 ≤ t + ‖c‖ ^ 2

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
have h_t_eq := leastSquaresVec_optimal_eq_mean hm a t h_ls
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
⊢ 0 ≤ t + ‖c‖ ^ 2

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
have h_c2_eq : ‖c‖ ^ 2 = (1 / m) * ∑ i : Fin m, ‖c‖ ^ 2 := by
  simp [sum_const]
  field_simp
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ 0 ≤ t + ‖c‖ ^ 2

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
have h_t_add_c2_eq : t + ‖c‖ ^ 2 = (1 / m) * ∑ i, ‖(x i) - c‖ ^ 2 := by
  rw [h_t_eq]; dsimp [mean]
  rw [h_c2_eq, mul_sum, mul_sum, mul_sum, ← sum_add_distrib]
  congr; funext i; rw [← mul_add]
  congr; simp [Vec.norm]
  rw [norm_sub_sq (𝕜 := ℝ) (E := Fin n → ℝ)]
  simp [a]; congr
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ 0 ≤ t + ‖c‖ ^ 2

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
rw [← rpow_two, h_t_add_c2_eq]
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ 0 ≤ 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ 0 ≤ 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
Tactic:
apply mul_nonneg (by norm_num)
State after:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ 0 ≤ ∑ i : Fin m, ‖x i - c‖ ^ 2

State before:
case left
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ 0 ≤ ∑ i : Fin m, ‖x i - c‖ ^ 2
Tactic:
apply sum_nonneg
State after:
case left.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ ∀ i ∈ univ, 0 ≤ ‖x i - c‖ ^ 2

State before:
case left.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ ∀ i ∈ univ, 0 ≤ ‖x i - c‖ ^ 2
Tactic:
intros i _
State after:
case left.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
i : Fin m
a✝ : i ∈ univ
⊢ 0 ≤ ‖x i - c‖ ^ 2

State before:
case left.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
i : Fin m
a✝ : i ∈ univ
⊢ 0 ≤ ‖x i - c‖ ^ 2
Tactic:
exact sq_nonneg _
State after:
no goals

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
⊢ (leastSquaresVec a).optimal t
Tactic:
refine ⟨trivial, ?_⟩
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
⊢ ∀ (y : ℝ), (leastSquaresVec a).feasible y → (leastSquaresVec a).objFun t ≤ (leastSquaresVec a).objFun y

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
⊢ ∀ (y : ℝ), (leastSquaresVec a).feasible y → (leastSquaresVec a).objFun t ≤ (leastSquaresVec a).objFun y
Tactic:
intros y _
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
y : ℝ
a✝ : (leastSquaresVec a).feasible y
⊢ (leastSquaresVec a).objFun t ≤ (leastSquaresVec a).objFun y

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
y : ℝ
a✝ : (leastSquaresVec a).feasible y
⊢ (leastSquaresVec a).objFun t ≤ (leastSquaresVec a).objFun y
Tactic:
simp [objFun, leastSquaresVec]
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
y : ℝ
a✝ : (leastSquaresVec a).feasible y
⊢ Vec.sum ((a - Vec.const m t) ^ 2) ≤ Vec.sum ((a - Vec.const m y) ^ 2)

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
y : ℝ
a✝ : (leastSquaresVec a).feasible y
⊢ Vec.sum ((a - Vec.const m t) ^ 2) ≤ Vec.sum ((a - Vec.const m y) ^ 2)
Tactic:
exact h_opt c y
State after:
no goals

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
⊢ ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
Tactic:
simp [sum_const]
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
⊢ ‖c‖ ^ 2 = (↑m)⁻¹ * (↑m * ‖c‖ ^ 2)

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
⊢ ‖c‖ ^ 2 = (↑m)⁻¹ * (↑m * ‖c‖ ^ 2)
Tactic:
field_simp
State after:
no goals

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
Tactic:
rw [h_t_eq]
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ mean a + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ mean a + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
Tactic:
dsimp [mean]
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ 1 / ↑m * ∑ i : Fin m, a i + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ 1 / ↑m * ∑ i : Fin m, a i + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
Tactic:
rw [h_c2_eq, mul_sum, mul_sum, mul_sum, ← sum_add_distrib]
State after:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ ∑ x : Fin m, (1 / ↑m * a x + 1 / ↑m * ‖c‖ ^ 2) = ∑ i : Fin m, 1 / ↑m * ‖x i - c‖ ^ 2

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ ∑ x : Fin m, (1 / ↑m * a x + 1 / ↑m * ‖c‖ ^ 2) = ∑ i : Fin m, 1 / ↑m * ‖x i - c‖ ^ 2
Tactic:
congr
State after:
case e_f
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ (fun x => 1 / ↑m * a x + 1 / ↑m * ‖c‖ ^ 2) = fun i => 1 / ↑m * ‖x i - c‖ ^ 2

State before:
case e_f
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
⊢ (fun x => 1 / ↑m * a x + 1 / ↑m * ‖c‖ ^ 2) = fun i => 1 / ↑m * ‖x i - c‖ ^ 2
Tactic:
funext i
State after:
case e_f.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ 1 / ↑m * a i + 1 / ↑m * ‖c‖ ^ 2 = 1 / ↑m * ‖x i - c‖ ^ 2

State before:
case e_f.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ 1 / ↑m * a i + 1 / ↑m * ‖c‖ ^ 2 = 1 / ↑m * ‖x i - c‖ ^ 2
Tactic:
rw [← mul_add]
State after:
case e_f.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ 1 / ↑m * (a i + ‖c‖ ^ 2) = 1 / ↑m * ‖x i - c‖ ^ 2

State before:
case e_f.h
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ 1 / ↑m * (a i + ‖c‖ ^ 2) = 1 / ↑m * ‖x i - c‖ ^ 2
Tactic:
congr
State after:
case e_f.h.e_a
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ a i + ‖c‖ ^ 2 = ‖x i - c‖ ^ 2

State before:
case e_f.h.e_a
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ a i + ‖c‖ ^ 2 = ‖x i - c‖ ^ 2
Tactic:
rw [norm_sub_sq (𝕜 := ℝ) (E := Fin n → ℝ)]
State after:
case e_f.h.e_a
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ a i + ‖c‖ ^ 2 = ‖x i‖ ^ 2 - 2 * RCLike.re ⟪x i, c⟫_ℝ + ‖c‖ ^ 2

State before:
case e_f.h.e_a
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ a i + ‖c‖ ^ 2 = ‖x i‖ ^ 2 - 2 * RCLike.re ⟪x i, c⟫_ℝ + ‖c‖ ^ 2
Tactic:
simp [a]
State after:
case e_f.h.e_a
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ Vec.norm x i ^ 2 - 2 * (x *ᵥ c) i = ‖x i‖ ^ 2 - 2 * ⟪x i, c⟫_ℝ

State before:
case e_f.h.e_a
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
i : Fin m
⊢ Vec.norm x i ^ 2 - 2 * (x *ᵥ c) i = ‖x i‖ ^ 2 - 2 * ⟪x i, c⟫_ℝ
Tactic:
congr
State after:
no goals

State before:
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
a : Fin m → ℝ := Vec.norm x ^ 2 - 2 * x *ᵥ c
h_ls : (leastSquaresVec a).optimal t
h_t_eq : t = mean a
h_c2_eq : ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖c‖ ^ 2
h_t_add_c2_eq : t + ‖c‖ ^ 2 = 1 / ↑m * ∑ i : Fin m, ‖x i - c‖ ^ 2
⊢ 0 ≤ 1 / ↑m
Tactic:
norm_num
State after:
no goals

State before:
case right
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
⊢ ∀ (a : Fin n → ℝ) (b : ℝ),
    0 ≤ b + ‖a‖ ^ 2 →
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
        Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
Tactic:
intros c' x' _
State after:
case right
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
c' : Fin n → ℝ
x' : ℝ
a✝ : 0 ≤ x' + ‖c'‖ ^ 2
⊢ Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c' - Vec.const m x') ^ 2)

State before:
case right
n m : ℕ
x : Fin m → Fin n → ℝ
hm : 0 < m
c : Fin n → ℝ
t : ℝ
h_opt :
  ∀ (a : Fin n → ℝ) (b : ℝ),
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
      Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ a - Vec.const m b) ^ 2)
c' : Fin n → ℝ
x' : ℝ
a✝ : 0 ≤ x' + ‖c'‖ ^ 2
⊢ Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c - Vec.const m t) ^ 2) ≤
    Vec.sum ((Vec.norm x ^ 2 - 2 * x *ᵥ c' - Vec.const m x') ^ 2)
Tactic:
exact h_opt c' x'
State after:
no goals