OAI/Probability/ParisiFinite/DyadicEvolutionGridBound.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Dyadic Evolution Grid Bound.

  1. lemma OAI.ParisiFinite.dyadicEvolution_grid_bound line 63
  2. lemma OAI.ParisiFinite.dyadic_low_tendstoUniformly line 78
  3. lemma OAI.ParisiFinite.dyadicSchedule_coeff_bound line 90
  4. lemma OAI.ParisiFinite.dyadicEvolution_terminal_gradient line 106
  5. def OAI.ParisiFinite.field line 124
  6. def OAI.ParisiFinite.fieldGradient line 127
  7. lemma OAI.ParisiFinite.hasDerivAt_field line 130
  8. lemma OAI.ParisiFinite.fieldGradient_lipschitz line 139
  9. lemma OAI.ParisiFinite.fieldGradient_bound line 147
  10. lemma OAI.ParisiFinite.gaussian_integral_neg line 164
  11. lemma OAI.ParisiFinite.step_even line 169
  12. lemma OAI.ParisiFinite.evolve_even line 183
  13. lemma OAI.ParisiFinite.field_even line 190
  14. lemma OAI.ParisiFinite.fieldGradient_odd line 197
  15. lemma OAI.ParisiFinite.fieldGradient_zero line 207
  16. lemma OAI.ParisiFinite.dyadicEvolution_zero_width line 214
  17. lemma OAI.ParisiFinite.field_terminal line 226
  18. lemma OAI.ParisiFinite.fieldGradient_terminal line 232
  19. lemma OAI.ParisiFinite.curvature_gradient_monotone line 247
  20. lemma OAI.ParisiFinite.fieldGradient_monotone line 251
  21. lemma OAI.ParisiFinite.curvature_hamiltonian_bounds line 265
  22. lemma OAI.ParisiFinite.step_curvature_time_bound line 275
  23. lemma OAI.ParisiFinite.recursion_terminal_time_bound line 309
  24. lemma OAI.ParisiFinite.field_terminal_time_bound line 326
  25. lemma OAI.ParisiFinite.dyadicEvolution_stable line 345
  26. lemma OAI.ParisiFinite.dyadicEvolution_half line 355
  27. lemma OAI.ParisiFinite.field_half_DPP line 376
  28. def OAI.ParisiFinite.transitionMeasure line 400
  29. instance OAI.ParisiFinite.transitionMeasure_probability line 403
  30. lemma OAI.ParisiFinite.transition_integral line 409
  31. lemma OAI.ParisiFinite.transition_magnetization line 416
  32. lemma OAI.ParisiFinite.gaussian_density_ibp line 420
  33. lemma OAI.ParisiFinite.transition_increment_mean line 434
  34. lemma OAI.ParisiFinite.integrable_sq_exp_shift line 446
  35. lemma OAI.ParisiFinite.gaussian_density_second_moment line 458
  36. lemma OAI.ParisiFinite.transition_increment_second_moment line 482
  37. lemma OAI.ParisiFinite.transition_increment_bounds line 498
  38. def OAI.ParisiFinite.noiseTiltKernel line 523
  39. lemma OAI.ParisiFinite.measurable_noise_density line 527
  40. lemma OAI.ParisiFinite.noiseTiltKernel_apply line 534
  41. instance OAI.ParisiFinite.noiseTiltKernel_markov line 539
  42. def OAI.ParisiFinite.transitionKernel line 545
  43. instance OAI.ParisiFinite.transitionKernel_markov line 548
  44. lemma OAI.ParisiFinite.transitionKernel_apply line 552
  45. def OAI.ParisiFinite.evolutionKernel line 560
  46. instance OAI.ParisiFinite.evolutionKernel_markov line 565
  47. lemma OAI.ParisiFinite.integrable_smooth_d1 line 574
  48. lemma OAI.ParisiFinite.evolution_magnetization line 581
  49. lemma OAI.ParisiFinite.evolution_tanh line 592
  50. lemma OAI.ParisiFinite.integrable_transition_sq line 604
  51. lemma OAI.ParisiFinite.integrable_transition_id line 617
  52. lemma OAI.ParisiFinite.integrable_transition_increment line 624
  53. lemma OAI.ParisiFinite.integrable_transition_increment_sq line 628
  54. lemma OAI.ParisiFinite.transition_source_second_moment line 634
  55. lemma OAI.ParisiFinite.transition_lyapunov_bound line 649