internlm/Lean-Github huggingface dataset:
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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)
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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 _
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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 _
Proof state after:
no goals
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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, ?_⟩
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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 _
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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)
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof state after:
no goals
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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)
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof state after:
no goals
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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 → ℝ)]
Proof 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
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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]
Proof 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⟫_ℝ
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof state after:
no goals
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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
Proof state after:
no goals
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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' _
Proof 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)
Theorem: FittingSphere.optimal_convex_implies_optimal_t
Proof 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'
Proof state after:
no goals
Theorem: repr_gramSchmidt_diagonal
Proof state before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
⊢ (b.repr (gramSchmidt 𝕜 (⇑b) i)) i = 1
Tactic:
rw [gramSchmidt_def, map_sub, Finsupp.sub_apply, Basis.repr_self, Finsupp.single_eq_same,
  sub_eq_self, map_sum, Finsupp.coe_finset_sum, Finset.sum_apply, Finset.sum_eq_zero]
Proof state after:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
⊢ ∀ x ∈ Finset.Iio i, (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) x})) (b i))) i = 0
Theorem: repr_gramSchmidt_diagonal
Proof state before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
⊢ ∀ x ∈ Finset.Iio i, (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) x})) (b i))) i = 0
Tactic:
intros j hj
Proof state after:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j ∈ Finset.Iio i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0
Theorem: repr_gramSchmidt_diagonal
Proof state before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j ∈ Finset.Iio i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0
Tactic:
rw [Finset.mem_Iio] at hj
Proof state after:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j < i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0