OAI/Probability/ParisiFinite/GlobalDyadicFieldError.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Global Dyadic Field Error.

  1. lemma OAI.ParisiFinite.global_dyadic_field_error line 16
  2. lemma OAI.ParisiFinite.global_dyadic_field_tendstoUniformly line 24
  3. lemma OAI.ParisiFinite.global_dyadic_gradient_tendstoUniformly line 36
  4. lemma OAI.ParisiFinite.finiteTimeCoefficient_scheduleValue line 46
  5. lemma OAI.ParisiFinite.dyadicSchedule_low_sample line 61
  6. lemma OAI.ParisiFinite.dyadicSchedule_low_value_tendsto line 87
  7. lemma OAI.ParisiFinite.dyadicSchedule_low_value_coe_tendsto line 102
  8. lemma OAI.ParisiFinite.global_dyadic_coefficient_tendsto_ae line 114
  9. lemma OAI.ParisiFinite.ThirdJet.continuous_transformD3_joint line 148
  10. def OAI.ParisiFinite.ThirdJet.slabD3 line 159
  11. lemma OAI.ParisiFinite.ThirdJet.continuous_slabD3 line 162
  12. lemma OAI.ParisiFinite.ThirdJet.slabD3_bound line 167
  13. def OAI.ParisiFinite.ThirdJet.gradientDt line 171
  14. def OAI.ParisiFinite.ThirdJet.gradientTimeBound line 175
  15. lemma OAI.ParisiFinite.ThirdJet.gradientDt_bound line 178
  16. lemma OAI.ParisiFinite.ThirdJet.measurable_gradientDt line 193
  17. lemma OAI.ParisiFinite.ThirdJet.continuous_gradientDt line 201
  18. lemma OAI.ParisiFinite.ThirdJet.hasDerivAt_fieldOnInterval_dt line 210
  19. lemma OAI.ParisiFinite.ThirdJet.gradient_integral_time line 219
  20. def OAI.ParisiFinite.ThirdJet.slabGradientTest line 241
  21. lemma OAI.ParisiFinite.ThirdJet.intervalIntegrable_gradientDt line 278
  22. lemma OAI.ParisiFinite.ThirdJet.gradientDt_rightContinuous line 284
  23. lemma OAI.ParisiFinite.ThirdJet.hasDerivWithinAt_gradient_time line 300
  24. lemma OAI.ParisiFinite.ThirdJet.gradient_square_integral_time line 315
  25. def OAI.ParisiFinite.ThirdJet.squareGradientField line 336
  26. def OAI.ParisiFinite.ThirdJet.slabSquareGradientTest line 359
  27. lemma OAI.ParisiFinite.SmoothField.d1_eq_of_val_eq line 410
  28. structure OAI.ParisiFinite.ScheduleGradientSquare line 414
  29. def OAI.ParisiFinite.scheduleGradientSquare line 425
  30. lemma OAI.ParisiFinite.finiteTimeField_d1_start line 473
  31. lemma OAI.ParisiFinite.finiteTimeField_d1_after line 478
  32. lemma OAI.ParisiFinite.scheduleSuffix_ordered line 494
  33. lemma OAI.ParisiFinite.SmoothField.d2_eq_of_val_eq line 505
  34. lemma OAI.ParisiFinite.finiteTimeField_suffix_d2 line 510
  35. lemma OAI.ParisiFinite.finiteTimeField_curvature_lipschitz line 517
  36. lemma OAI.ParisiFinite.global_dyadic_curvature_tendstoUniformly line 523
  37. lemma OAI.ParisiPath.generatorC2_bound line 551
  38. lemma OAI.ParisiPath.generatorC2_integrable line 556
  39. lemma OAI.ParisiPath.timeDerivativeC2_integrable_inner line 567
  40. lemma OAI.ParisiPath.timeGeneratorC2_aestronglyMeasurable line 576
  41. lemma OAI.ParisiPath.timeDerivativeC2_aestronglyMeasurable line 584
  42. lemma OAI.ParisiPath.timeGeneratorC2_intervalIntegrable line 592
  43. lemma OAI.ParisiPath.timeDerivativeC2_intervalIntegrable line 602
  44. theorem OAI.ParisiFinite.finite_schedule_verification line 618