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

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : (leastSquaresVec a).optimal x
⊢ x = mean a
Tactic:
apply leastSquares_optimal_eq_mean hn a
State after:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : (leastSquaresVec a).optimal x
⊢ (leastSquares a).optimal x

State before:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : (leastSquaresVec a).optimal x
⊢ (leastSquares a).optimal x
Tactic:
simp [leastSquaresVec, leastSquares, optimal, feasible] at h ⊢
State after:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), Vec.sum ((a - Vec.const n x) ^ 2) ≤ Vec.sum ((a - Vec.const n y) ^ 2)
⊢ ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2

State before:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), Vec.sum ((a - Vec.const n x) ^ 2) ≤ Vec.sum ((a - Vec.const n y) ^ 2)
⊢ ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
Tactic:
intros y
State after:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), Vec.sum ((a - Vec.const n x) ^ 2) ≤ Vec.sum ((a - Vec.const n y) ^ 2)
y : ℝ
⊢ ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2

State before:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), Vec.sum ((a - Vec.const n x) ^ 2) ≤ Vec.sum ((a - Vec.const n y) ^ 2)
y : ℝ
⊢ ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
Tactic:
simp only [Vec.sum, Pi.pow_apply, Pi.sub_apply, Vec.const, rpow_two] at h
State after:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
y : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
⊢ ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2

State before:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
y : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
⊢ ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
Tactic:
exact h y
State after:
no goals