n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
n : ℕ
h : 0 < ↑n
x : ↑I
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
have h' : (n : ℝ) ≠ 0 := ne_of_gt h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
have h'' := GroupWithZero.mul_right_injective h'
case a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (fun y => y * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) =
    (fun y => y * ↑n) (↑x * (1 - ↑x) / ↑n)
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
apply h''
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (fun y => y * ↑n) ((fun y => y * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x)) =
    (fun y => y * ↑n) ((fun y => y * ↑n) (↑x * (1 - ↑x) / ↑n))
case a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (fun y => y * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) =
    (fun y => y * ↑n) (↑x * (1 - ↑x) / ↑n)
apply h''
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (fun y => y * ↑n) ((fun y => y * ↑n) (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x)) =
    (fun y => y * ↑n) ((fun y => y * ↑n) (↑x * (1 - ↑x) / ↑n))
dsimp
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ (∑ k : Fin (n + 1), (↑x - ↑(k/ₙ)) ^ 2 * ↑(bernstein n ↑k) x) * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
conv_lhs => simp only [Finset.sum_mul, z]
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) / ↑n * ↑n * ↑n
conv_rhs => rw [div_mul_cancel _ h']
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ ν in Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν =
    n • Polynomial.X * (1 - Polynomial.X)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
have := bernsteinPolynomial.variance ℝ n
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ↑(Polynomial.aeval ↑x) (∑ ν in Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) =
    ↑(Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X))
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ ν in Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν =
    n • Polynomial.X * (1 - Polynomial.X)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
apply_fun fun p => Polynomial.aeval (x : ℝ) p at this
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ↑(Polynomial.aeval ↑x) (∑ ν in Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) =
    ↑(Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X))
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
simp [AlgHom.map_sum, Finset.sum_range, ← Polynomial.nat_cast_mul] at this
case h.e'_2
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n =
    ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1)

case h.e'_3
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ↑x * (1 - ↑x) * ↑n = ↑n * ↑x * (1 - ↑x)
case a.a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n
convert this using 1
case h.e'_2.e_f
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ (fun x_1 => (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n) = fun x_1 =>
    (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1)
case h.e'_2
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ∑ x_1 : Fin (n + 1), (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n =
    ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1)
congr 1
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ (↑x - ↑↑k / ↑n) ^ 2 * ↑(bernstein n ↑k) x * ↑n * ↑n =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)
case h.e'_2.e_f
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ (fun x_1 => (↑x - ↑↑x_1 / ↑n) ^ 2 * ↑(bernstein n ↑x_1) x * ↑n * ↑n) = fun x_1 =>
    (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1)
funext k
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x - ↑↑k / ↑n) ^ 2 * ↑(bernstein n ↑k) x =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ (↑x - ↑↑k / ↑n) ^ 2 * ↑(bernstein n ↑k) x * ↑n * ↑n =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)
rw [mul_comm _ (n : ℝ), mul_comm _ (n : ℝ), ← mul_assoc, ← mul_assoc]
case h.e'_2.e_f.h.e_a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x - ↑↑k / ↑n) ^ 2 = (↑n * ↑x - ↑↑k) ^ 2
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x - ↑↑k / ↑n) ^ 2 * ↑(bernstein n ↑k) x =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)
congr 1
case h.e'_2.e_f.h.e_a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x * ↑n - ↑↑k) ^ 2 = (↑n * ↑x - ↑↑k) ^ 2 * ↑n ^ 2
case h.e'_2.e_f.h.e_a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x - ↑↑k / ↑n) ^ 2 = (↑n * ↑x - ↑↑k) ^ 2
field_simp [h]
no goals
case h.e'_2.e_f.h.e_a
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x * ↑n - ↑↑k) ^ 2 = (↑n * ↑x - ↑↑k) ^ 2 * ↑n ^ 2
ring
no goals
case h.e'_3
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
h'' : Function.Injective fun y => y * ↑n
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ↑x * (1 - ↑x) * ↑n = ↑n * ↑x * (1 - ↑x)
ring