IndisputableMonolith.Cost.Ndim.Symmetry

   1import IndisputableMonolith.Cost.Ndim.Calibration
   2
   3/-!
   4# Permutation symmetry of coefficient weights
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Cost
   9namespace Ndim
  10
  11/-- Coefficients are invariant under permutations of indices. -/
  12def CoeffPermutationInvariant {n : ℕ} (α : Vec n) : Prop :=
  13  ∀ σ : Equiv.Perm (Fin n), ∀ i : Fin n, α (σ i) = α i
  14
  15theorem coeff_perm_invariant_of_uniform {n : ℕ} {α : Vec n}
  16    (hU : UniformWeights α) :
  17    CoeffPermutationInvariant α := by
  18  rcases hU with ⟨a, ha⟩
  19  intro σ i
  20  simp [ha]
  21
  22theorem uniform_of_coeff_perm_invariant {n : ℕ} (hn : 0 < n) {α : Vec n}
  23    (hperm : CoeffPermutationInvariant α) :
  24    UniformWeights α := by
  25  let i0 : Fin n := ⟨0, hn⟩
  26  refine ⟨α i0, ?_⟩
  27  intro i
  28  have h := hperm (Equiv.swap i0 i) i0
  29  simpa using h
  30
  31end Ndim
  32end Cost
  33end IndisputableMonolith
  34