OAI/Combinatorics/ContingencyTables/Sampling/PhysicalGraphVertices.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ContingencyTables.SmallGraphProfiles.profilesFintype line 18
2. def OAI.ContingencyTables.SmallGraphProfiles.vertices line 21
3. lemma OAI.ContingencyTables.SmallGraphProfiles.mem_vertices_iff line 24
4. theorem OAI.ContingencyTables.SmallGraphProfiles.context_vertex_mem line 37

   Source documentation

   Every vertex used by the common conditional energy is an actual bounded allowed small-graph profile after the physical coordinate map.

   theorem context_vertex_mem (small : I → J → Bool) (B : I → J → ℕ)
       (s : I×J) (hs : small s.1 s.2=true) (σ : I×J → ℕ) (U : ℕ)
       (hU : 1 ≤ 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 ∈ contextVertices U n)
       (hbox : InBox (bounds (fun _ : Bool => U) (widths (fun _ : Fin n => U))) x) :
       assemble small s hs σ U e x ∈ vertices small B := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.vertices