OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperSmallChain.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The literal first-paper completion chain has the stated Poincare bound

  1. abbrev OAI.ContingencyTables.SmallGraphProfiles.stateCapacity line 21
  2. abbrev OAI.ContingencyTables.SmallGraphProfiles.PaperStates line 25
  3. instance OAI.ContingencyTables.SmallGraphProfiles.paperStatesFintype line 31

    Source documentation

    Keep one public enumeration instance for the paper's state type, so rational laws and generic finite kernels share the same index.

    noncomputable instance paperStatesFintype (r : I → ℕ) (c : J → ℕ) :
    Fintype (PaperStates r c) :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates

  4. lemma OAI.ContingencyTables.SmallGraphProfiles.stateCapacity_small line 37
  5. def OAI.ContingencyTables.SmallGraphProfiles.paperSmallChain line 42
  6. def OAI.ContingencyTables.SmallGraphProfiles.stateWeight line 59
  7. def OAI.ContingencyTables.SmallGraphProfiles.stateGraphEnergy line 64
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.stateWeight_positive line 69
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.paperSmallChain_pi line 72
  10. lemma OAI.ContingencyTables.SmallGraphProfiles.paperSmallChain_energy_lower line 83
  11. theorem OAI.ContingencyTables.SmallGraphProfiles.paperSmallChain_poincare line 117

    Source documentation

    Every observable on the actual positive completion states satisfies the source's d^160 bound, with the actual dyadic proposal probability.

    theorem paperSmallChain_poincare (r : I → ℕ) (c : J → ℕ) [Nonempty (PaperStates r c)]
    (i₀ : LargeRows r ((dimensionAllowance (I := I) (J := J))^20))
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.LargeRows