internlm/Lean-Github huggingface dataset:
Theorem: Vec.le_div_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
⊢ a * c ≤ b → a ≤ b / c
Tactic:
intro h i
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
⊢ a i ≤ (b / c) i
Theorem: Vec.le_div_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
⊢ a i ≤ (b / c) i
Tactic:
have hi := h i
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : (a * c) i ≤ b i
⊢ a i ≤ (b / c) i
Theorem: Vec.le_div_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : (a * c) i ≤ b i
⊢ a i ≤ (b / c) i
Tactic:
simp at hi
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ (b / c) i
Theorem: Vec.le_div_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ (b / c) i
Tactic:
dsimp
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ b i / c i
Theorem: Vec.le_div_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i ≤ b i / c i
Tactic:
rw [_root_.le_div_iff (hc i)]
Proof state after:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i * c i ≤ b i
Theorem: Vec.le_div_iff
Proof state before:
case mpr
m : Type u
n : Type v
inst✝¹ : Fintype m
inst✝ : Fintype n
α : Type w
a b c : m → ℝ
hc : StrongLT 0 c
h : a * c ≤ b
i : m
hi : a i * c i ≤ b i
⊢ a i * c i ≤ b i
Tactic:
exact hi
Proof state after:
no goals
Theorem: HypersonicShapeDesign.aₚ_nonneg
Proof state before:
a b : ℝ
⊢ 0 ≤ aₚ
Tactic:
unfold aₚ
Proof state after:
a b : ℝ
⊢ 0 ≤ 5e-2
Theorem: HypersonicShapeDesign.aₚ_nonneg
Proof state before:
a b : ℝ
⊢ 0 ≤ 5e-2
Tactic:
norm_num
Proof state after:
no goals
Theorem: HypersonicShapeDesign.bₚ_nonneg
Proof state before:
a b : ℝ
⊢ 0 ≤ bₚ
Tactic:
unfold bₚ
Proof state after:
a b : ℝ
⊢ 0 ≤ 0.65
Theorem: HypersonicShapeDesign.bₚ_nonneg
Proof state before:
a b : ℝ
⊢ 0 ≤ 0.65
Tactic:
norm_num
Proof state after:
no goals
Theorem: HypersonicShapeDesign.bₚ_lt_one
Proof state before:
a b : ℝ
⊢ bₚ < 1
Tactic:
unfold bₚ
Proof state after:
a b : ℝ
⊢ 0.65 < 1
Theorem: HypersonicShapeDesign.bₚ_lt_one
Proof state before:
a b : ℝ
⊢ 0.65 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: HypersonicShapeDesign.one_sub_bₚ_nonneg
Proof state before:
a b : ℝ
⊢ 0 ≤ 1 - bₚ
Tactic:
unfold bₚ
Proof state after:
a b : ℝ
⊢ 0 ≤ 1 - 0.65
Theorem: HypersonicShapeDesign.one_sub_bₚ_nonneg
Proof state before:
a b : ℝ
⊢ 0 ≤ 1 - 0.65
Tactic:
norm_num
Proof state after:
no goals
Theorem: leastSquares_alt_objFun
Proof 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
Proof state after:
no goals
Theorem: leastSquares_alt_objFun
Proof 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
Proof 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
Theorem: leastSquares_alt_objFun
Proof 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
Proof 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
Theorem: leastSquares_alt_objFun
Proof 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
Proof state after:
no goals
Theorem: leastSquares_alt_objFun
Proof 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]
Proof 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
Theorem: leastSquares_alt_objFun
Proof 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]
Proof state after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
⊢ (2 * ∑ i : Fin n, a i) * x = 2 * x * ∑ i : Fin n, a i
Theorem: leastSquares_alt_objFun
Proof 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
Proof state after:
no goals
Theorem: leastSquares_alt_objFun
Proof 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]
Proof 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)
Theorem: leastSquares_alt_objFun
Proof 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
Proof 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
Theorem: leastSquares_alt_objFun
Proof 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
Proof state after:
no goals
Theorem: leastSquares_alt_objFun
Proof 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]
Proof 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))
Theorem: leastSquares_alt_objFun
Proof 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
Proof 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
Theorem: leastSquares_alt_objFun
Proof 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
Proof state after:
no goals
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof state after:
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : ∀ (y : ℝ), (x - mean a) ^ 2 ≤ (y - mean a) ^ 2
⊢ x = mean a
Theorem: leastSquares_optimal_eq_mean
Proof 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)
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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 _)
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof state after:
no goals
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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 ⊢
Proof 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
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof state after:
no goals
Theorem: leastSquares_optimal_eq_mean
Proof 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
Proof state after:
no goals
Theorem: leastSquaresVec_optimal_eq_mean
Proof 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
Proof state after:
case h
n : ℕ
hn : 0 < n
a : Fin n → ℝ
x : ℝ
h : (leastSquaresVec a).optimal x
⊢ (leastSquares a).optimal x
Theorem: leastSquaresVec_optimal_eq_mean
Proof 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 ⊢
Proof 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
Theorem: leastSquaresVec_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquaresVec_optimal_eq_mean
Proof 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
Proof 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
Theorem: leastSquaresVec_optimal_eq_mean
Proof 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
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 : (fittingSphereConvex n m x).optimal (c, t)
⊢ (fittingSphereT n m x).optimal (c, t)
Tactic:
simp [fittingSphereT, fittingSphereConvex, optimal, feasible] at h_opt ⊢
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)
⊢ 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)
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)
⊢ 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
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)
⊢ 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)
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)
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
let a := Vec.norm x ^ 2 - 2 * mulVec x c
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
⊢ 0 ≤ t + ‖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
⊢ 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
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
⊢ 0 ≤ t + ‖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
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
have h_t_eq := leastSquaresVec_optimal_eq_mean hm a t h_ls
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
⊢ 0 ≤ t + ‖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
⊢ 0 ≤ t + ‖c‖ ^ 2
Tactic:
have h_c2_eq : ‖c‖ ^ 2 = (1 / m) * ∑ i : Fin m, ‖c‖ ^ 2 := by
  simp [sum_const]
  field_simp
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
⊢ 0 ≤ t + ‖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
⊢ 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
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 ≤ t + ‖c‖ ^ 2