OAI/MathematicalPhysics/CriticalSK/SaddleLimit.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.saddleRadius_le_iff line 59
  2. lemma OAI.CriticalSK.le_saddleRadius_iff line 72
  3. lemma OAI.CriticalSK.semicircleResolvent_gt_from_inverse line 85
  4. lemma OAI.CriticalSK.semicircleResolvent_subcritical_margin line 93
  5. lemma OAI.CriticalSK.subcritical_test_scale line 111
  6. lemma OAI.CriticalSK.saddleRadius_subcritical_lower line 121
  7. def OAI.CriticalSK.saddlePairDeficit line 134
  8. def OAI.CriticalSK.saddlePairSlope line 137
  9. lemma OAI.CriticalSK.saddlePairDeficit_zero line 140
  10. lemma OAI.CriticalSK.saddlePairDeficit_hasDerivAt line 143
  11. lemma OAI.CriticalSK.saddlePairDeficit_continuousOn line 153
  12. lemma OAI.CriticalSK.subcritical_coefficient line 160
  13. lemma OAI.CriticalSK.subcritical_short_coefficient line 172
  14. lemma OAI.CriticalSK.saddlePairSlope_small_bound line 179
  15. lemma OAI.CriticalSK.saddlePairDeficit_small_bound line 207
  16. lemma OAI.CriticalSK.saddlePairDeficit_shrinking_cubic line 236
  17. lemma OAI.CriticalSK.semicircleResolvent_lt_from_inverse line 249
  18. lemma OAI.CriticalSK.subcritical_radius_gap line 258
  19. lemma OAI.CriticalSK.saddleRadius_subcritical_tendsto line 265
  20. lemma OAI.CriticalSK.sphericalVariational_deriv_tendsto line 296
  21. def OAI.CriticalSK.saddleSubcriticalError line 304
  22. lemma OAI.CriticalSK.saddleSubcriticalError_tendsto line 307
  23. lemma OAI.CriticalSK.spectralGood_reference line 341
  24. lemma OAI.CriticalSK.spectralGood_natural_controls line 349
  25. lemma OAI.CriticalSK.spectralGood_natural_top_tendsto line 367
  26. lemma OAI.CriticalSK.traceError_fixed_tendsto line 378
  27. lemma OAI.CriticalSK.spectralGood_natural_resolvent_tendsto line 388
  28. lemma OAI.CriticalSK.spectralGood_natural_saddle_tendsto line 411
  29. lemma OAI.CriticalSK.spectralGood_saddle_uniform line 422