OAI/Probability/ParisiFinite/HasDerivAtDeviation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Has Deriv At Deviation.

  1. lemma OAI.ParisiFinite.hasDerivAt_deviation line 19
  2. theorem OAI.ParisiFinite.minimizingParisi_replicon line 26
  3. theorem OAI.ParisiFinite.minimizingParisi_support_endpoint line 74
  4. theorem OAI.ParisiFinite.minimizingParisi_diffusion_square line 98
  5. lemma OAI.ParisiFinite.measureCoefficient_after_support line 129
  6. lemma OAI.ParisiFinite.dyadicSchedule_congr_future line 140
  7. lemma OAI.ParisiFinite.field_final_plateau line 151
  8. lemma OAI.ParisiFinite.fieldGradient_final_plateau line 163
  9. lemma OAI.ParisiFinite.fieldCurvature_final_plateau line 172
  10. theorem OAI.ParisiFinite.minimizingParisi_endpoint_bound line 190
  11. lemma OAI.ParisiFinite.measureCoefficient_before_support line 251
  12. lemma OAI.ParisiFinite.dyadicSchedule_congr_initial line 262
  13. lemma OAI.ParisiFinite.field_lipschitz line 274
  14. lemma OAI.ParisiFinite.field_initial_heat line 279
  15. lemma OAI.ParisiFinite.hasDerivAt_step_mean line 295
  16. lemma OAI.ParisiFinite.fieldGradient_initial_heat line 315
  17. lemma OAI.ParisiFinite.fieldCurvature_initial_heat line 329
  18. lemma OAI.ParisiFinite.bounded_lipschitz_square line 355
  19. lemma OAI.ParisiFinite.step_mean_square_le line 367
  20. lemma OAI.ParisiFinite.fieldCurvature_square_lipschitz line 379
  21. lemma OAI.ParisiFinite.initial_heat_curvature_square_le line 385
  22. lemma OAI.ParisiFinite.step_mean_zero_eq_gaussian_integral line 405
  23. lemma OAI.ParisiFinite.BoundedCoefficient.solution_initial_heat line 433
  24. lemma OAI.ParisiFinite.BoundedCoefficient.expectedSquareCurvature_initial_heat line 453
  25. lemma OAI.ParisiFinite.BoundedCoefficient.expectedSquareCurvature_initial_le line 472
  26. lemma OAI.ParisiFinite.BoundedCoefficient.expectedSquareCurvature_zero line 480
  27. lemma OAI.ParisiFinite.fieldCurvature_not_constant line 507
  28. lemma OAI.ParisiFinite.fieldCurvature_gaussian_variance_pos line 526
  29. lemma OAI.ParisiFinite.minimizingParisi_least_support_eq_zero line 557
  30. theorem OAI.ParisiFinite.minimizingParisi_zero_mem_support line 621