OAI/NumberTheory/Ostmann/Construction/FiniteScheduledTemplate.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A finite, concrete variable set for the reverse atom construction

  1. abbrev OAI.Ostmann.ScheduledVariable line 13

    Source documentation

    Actual surviving atoms and a finite supply of labelled pivot positions. Unused pivot positions have no sampling prior.

    abbrev ScheduledVariable {I : Type*} (role : I → CopyScheduleRole) (n : ℕ) :=
…

    Mentions: OAI.Ostmann.CopyScheduleRole

  2. instance OAI.Ostmann.scheduledVariableFintype line 16
  3. def OAI.Ostmann.scheduledPivotAddress line 20
  4. def OAI.Ostmann.finiteScheduledTemplate line 24
  5. def OAI.Ostmann.scheduledPrimeAssignment line 29
  6. theorem OAI.Ostmann.scheduledPivotAddress_ne_actual line 33
  7. theorem OAI.Ostmann.scheduledPivotAddress_level line 38
  8. theorem OAI.Ostmann.scheduledPivotAddress_path line 44
  9. theorem OAI.Ostmann.finiteScheduledTemplate_size line 55
  10. theorem OAI.Ostmann.scheduledVariable_card_le line 60