OAI/Probability/ParisiFinite/MeasureCoefficientOnSupportGap.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Measure Coefficient On Support Gap.

  1. lemma OAI.ParisiFinite.measureCoefficient_on_support_gap line 17
  2. lemma OAI.ParisiFinite.measureCoefficient_on_support_gap_pos line 25
  3. theorem OAI.ParisiFinite.minimizingParisi_gap_of_not_full_support line 37
  4. lemma OAI.ParisiFinite.dyadicSchedule_congr_on_Ico line 58
  5. lemma OAI.ParisiFinite.field_on_plateau line 73
  6. def OAI.ParisiFinite.canonicalSmoothField line 93
  7. lemma OAI.ParisiFinite.fieldGradient_on_plateau line 106
  8. lemma OAI.ParisiFinite.fieldCurvature_on_plateau line 120
  9. lemma OAI.ParisiFinite.fieldGradient_tilted_variance_pos line 139
  10. lemma OAI.ParisiFinite.fieldCurvature_gt_tilted_mean_on_plateau line 179
  11. lemma OAI.ParisiFinite.minimizingParisi_squareCurvature_integral_between_support line 198
  12. lemma OAI.ParisiFinite.minimizingParisi_deviation_integral_between_support line 217
  13. lemma OAI.ParisiFinite.minimizingParisi_deviation_integral_le_zero line 234
  14. lemma OAI.ParisiFinite.minimizingParisi_replicon_zero line 249
  15. lemma OAI.ParisiFinite.minimizingParisi_replicon_of_lt_one line 290
  16. theorem OAI.ParisiFinite.minimizingParisi_not_strictConvex_between_support line 303
  17. theorem OAI.ParisiFinite.minimizingParisi_noGap_countercase line 337
  18. lemma OAI.ParisiFinite.contact_area_has_interior_localMax line 384
  19. theorem OAI.ParisiFinite.minimizingParisi_localMax_between_support line 423
  20. theorem OAI.ParisiFinite.minimizingParisi_positive_plateau_localMax_countercase line 441
  21. def OAI.ParisiFinite.terminalPerturbation line 474
  22. def OAI.ParisiFinite.SmoothField.directional line 494
  23. def OAI.ParisiFinite.terminalFamily line 519
  24. def OAI.ParisiFinite.evolveFamily line 551
  25. lemma OAI.ParisiFinite.ambientStep_real line 556
  26. lemma OAI.ParisiFinite.ambientTilt_real line 560
  27. lemma OAI.ParisiFinite.evolveFamily_val line 565
  28. def OAI.ParisiFinite.linearEvolve line 576
  29. lemma OAI.ParisiFinite.evolveFamily_dot line 580
  30. lemma OAI.ParisiFinite.hasDerivAt_evolve_terminal line 590