theorem
proved
tactic proof
uniform_sqNorm_one
show as:
view Lean formalization →
formal statement (Lean)
50theorem uniform_sqNorm_one {n : ℕ} {α : Vec n}
51 (hn : 0 < n) (hU : UniformWeights α) (hcurv : sqNorm α = 1) :
52 ∃ a : ℝ, (∀ i : Fin n, α i = a) ∧ a ^ 2 = 1 / (n : ℝ) := by
proof body
Tactic-mode proof.
53 rcases hU with ⟨a, ha⟩
54 have hna : (n : ℝ) ≠ 0 := by
55 exact_mod_cast (Nat.ne_of_gt hn)
56 have hnorm : (n : ℝ) * a ^ 2 = 1 := by
57 simpa [sqNorm, dot, ha, pow_two, Finset.card_univ] using hcurv
58 have hsquare : a ^ 2 = 1 / (n : ℝ) := by
59 apply (eq_div_iff hna).2
60 linarith [hnorm]
61 exact ⟨a, ha, hsquare⟩
62
63end Ndim
64end Cost
65end IndisputableMonolith