theorem
proved
uniform_sqNorm_one
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cost.Ndim.Calibration on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
47 exact ⟨a, ha, ha_val⟩
48
49/-- Under uniform weights, unit squared norm gives `a² = 1/n` (for `n > 0`). -/
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
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