DenseCanonicalSemantics.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Correctness of dense sampling with computed initialization

def OAI.ContingencyTables.DensePrograms.canonicalOrigin line 13
lemma OAI.ContingencyTables.DensePrograms.zeroGrid_code line 21
def OAI.ContingencyTables.DensePrograms.canonicalFallback line 31
lemma OAI.ContingencyTables.DensePrograms.canonicalFallback_output line 39
lemma OAI.ContingencyTables.DensePrograms.canonicalInput_code line 52
theorem OAI.ContingencyTables.DensePrograms.canonicalDenseDraw_eq line 61
Source documentation
No caller-supplied grid or feasible fallback is needed by the binary dense program. Every output is the analyzed table-valued draw.
```
theorem canonicalDenseDraw_eq {m n d : ℕ}
    (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
    (htotal : (∑ i,R i)=∑ j,P j) (h : ℕ)
    (bits : Fin (normalizedDrawBits R P d h) → Bool) :
    canonicalDenseDraw (((marginCode R,marginCode P),(d,h)),List.ofFn bits)=
      tableOutput (normalizedBooleanDraw R P hd hR hP htotal h
        (canonicalOrigin (m*n) d (by omega)) (canonicalFallback R P htotal) bits) := by
…
```
Mentions: OAI.ContingencyTables.DensePrograms.normalizedDrawBits, OAI.ContingencyTables.DensePrograms.canonicalDenseDraw, OAI.ContingencyTables.DensePrograms.marginCode, OAI.ContingencyTables.DensePrograms.tableOutput, OAI.ContingencyTables.DensePrograms.normalizedBooleanDraw, OAI.ContingencyTables.DensePrograms.canonicalOrigin, OAI.ContingencyTables.DensePrograms.canonicalFallback

theorem OAI.ContingencyTables.DensePrograms.canonicalDenseDraw_variation line 75

Source documentation

The initialized dense call retains the stated error for every margin ordering and uses only the published analytic inputs.

theorem canonicalDenseDraw_variation {m n d : ℕ}
    (R : Option (Fin m) → ℕ) (P : Option (Fin n) → ℕ)
    (hd : 14≤d) (hR : ∀ i,d^12≤R i) (hP : ∀ j,d^12≤P j)
    (hdimR : Fintype.card (Option (Fin m))≤d) (hdimP : Fintype.card (Option (Fin n))≤d)
    (hfree : Fintype.card (Fin m×Fin n)≤d) (htotal : (∑ i,R i)=∑ j,P j)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (m*n))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (m*n)) (4*d^8))) (h : ℕ) :
…

Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger