OAI/Combinatorics/ContingencyTables/Counting/CompanionNearMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionNearMass.cellPositions line 17
2. def OAI.ContingencyTables.CompanionNearMass.nearMass line 22
3. lemma OAI.ContingencyTables.CompanionNearMass.nearMass_eq_fibres line 25
4. theorem OAI.ContingencyTables.CompanionNearMass.near_mass_bound line 42

   Source documentation

   This uses actual feasible endpoint tables, the proved raw marginal signature and equality limit, and the exact count normalizer.

   theorem near_mass_bound (A : Instance I J) (alpha gamma : ℝ) (t : I×J)
       (ht : A.T.Adj (.inl t.1) (.inr t.2)) (ha : 0 ≤ alpha) (hg : 0 < gamma)
       (hW : 20*A.d ≤ A.W) (B K : ℕ)
       (hB : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^B) (hBK : 2*B ≤ K) (hK : 0 < K)
       (Y0 Y1 : I → J → ℤ)
       (hY0 : ∀ i j,0 ≤ Y0 i j ∧ Y0 i j ≤ A.b i j)
       (hY1 : ∀ i j,0 ≤ Y1 i j ∧ Y1 i j ≤ A.b i j)
       (hr0 : ∀ i,(∑ j,Y0 i j)=A.r i) (hc0 : ∀ j,(∑ i,Y0 i j)=A.c j)
       (hr1 : ∀ i,(∑ j,Y1 i j)=A.r i) (hc1 : ∀ j,(∑ i,Y1 i j)=A.c j)
       (hy0 : Y0 t.1 t.2=0) (hy1 : Y1 t.1 t.2=(A.b t.1 t.2:ℤ)) :
       nearMass A alpha t gamma/physicalMass A alpha ≤ 4*gamma*K := by
   …

   Mentions: OAI.ContingencyTables.CompanionNearMass.nearMass