pith. machine review for the scientific record. sign in
theorem proved term proof

sqNorm_uniform

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  27theorem sqNorm_uniform {n : ℕ} {α : Vec n}
  28    (hU : UniformWeights α) :
  29    ∃ a : ℝ, sqNorm α = (n : ℝ) * a ^ 2 := by

proof body

Term-mode proof.

  30  rcases hU with ⟨a, ha⟩
  31  refine ⟨a, ?_⟩
  32  unfold sqNorm dot
  33  simp [ha, pow_two, Finset.card_univ]
  34
  35/-- If weights are uniform and sum to one, each weight is `1/n` (for `n > 0`). -/

depends on (15)

Lean names referenced from this declaration's body.