OAI/Probability/ParisiFinite/Nnwidth.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Nnwidth.

  1. def OAI.ParisiFinite.nnwidth line 17
  2. lemma OAI.ParisiFinite.coe_nnwidth line 21
  3. lemma OAI.ParisiFinite.nnwidth_append line 26
  4. def OAI.ParisiFinite.scheduleValue line 34
  5. lemma OAI.ParisiFinite.scheduleValue_zero_cons line 38
  6. lemma OAI.ParisiFinite.scheduleValue_cons_shift line 42
  7. lemma OAI.ParisiFinite.scheduleValue_split_shift line 46
  8. lemma OAI.ParisiFinite.scheduleValue_append_left line 59
  9. lemma OAI.ParisiFinite.scheduleValue_append_right line 71
  10. lemma OAI.ParisiFinite.evolve_zero_cons line 79
  11. lemma OAI.ParisiFinite.evolve_of_nnwidth_zero line 84
  12. lemma OAI.ParisiFinite.evolve_le_of_scheduleValue_le line 96
  13. lemma OAI.ParisiFinite.dyadicSchedule_nnwidth line 184
  14. lemma OAI.ParisiFinite.dyadicSchedule_value_bounds line 189
  15. lemma OAI.ParisiFinite.dyadicSchedule_append_value_bounds line 218
  16. lemma OAI.ParisiFinite.dyadicEvolution_high_grid_bound line 237
  17. lemma OAI.ParisiFinite.dyadicEvolution_dyadic_grid_bound line 252
  18. lemma OAI.ParisiFinite.dyadic_tendsto line 261
  19. lemma OAI.ParisiFinite.dyadic_append_tendsto line 270
  20. lemma OAI.ParisiFinite.dyadicEvolution_DPP line 294
  21. lemma OAI.ParisiFinite.field_DPP line 321
  22. lemma OAI.ParisiFinite.recursion_prefix_time_bound line 332
  23. lemma OAI.ParisiFinite.field_time_bound line 352
  24. lemma OAI.ParisiFinite.field_time_abs_bound line 385
  25. lemma OAI.ParisiFinite.field_joint_lipschitz line 399
  26. lemma OAI.ParisiFinite.continuous_field_joint line 422
  27. lemma OAI.ParisiFinite.field_taylor_error line 427
  28. lemma OAI.ParisiFinite.field_slope_error line 441
  29. lemma OAI.ParisiFinite.continuous_fieldGradient_joint line 451
  30. def OAI.ParisiFinite.fieldCurvature line 486
  31. lemma OAI.ParisiFinite.fieldGradient_dyadic_uniform line 489
  32. lemma OAI.ParisiFinite.fieldCurvature_exists line 498
  33. lemma OAI.ParisiFinite.hasDerivAt_fieldGradient line 516
  34. lemma OAI.ParisiFinite.fieldCurvature_lipschitz line 521
  35. lemma OAI.ParisiFinite.fieldCurvature_dyadic_tendsto line 526
  36. lemma OAI.ParisiFinite.fieldCurvature_bounds line 532
  37. lemma OAI.ParisiFinite.fieldCurvature_abs line 547
  38. lemma OAI.ParisiFinite.fieldGradient_slope_error line 554
  39. lemma OAI.ParisiFinite.continuous_fieldCurvature_joint line 564