theorem
proved
tactic proof
uniform_weight_of_sum_one
show as:
view Lean formalization →
formal statement (Lean)
36theorem uniform_weight_of_sum_one {n : ℕ} {α : Vec n}
37 (hn : 0 < n) (hU : UniformWeights α) (hsum : weightSum α = 1) :
38 ∃ a : ℝ, (∀ i : Fin n, α i = a) ∧ a = 1 / (n : ℝ) := by
proof body
Tactic-mode proof.
39 rcases hU with ⟨a, ha⟩
40 have hna : (n : ℝ) ≠ 0 := by
41 exact_mod_cast (Nat.ne_of_gt hn)
42 have hsum' : (n : ℝ) * a = 1 := by
43 simpa [weightSum, ha, Finset.card_univ] using hsum
44 have ha_val : a = 1 / (n : ℝ) := by
45 apply (eq_div_iff hna).2
46 linarith [hsum']
47 exact ⟨a, ha, ha_val⟩
48
49/-- Under uniform weights, unit squared norm gives `a² = 1/n` (for `n > 0`). -/