OAI/Combinatorics/ContingencyTables/Transport/ContextGraphMembership.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.SmallGraphProfiles.pair_total_removeOne line 17
2. lemma OAI.ContingencyTables.SmallGraphProfiles.balanced_of_pair_totals line 30
3. lemma OAI.ContingencyTables.SmallGraphProfiles.pattern_after_one_removal line 40
4. lemma OAI.ContingencyTables.SmallGraphProfiles.assemble_bounded line 81
5. lemma OAI.ContingencyTables.SmallGraphProfiles.base_pair_total line 99
6. theorem OAI.ContingencyTables.SmallGraphProfiles.leaf_pattern line 141

   Source documentation

   Every box-valid transport leaf has exactly an allowed physical small-graph pattern. No multi-defect vertex enters the local energy.

   theorem leaf_pattern (small : I → J → Bool) (B : I → J → ℕ)
       (s : I×J) (hs : small s.1 s.2=true) (σ : I×J → ℕ) (U l : ℕ)
       (hU : 1 ≤ U) (hlU : l ≤ U) (hB : ∀ i j, small i j=true → B i j=U)
       (hσ : ∀ a : Earlier small s, σ a.val.val ≤ U) {n : ℕ} (e : Fin n ≃ Later small s)
       (x : Coordinates Bool (widths (fun _ : Fin n => U)) → ℕ)
       (hx : x ∈ leafVertices _ (rootDisplay U l))
       (hbox : InBox (bounds (fun _ : Bool => U) (widths (fun _ : Fin n => U))) x) :
       Pattern small B (assemble small s hs σ U e x) := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.Pattern