CompletionChainFlow.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact edge flow of the completion-translation chain

lemma OAI.ContingencyTables.CompletionTranslation.completionMove_flow line 15

theorem OAI.ContingencyTables.CompletionTranslation.completionChain_energy line 30

Source documentation

The flow formula includes the holding terms: those contribute zero energy. The numerator counts literal acceptable completion translations.

theorem completionChain_energy (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) (H : X → ℝ) :
    (completionChain R P htotal Adj hsym β hβ D hdegree hproposal).energy H=
      (∑ x,∑ y,if Adj x y then
        β*(acceptedCount R P x y:ℝ)*(H x-H y)^2 else 0)/
          (2*MetropolisChain.normalizer (fun z => (blockCount R P z:ℝ))) := by
…

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

lemma OAI.ContingencyTables.CompletionTranslation.completionMove_lower line 55
Source documentation
A half-acceptance estimate yields the min-weight comparison on every actual edge, with no request for completion-count evaluation.
```
lemma completionMove_lower (R : X → Option I → ℕ) (P : X → Option J → ℕ)
    (htotal : ∀ x,(∑ i,R x i)=∑ j,P x j)
    (Adj : X → X → Prop) (β : ℝ) (hβ : 0 ≤ β) (x y : X)
    (hxy : Adj x y)
    (haccept : (blockCount R P x:ℝ)/2 ≤ acceptedCount R P x y) :
    β/2*min 1 ((blockCount R P y:ℝ)/blockCount R P x) ≤ completionMove R P Adj β x y := by
…
```
Mentions: OAI.ContingencyTables.CompletionTranslation.blockCount, OAI.ContingencyTables.CompletionTranslation.acceptedCount, OAI.ContingencyTables.CompletionTranslation.completionMove