OAI/Analysis/CircleDomains/Probability/FusionTrajectory.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A probability measure on Baire addresses with a prescribed finite-history transition law. The first coordinate is a dummy; later coordinates choose the successive children.

  1. abbrev OAI.CircleDomainRigidity.FusionTrajectory.History line 19
  2. def OAI.CircleDomainRigidity.FusionTrajectory.history line 21
  3. def OAI.CircleDomainRigidity.FusionTrajectory.branch line 24
  4. theorem OAI.CircleDomainRigidity.FusionTrajectory.history_restrict line 26
  5. def OAI.CircleDomainRigidity.FusionTrajectory.transition line 36
  6. instance OAI.CircleDomainRigidity.FusionTrajectory.(instance at line 40) line 40
  7. def OAI.CircleDomainRigidity.FusionTrajectory.measure line 43
  8. instance OAI.CircleDomainRigidity.FusionTrajectory.(instance at line 46) line 46
  9. theorem OAI.CircleDomainRigidity.FusionTrajectory.measurable_branch line 50
  10. theorem OAI.CircleDomainRigidity.FusionTrajectory.integral_next line 54