OAI/Combinatorics/ContingencyTables/Sampling/PhysicalSmallEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.SmallGraphProfiles.fullEdges_vertices line 18
2. lemma OAI.ContingencyTables.SmallGraphProfiles.positive_vertex_is_physical line 38
3. theorem OAI.ContingencyTables.SmallGraphProfiles.fullEnergy_physical_eq line 49

   Source documentation

   Deleting zero-weight vertices preserves the exact unnormalized energy, not merely an inequality for a restricted class of observables.

   theorem fullEnergy_physical_eq (r : I → ℕ) (c : J → ℕ) (U L : ℕ) (B : I → J → ℕ)
       (hB : ∀ i j,firstPaperSmall r c U i j=true → B i j=U)
       (H : PhysicalStates (firstPaperSmall r c U) B r c L → ℝ) :
       fullEnergy r c U L B hB (physicalExtension _ B r c L H)=
         (∑ x,∑ y,if physicalAdjacent r c U L B hB x y then
           min (hardMarginal (firstPaperSmall r c U) B r c L (physicalProfile _ B r c L x))
             (hardMarginal (firstPaperSmall r c U) B r c L (physicalProfile _ B r c L y))*
             (H x-H y)^2 else 0)/2 := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PhysicalStates, OAI.ContingencyTables.SmallGraphProfiles.fullEnergy, OAI.ContingencyTables.SmallGraphProfiles.physicalExtension, OAI.ContingencyTables.SmallGraphProfiles.physicalAdjacent, OAI.ContingencyTables.SmallGraphProfiles.physicalProfile