OAI/Probability/DilutedSpin/UniversalDictionary.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DilutedSpinGlass.UniversalDictionary.Table line 14
  2. abbrev OAI.DilutedSpinGlass.UniversalDictionary.Spec line 17

    Source documentation

    Two bounded mark tables and the choice of spin or marker anchor.

    abbrev Spec (L : ℕ) := Σ r : ℕ, Table L r × Table L r × Bool

    Mentions: OAI.DilutedSpinGlass.UniversalDictionary.Table

  3. instance OAI.DilutedSpinGlass.UniversalDictionary.tableCountable line 19
  4. instance OAI.DilutedSpinGlass.UniversalDictionary.specCountable line 20
  5. instance OAI.DilutedSpinGlass.UniversalDictionary.tableNonempty line 21
  6. instance OAI.DilutedSpinGlass.UniversalDictionary.specNonempty line 22
  7. instance OAI.DilutedSpinGlass.UniversalDictionary.specMeasurable line 24
  8. instance OAI.DilutedSpinGlass.UniversalDictionary.specSingleton line 25
  9. instance OAI.DilutedSpinGlass.UniversalDictionary.specDecidable line 26
  10. abbrev OAI.DilutedSpinGlass.UniversalDictionary.Alphabet line 28
  11. def OAI.DilutedSpinGlass.UniversalDictionary.prior line 29
  12. def OAI.DilutedSpinGlass.UniversalDictionary.interior line 32
  13. def OAI.DilutedSpinGlass.UniversalDictionary.direction line 35
  14. def OAI.DilutedSpinGlass.UniversalDictionary.anchor line 38
  15. lemma OAI.DilutedSpinGlass.UniversalDictionary.table_bound line 42
  16. lemma OAI.DilutedSpinGlass.UniversalDictionary.direction_bound line 44
  17. lemma OAI.DilutedSpinGlass.UniversalDictionary.anchor_bound line 50
  18. def OAI.DilutedSpinGlass.UniversalDictionary.weights line 60

    Source documentation

    One fixed countable full-support law suffices for all finitely many colors/requirements and their signed rational polarizations.

    noncomputable def weights (L : ℕ) : Measure (Spec L × ℕ) :=
…

    Mentions: OAI.DilutedSpinGlass.UniversalDictionary.Spec

  19. instance OAI.DilutedSpinGlass.UniversalDictionary.weightsProbability line 62
  20. lemma OAI.DilutedSpinGlass.UniversalDictionary.weights_pos line 64
  21. def OAI.DilutedSpinGlass.UniversalDictionary.signQ line 68
  22. lemma OAI.DilutedSpinGlass.UniversalDictionary.abs_signQ line 69
  23. lemma OAI.DilutedSpinGlass.UniversalDictionary.cast_signQ line 70
  24. def OAI.DilutedSpinGlass.UniversalDictionary.selector line 73
  25. lemma OAI.DilutedSpinGlass.UniversalDictionary.selector_eq_pathColor line 87
  26. def OAI.DilutedSpinGlass.UniversalDictionary.average line 99

    Source documentation

    Signed averages needed by polarization stay in the SAME finite alphabet and in the unit-bounded rational table family.

    noncomputable def average {L r k : ℕ} (hk : 0 < k) (ε : Fin k → Bool)
    (g : Fin k → Table L r) : Table L r :=
…

    Mentions: OAI.DilutedSpinGlass.UniversalDictionary.Table