uniform_weight_of_sum_one

formal source

  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`). -/
  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
  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`). -/
  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