OAI/Combinatorics/ContingencyTables/Transport/FiniteCorrectionLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.FirstSuccess.variation_point_le line 13
2. theorem OAI.ContingencyTables.FirstSuccess.residual_from_variation line 30

   Source documentation

   Total variation at most the square of the rare-branch probability implies the exact pointwise domination required by residual correction.

   theorem residual_from_variation {X : Type*} [Fintype X] [Nonempty X]
       (p : RationalLaw X) (delta : ℚ) (hd : 0 < delta) (hd1 : delta ≤ 1)
       (hcard : (Fintype.card X:ℚ)*delta ≤ 1)
       (herror : variation p (uniformLaw (α := X)) ≤ delta^2) :
   …

   Mentions: OAI.ContingencyTables.FirstSuccess.variation, OAI.ContingencyTables.FirstSuccess.uniformLaw

3. theorem OAI.ContingencyTables.SmallGraphProfiles.initialized_residual_correction line 63

   Source documentation

   The rare correction law for the actual initialized finite experiment. This establishes its exact probability identity; tabulation and execution of this law are separate implementation obligations.

   theorem initialized_residual_correction (htotal : (∑ i,r i)=∑ j,c j)
       (a : GridBoundary.Grid (I := Fin q) (4*d^8))
   …

   Mentions: OAI.ContingencyTables.GridBoundary.Grid