OAI/Combinatorics/ContingencyTables/Sampling/PhysicalPrefixEnergies.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.prefixExtension line 18
2. lemma OAI.ContingencyTables.SmallGraphProfiles.prefixExtension_at line 23
3. lemma OAI.ContingencyTables.SmallGraphProfiles.prefixExtension_bounded line 31
4. def OAI.ContingencyTables.SmallGraphProfiles.prefixValues line 37
5. lemma OAI.ContingencyTables.SmallGraphProfiles.physicalPrefix_iff_values line 42
6. def OAI.ContingencyTables.SmallGraphProfiles.physicalEdges line 59
7. def OAI.ContingencyTables.SmallGraphProfiles.physicalEnergy line 63
8. lemma OAI.ContingencyTables.SmallGraphProfiles.physicalContextEdges_eq_filter line 67
9. lemma OAI.ContingencyTables.SmallGraphProfiles.sum_physicalContextEdgeTerms_le line 93
10. theorem OAI.ContingencyTables.SmallGraphProfiles.sum_physicalContextEnergy_le line 112

    Source documentation

    At a fixed exposed cell, prefix contexts partition eligible physical edges. Nonnegative exchange energy is therefore counted at most once.

    theorem sum_physicalContextEnergy_le (small : I → J → Bool) (B : I → J → ℕ)
        (s : I×J) (U : ℕ) (hB : ∀ i j,small i j=true → B i j=U)
        (f H : SmallProfile small → ℝ) (hf : ∀ z,0 ≤ f z) :
        (∑ τ : Earlier small s → Fin (U+1),
          physicalContextEnergy small B s (prefixExtension small s U τ) f H) ≤
          physicalEnergy small B f H := by
    …

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.physicalContextEnergy, OAI.ContingencyTables.SmallGraphProfiles.prefixExtension, OAI.ContingencyTables.SmallGraphProfiles.physicalEnergy