OAI/Combinatorics/ContingencyTables/Sampling/AllSmallOuter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.unitOuterDraw line 23

   Source documentation

   Each trial reads a disjoint word; failed trials use the feasible fallback.

   def unitOuterDraw (fallback : (z : PaperStates r c) → PaperFibre r c z)
       (x : PaperStates r c) (n M : ℕ) (z₀ : Table r c)
       (bits : Fin (M*(n*s)) → Bool) : Table r c :=
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.PaperFibre, OAI.ContingencyTables.Table

2. lemma OAI.ContingencyTables.SmallGraphProfiles.unitOuterDraw_law line 29
3. lemma OAI.ContingencyTables.SmallGraphProfiles.unitOuterDraw_error line 40
4. theorem OAI.ContingencyTables.SmallGraphProfiles.unitOuterDraw_accuracy line 76

   Source documentation

   The all-small branch reaches the same requested error as the branch with a nonempty large rectangle, using no completion-sampling oracle.

   theorem unitOuterDraw_accuracy [Nonempty I] [Nonempty J] [Nonempty (PaperStates r c)]
       [Nonempty (Table r c)] (hsmall : ∀ i j,FirstPaperPhysicalMarginal.paperSmall r c i j=true)
       (htotal : (∑ i,r i)=∑ j,c j) (k : ℕ) (hk : 1 ≤ k)
       (fallback : (z : PaperStates r c) → PaperFibre r c z)
       (x : PaperStates r c) (z₀ : Table r c) :
       (variation (mapLaw (uniformLaw (α := Fin (outerTrials d k*(outerSteps d (smallBinaryLength r c) k*s)) → Bool))
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.Table, OAI.ContingencyTables.FirstPaperPhysicalMarginal.paperSmall, OAI.ContingencyTables.SmallGraphProfiles.PaperFibre, OAI.ContingencyTables.outerTrials, OAI.ContingencyTables.outerSteps, OAI.ContingencyTables.SmallGraphProfiles.smallBinaryLength