OAI/Probability/SKBarriers/Scalar/ScalarTimeChain.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.scalarTimeStep line 15
  2. theorem OAI.SK.Analytic.scalarTimeStep_regular line 18
  3. theorem OAI.SK.Analytic.scalarTimeStep_lipschitz line 22
  4. theorem OAI.SK.Analytic.scalarTimeStep_semigroup line 26
  5. theorem OAI.SK.Analytic.scalarTimeStep_zero line 34
  6. def OAI.SK.Analytic.scalarTimeChain line 37
  7. theorem OAI.SK.Analytic.scalarTimeChain_regular line 41
  8. theorem OAI.SK.Analytic.scalarTimeChain_lipschitz line 47
  9. theorem OAI.SK.Analytic.scalarTimeChain_append line 56
  10. theorem OAI.SK.Analytic.scalarTimeChain_ofFn line 62
  11. theorem OAI.SK.Analytic.scalarTimeChain_split line 72
  12. theorem OAI.SK.Analytic.scalarTimeChain_constant line 79
  13. theorem OAI.SK.Analytic.scalarTimeStep_mass_lipschitz line 88
  14. theorem OAI.SK.Analytic.scalarTimeChain_mass_lipschitz line 100