OAI/Combinatorics/ContingencyTables/Dense/DenseExponentArithmetic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Natural arithmetic for the dense acceptance exponent

Each integral completion entry is represented by a difference of two natural numbers. The rational floor in the geometric definition is then an ordinary natural quotient, including zero denominators.

  1. def OAI.ContingencyTables.GridBoundary.componentExponent line 15
  2. lemma OAI.ContingencyTables.GridBoundary.floor_signed_quotient line 18
  3. lemma OAI.ContingencyTables.GridBoundary.componentExponent_eq line 23
  4. def OAI.ContingencyTables.GridBoundary.integerParts line 48
  5. lemma OAI.ContingencyTables.GridBoundary.integerParts_sub line 55
  6. lemma OAI.ContingencyTables.GridBoundary.integerParts_sub_rat line 64
  7. def OAI.ContingencyTables.GridBoundary.arithmeticExponentAt line 72
  8. lemma OAI.ContingencyTables.GridBoundary.arithmeticExponentAt_eq line 80
  9. theorem OAI.ContingencyTables.GridBoundary.denseExponent_eq_arithmetic line 93

    Source documentation

    A finite maximum of explicitly computable natural quotients is exactly the exponent used in the dense Metropolis acceptance probability.

    theorem denseExponent_eq_arithmetic (R : Option I → ℕ) (P : Option J → ℕ) (d : ℕ)
    (e : I×J ≃ Fin q) (a : Grid (I := Fin q) K) :
…

    Mentions: OAI.ContingencyTables.GridBoundary.Grid