OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperPhysicalVariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Poincare inequality on the actual feasible small states

  1. abbrev OAI.ContingencyTables.SmallGraphProfiles.PhysicalStates line 18
  2. instance OAI.ContingencyTables.SmallGraphProfiles.physicalStatesFintype line 22
  3. def OAI.ContingencyTables.SmallGraphProfiles.physicalProfile line 27
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.physicalProfile_injective line 31
  5. def OAI.ContingencyTables.SmallGraphProfiles.physicalExtension line 39
  6. lemma OAI.ContingencyTables.SmallGraphProfiles.physicalExtension_at line 43
  7. theorem OAI.ContingencyTables.SmallGraphProfiles.firstPaper_physical_variance line 52

    Source documentation

    Zero-weight bounded profiles can be removed before applying the full graph estimate, so this quantifies over every observable on the actual positive-weight state space.

    theorem firstPaper_physical_variance (r : I → ℕ) (c : J → ℕ) :
    let d := dimensionAllowance (I := I) (J := J)
…