OAI/Combinatorics/ContingencyTables/Sampling/PhysicalContextVariance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.SmallGraphProfiles.physicalContextEnergy_nonnegative line 20
2. theorem OAI.ContingencyTables.SmallGraphProfiles.physical_context_variance line 29

   Source documentation

   No positivity assumption is needed on the whole context. Its child variance is bounded by its actual physical prefix exchange energy.

   theorem physical_context_variance (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 : 2 ≤ U) (hB : ∀ i j,small i j=true → B i j=U)
       (hlarge : ∀ i j,small i j=false → 2 ≤ B i j)
       (hσ : ∀ a : Earlier small s,σ a.val.val ≤ U) {n : ℕ} (e : Fin n ≃ Later small s)
       (hcap : ∀ T : ResidualTables small r c (fun i => r i+rowLargeCount small i*L)
         (fun j => c j+columnLargeCount small j*L),∀ i j,T.val.val i j ≤ B i j)
       (H : SmallProfile small → ℝ) :
       let Ms := widths (fun _ : Fin n => U)
   …

   Mentions: OAI.ContingencyTables.ResidualTables