OAI/Combinatorics/EditApproximation/Probability/AdaptiveSeedLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Fresh streams indexed by every possible incoming seed make adaptive seed-dependent draw types compatible with a single finite product law.

  1. theorem OAI.EditApproximation.finite_integral_test line 12
  2. def OAI.EditApproximation.adaptiveSeedStep line 29

    Source documentation

    Only the coordinate belonging to the actual incoming table is consumed. All states within that coordinate retain their shared copy streams.

    def adaptiveSeedStep (next : ∀ seed, Draw seed → Seed) (pair : Seed × (∀ seed, Draw seed)) : Seed :=
…
  3. def OAI.EditApproximation.adaptiveSeedLaw line 32
  4. instance OAI.EditApproximation.adaptiveSeedLaw_probability line 35
  5. theorem OAI.EditApproximation.adaptiveSeedLaw_failure line 40
  6. def OAI.EditApproximation.adaptiveSeedSequence line 88
  7. instance OAI.EditApproximation.adaptiveSeedSequence_probability line 92
  8. theorem OAI.EditApproximation.adaptiveSeedSequence_failure line 101