OAI/Combinatorics/ContingencyTables/Transport/CompletionEnergyComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.CompletionTranslation.completionChain_energy_lower line 16

   Source documentation

   This is the actual chain energy comparison. The half-acceptance premise is supplied by the proved reference-star small-entry estimate.

   theorem completionChain_energy_lower
       (R : X → Option I → ℕ) (P : X → Option J → ℕ)
       (htotal : ∀ x,(∑ i,R x i)=∑ j,P x j)
       (Adj : X → X → Prop) (hsym : ∀ x y,Adj x y ↔ Adj y x)
       (β : ℝ) (hβ : 0 ≤ β) (D : ℕ)
       (hdegree : ∀ x,(Finset.univ.filter (Adj x)).card ≤ D)
       (hproposal : (D:ℝ)*β ≤ 1/2)
       (haccept : ∀ x y,Adj x y → (blockCount R P x:ℝ)/2 ≤ acceptedCount R P x y)
       (H : X → ℝ) :
       β/(2*MetropolisChain.normalizer (fun z => (blockCount R P z:ℝ)))*
         ((∑ x,∑ y,if Adj x y then min (blockCount R P x:ℝ) (blockCount R P y:ℝ)*
           (H x-H y)^2 else 0)/2) ≤
   …

   Mentions: OAI.ContingencyTables.CompletionTranslation.blockCount, OAI.ContingencyTables.CompletionTranslation.acceptedCount, OAI.ContingencyTables.MetropolisChain.normalizer