OAI/Combinatorics/ContingencyTables/Transport/ContextChildVariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.ExcessContextProfiles.graphEnergy_mono line 18
2. def OAI.ContingencyTables.ExcessContextProfiles.contextVertices line 32
3. lemma OAI.ContingencyTables.ExcessContextProfiles.leafVertices_subset_context line 36
4. theorem OAI.ContingencyTables.ExcessContextProfiles.physical_child_variance line 45

   Source documentation

   The physical conditional masses and means satisfy the paper's between-child estimate, allowing arbitrary zero-mass children.

   theorem physical_child_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 : (Coordinates Bool (widths (fun _ : Fin n => U)) → ℕ) → ℝ)
       (hZ : 0 < ∑ j : Fin (U+1), eliminate (widths (fun _ : Fin n => U))
         (contextHard small B r c L _ (contextEquiv small s hs e U) (prefixRaw small s σ U))
   …

   Mentions: OAI.ContingencyTables.ResidualTables