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

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ i : Fin n, (a i - x) ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
Tactic:
calc
_ = ∑ i, ((a i) ^ 2 - 2 * (a i) * x + (x ^ 2)) := by
  congr; funext i; simp; ring
_ = ∑ i, ((a i) ^ 2) - 2 * x * ∑ i, (a i) + n * (x ^ 2) := by
  rw [sum_add_distrib, sum_sub_distrib, ← sum_mul, ← mul_sum]; simp [sum_const]; ring
_ = n * mean (a ^ 2) - 2 * x * n * mean a + n * (x ^ 2) := by
  simp [mean]; field_simp; ring
_ = n * ((x - mean a) ^ 2 + (mean (a ^ 2) - (mean a) ^ 2)) := by
  simp [mean]; field_simp; ring
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ i : Fin n, (a i - x) ^ 2 = ∑ i : Fin n, (a i ^ 2 - 2 * a i * x + x ^ 2)
Tactic:
congr
State after:
case e_f
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ (fun i => (a i - x) ^ 2) = fun i => a i ^ 2 - 2 * a i * x + x ^ 2

State before:
case e_f
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ (fun i => (a i - x) ^ 2) = fun i => a i ^ 2 - 2 * a i * x + x ^ 2
Tactic:
funext i
State after:
case e_f.h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
i : Fin n
⊢ (a i - x) ^ 2 = a i ^ 2 - 2 * a i * x + x ^ 2

State before:
case e_f.h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
i : Fin n
⊢ (a i - x) ^ 2 = a i ^ 2 - 2 * a i * x + x ^ 2
Tactic:
ring
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ i : Fin n, (a i ^ 2 - 2 * a i * x + x ^ 2) = ∑ i : Fin n, a i ^ 2 - 2 * x * ∑ i : Fin n, a i + ↑n * x ^ 2
Tactic:
rw [sum_add_distrib, sum_sub_distrib, ← sum_mul, ← mul_sum]
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ x : Fin n, a x ^ 2 - (2 * ∑ i : Fin n, a i) * x + ∑ x_1 : Fin n, x ^ 2 =
    ∑ i : Fin n, a i ^ 2 - 2 * x * ∑ i : Fin n, a i + ↑n * x ^ 2

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ x : Fin n, a x ^ 2 - (2 * ∑ i : Fin n, a i) * x + ∑ x_1 : Fin n, x ^ 2 =
    ∑ i : Fin n, a i ^ 2 - 2 * x * ∑ i : Fin n, a i + ↑n * x ^ 2
Tactic:
simp [sum_const]
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ (2 * ∑ i : Fin n, a i) * x = 2 * x * ∑ i : Fin n, a i

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ (2 * ∑ i : Fin n, a i) * x = 2 * x * ∑ i : Fin n, a i
Tactic:
ring
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ i : Fin n, a i ^ 2 - 2 * x * ∑ i : Fin n, a i + ↑n * x ^ 2 = ↑n * mean (a ^ 2) - 2 * x * ↑n * mean a + ↑n * x ^ 2
Tactic:
simp [mean]
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ x : Fin n, a x ^ 2 - 2 * x * ∑ i : Fin n, a i =
    ↑n * ((↑n)⁻¹ * ∑ x : Fin n, a x ^ 2) - 2 * x * ↑n * ((↑n)⁻¹ * ∑ i : Fin n, a i)

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ∑ x : Fin n, a x ^ 2 - 2 * x * ∑ i : Fin n, a i =
    ↑n * ((↑n)⁻¹ * ∑ x : Fin n, a x ^ 2) - 2 * x * ↑n * ((↑n)⁻¹ * ∑ i : Fin n, a i)
Tactic:
field_simp
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ (∑ x : Fin n, a x ^ 2 - 2 * x * ∑ i : Fin n, a i) * ↑n = (∑ x : Fin n, a x ^ 2) * ↑n - 2 * x * ↑n * ∑ i : Fin n, a i

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ (∑ x : Fin n, a x ^ 2 - 2 * x * ∑ i : Fin n, a i) * ↑n = (∑ x : Fin n, a x ^ 2) * ↑n - 2 * x * ↑n * ∑ i : Fin n, a i
Tactic:
ring
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ↑n * mean (a ^ 2) - 2 * x * ↑n * mean a + ↑n * x ^ 2 = ↑n * ((x - mean a) ^ 2 + (mean (a ^ 2) - mean a ^ 2))
Tactic:
simp [mean]
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ↑n * ((↑n)⁻¹ * ∑ x : Fin n, a x ^ 2) - 2 * x * ↑n * ((↑n)⁻¹ * ∑ i : Fin n, a i) + ↑n * x ^ 2 =
    ↑n * ((x - (↑n)⁻¹ * ∑ i : Fin n, a i) ^ 2 + ((↑n)⁻¹ * ∑ x : Fin n, a x ^ 2 - ((↑n)⁻¹ * ∑ i : Fin n, a i) ^ 2))

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ↑n * ((↑n)⁻¹ * ∑ x : Fin n, a x ^ 2) - 2 * x * ↑n * ((↑n)⁻¹ * ∑ i : Fin n, a i) + ↑n * x ^ 2 =
    ↑n * ((x - (↑n)⁻¹ * ∑ i : Fin n, a i) ^ 2 + ((↑n)⁻¹ * ∑ x : Fin n, a x ^ 2 - ((↑n)⁻¹ * ∑ i : Fin n, a i) ^ 2))
Tactic:
field_simp
State after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ((∑ x : Fin n, a x ^ 2) * ↑n - 2 * x * ↑n * ∑ i : Fin n, a i + ↑n * x ^ 2 * ↑n) * (↑n ^ 2 * (↑n * ↑n ^ 2)) =
    ↑n *
        ((x * ↑n - ∑ i : Fin n, a i) ^ 2 * (↑n * ↑n ^ 2) +
          ((∑ x : Fin n, a x ^ 2) * ↑n ^ 2 - ↑n * (∑ i : Fin n, a i) ^ 2) * ↑n ^ 2) *
      ↑n

State before:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ ((∑ x : Fin n, a x ^ 2) * ↑n - 2 * x * ↑n * ∑ i : Fin n, a i + ↑n * x ^ 2 * ↑n) * (↑n ^ 2 * (↑n * ↑n ^ 2)) =
    ↑n *
        ((x * ↑n - ∑ i : Fin n, a i) ^ 2 * (↑n * ↑n ^ 2) +
          ((∑ x : Fin n, a x ^ 2) * ↑n ^ 2 - ↑n * (∑ i : Fin n, a i) ^ 2) * ↑n ^ 2) *
      ↑n
Tactic:
ring
State after:
no goals