OAI/Combinatorics/ContingencyTables/Transport/ContextGraphEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.PhysicalPrefix line 19
2. lemma OAI.ContingencyTables.SmallGraphProfiles.assemble_physicalPrefix line 24
3. def OAI.ContingencyTables.SmallGraphProfiles.physicalContextEdges line 31
4. def OAI.ContingencyTables.SmallGraphProfiles.physicalContextEnergy line 36
5. lemma OAI.ContingencyTables.SmallGraphProfiles.hardMarginal_nonnegative line 41
6. theorem OAI.ContingencyTables.SmallGraphProfiles.context_graphEnergy_le line 51

   Source documentation

   The actual conditional variance energy uses physical allowed states and ordinary exchange edges in its fixed row-major prefix only.

   theorem context_graphEnergy_le (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L : ℕ)
       (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)
       (H : SmallProfile small → ℝ) :
       let Ms := widths (fun _ : Fin n => U)
   …