OAI/Probability/ParisiFinite/Splice.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Splice.

  1. def OAI.ParisiPath.TimeQuadraticTest.splice line 23
  2. lemma OAI.ParisiPath.TimeQuadraticTest.integrable_dt line 25
  3. lemma OAI.ParisiPath.TimeQuadraticTest.measurable_splice line 31
  4. lemma OAI.ParisiPath.TimeQuadraticTest.bound_splice line 36
  5. lemma OAI.ParisiPath.TimeQuadraticTest.integrable_splice_dt line 44
  6. lemma OAI.ParisiPath.TimeQuadraticTest.continuousAt_splice line 51
  7. lemma OAI.ParisiPath.TimeQuadraticTest.splice_integralT line 62
  8. def OAI.ParisiPath.TimeQuadraticTest.glue line 108
  9. def OAI.ParisiFinite.SmoothField.staticTimeTest line 148
  10. def OAI.ParisiFinite.SmoothField.slabTimeTest line 169
  11. def OAI.ParisiFinite.finiteTimeField line 191
  12. def OAI.ParisiFinite.finiteTimeDerivative line 197
  13. def OAI.ParisiFinite.finiteTimeCoefficient line 203
  14. lemma OAI.ParisiFinite.finiteTimeField_start line 207
  15. lemma OAI.ParisiFinite.finiteTimeField_after line 222
  16. lemma OAI.ParisiFinite.finiteTimeField_curvature line 233
  17. lemma OAI.ParisiFinite.finiteTimeField_PDE line 245
  18. structure OAI.ParisiFinite.ScheduleTimeRealization line 264
  19. def OAI.ParisiFinite.scheduleTimeRealization line 273
  20. lemma OAI.ParisiFinite.finiteTimeCoefficient_measurable line 319
  21. lemma OAI.ParisiFinite.finiteTimeCoefficient_bound line 327
  22. lemma OAI.ParisiFinite.finiteTimeField_measurable_d1 line 338
  23. def OAI.ParisiFinite.scheduleSuffix line 366
  24. lemma OAI.ParisiFinite.scheduleSuffix_coeff_bound line 370
  25. lemma OAI.ParisiFinite.nnwidth_scheduleSuffix line 383
  26. lemma OAI.ParisiFinite.scheduleValue_suffix line 399
  27. lemma OAI.ParisiFinite.scheduleSuffix_add line 411
  28. lemma OAI.ParisiFinite.evolve_scheduleSuffix_zero line 431
  29. lemma OAI.ParisiFinite.scheduleSuffix_append line 441
  30. lemma OAI.ParisiFinite.finiteTimeField_suffix_val line 452
  31. lemma OAI.ParisiFinite.recursion_suffix_time_bound line 474
  32. lemma OAI.ParisiFinite.shifted_schedule_suffix_error line 506
  33. lemma OAI.ParisiFinite.dyadic_suffix_grid_error line 558
  34. lemma OAI.ParisiFinite.dyadic_suffix_value_bounds line 577
  35. lemma OAI.ParisiFinite.dyadic_suffix_value_error line 608