IndisputableMonolith.Cost.Ndim.Calibration

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Calibration relations for uniform weights
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Cost
   9namespace Ndim
  10
  11open scoped BigOperators
  12
  13def weightSum {n : ℕ} (α : Vec n) : ℝ := ∑ i : Fin n, α i
  14
  15def sqNorm {n : ℕ} (α : Vec n) : ℝ := dot α α
  16
  17def UniformWeights {n : ℕ} (α : Vec n) : Prop := ∃ a : ℝ, ∀ i : Fin n, α i = a
  18
  19theorem weightSum_uniform {n : ℕ} {α : Vec n}
  20    (hU : UniformWeights α) :
  21    ∃ a : ℝ, weightSum α = (n : ℝ) * a := by
  22  rcases hU with ⟨a, ha⟩
  23  refine ⟨a, ?_⟩
  24  unfold weightSum
  25  simp [ha, Finset.card_univ]
  26
  27theorem sqNorm_uniform {n : ℕ} {α : Vec n}
  28    (hU : UniformWeights α) :
  29    ∃ a : ℝ, sqNorm α = (n : ℝ) * a ^ 2 := by
  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`). -/
  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
  66