OAI/Combinatorics/ContingencyTables/Transport/IntegerResidualCorrection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.IntegerResidualCorrection.count line 14
2. lemma OAI.ContingencyTables.IntegerResidualCorrection.cast_count line 17
3. def OAI.ContingencyTables.IntegerResidualCorrection.law line 28

   Source documentation

   The finite integer weights sum to |A|*Q; all truncations are exact because the ordinary law is pointwise dominated by the uniform law.

   def law (p : IntegerLaw A Q) (T : ℕ) (hQ : 0<Q) (hT : 0<T)
       (hdom : ∀ x,(1-1/(T:ℚ))*(p.toRational hQ).mass x≤uniformMass (α := A)) :
   …

   Mentions: OAI.ContingencyTables.IntegerLaw

4. lemma OAI.ContingencyTables.IntegerResidualCorrection.denominator_pos line 42
5. lemma OAI.ContingencyTables.IntegerResidualCorrection.law_mass line 45
6. theorem OAI.ContingencyTables.IntegerResidualCorrection.mixture_exact line 58

   Source documentation

   The ordinary branch and the explicit integer-weight branch have exactly uniform combined mass, before physical execution is compiled.

   theorem mixture_exact (p : IntegerLaw A Q) (T : ℕ) (hQ : 0<Q) (hT : 0<T)
       (hdom : ∀ x,(1-1/(T:ℚ))*(p.toRational hQ).mass x≤uniformMass (α := A)) (a : A) :
   …

   Mentions: OAI.ContingencyTables.IntegerLaw