OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseTrialLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionPhaseTrialProgram.data line 20
2. lemma OAI.ContingencyTables.CompanionPhaseTrialProgram.output_data line 29
3. theorem OAI.ContingencyTables.CompanionPhaseTrialProgram.sameLaw line 47

   Source documentation

   Before changing multiplier representation, this law uses the canonical matrix's source weights for the trajectory and the given stored value for the update.

   theorem sameLaw (A : Instance (Fin m) (Fin n)) (C K j k N : ℕ)
       (hC : 0<C) (hj : j+1 ≤ rationalHeight A C) (hK : 1≤K)
       (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
       (xi : ℚ) (hxi : 0<xi) (z : View A→ℕ)
       (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
   …

   Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount

4. theorem OAI.ContingencyTables.CompanionPhaseTrialProgram.trial_sameLaw line 108