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

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

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
⊢ x = mean a
Tactic:
replace h : ∀ y, (x - mean a) ^ 2 ≤ (y - mean a) ^ 2  := by
  intros y
  have hy := h y
  have h_rw_x := leastSquares_alt_objFun hn a x
  have h_rw_y := leastSquares_alt_objFun hn a y
  simp only [rpow_two] at h_rw_x h_rw_y ⊢
  rwa [h_rw_x, h_rw_y, mul_le_mul_left (by positivity), add_le_add_iff_right] at hy
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
⊢ x = mean a

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
⊢ x = mean a
Tactic:
have hmean := h (mean a)
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
hmean : (x - mean a) ^ 2 ≤ (mean a - mean a) ^ 2
⊢ x = mean a

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
hmean : (x - mean a) ^ 2 ≤ (mean a - mean a) ^ 2
⊢ x = mean a
Tactic:
simp at hmean
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
hmean : (x - mean a) ^ 2 ≤ 0
⊢ x = mean a

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
hmean : (x - mean a) ^ 2 ≤ 0
⊢ x = mean a
Tactic:
have h_sq_eq_zero := le_antisymm hmean (sq_nonneg _)
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
hmean : (x - mean a) ^ 2 ≤ 0
h_sq_eq_zero : (x - mean a) ^ 2 = 0
⊢ x = mean a

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
hmean : (x - mean a) ^ 2 ≤ 0
h_sq_eq_zero : (x - mean a) ^ 2 = 0
⊢ x = mean a
Tactic:
rwa [sq_eq_zero_iff, sub_eq_zero] at h_sq_eq_zero
State after:
no goals

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

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
Tactic:
have hy := h y
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
Tactic:
have h_rw_x := leastSquares_alt_objFun hn a x
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
h_rw_x : ∑ i : Fin n, (a i - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
h_rw_x : ∑ i : Fin n, (a i - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
Tactic:
have h_rw_y := leastSquares_alt_objFun hn a y
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
h_rw_x : ∑ i : Fin n, (a i - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
h_rw_y : ∑ i : Fin n, (a i - y) ^ 2 = ↑n * ((y - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
h_rw_x : ∑ i : Fin n, (a i - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
h_rw_y : ∑ i : Fin n, (a i - y) ^ 2 = ↑n * ((y - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
Tactic:
simp only [rpow_two] at h_rw_x h_rw_y ⊢
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
h_rw_x : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
h_rw_y : ∑ x : Fin n, (a x - y) ^ 2 = ↑n * ((y - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
h_rw_x : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
h_rw_y : ∑ x : Fin n, (a x - y) ^ 2 = ↑n * ((y - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
⊢ (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
Tactic:
rwa [h_rw_x, h_rw_y, mul_le_mul_left (by positivity), add_le_add_iff_right] at hy
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), ∑ x_1 : Fin n, (a x_1 - x) ^ 2 ≤ ∑ x : Fin n, (a x - y) ^ 2
y : ℝ
hy : ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2)) ≤ ↑n * ((y - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
h_rw_x : ∑ x_1 : Fin n, (a x_1 - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
h_rw_y : ∑ x : Fin n, (a x - y) ^ 2 = ↑n * ((y - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
⊢ 0 < ↑n
Tactic:
positivity
State after:
no goals