OAI/MathematicalPhysics/CriticalSK/EdgeAsymptotics.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.edgeLength line 34
  2. def OAI.CriticalSK.naturalEdgeScale line 36
  3. def OAI.CriticalSK.formConstant line 38
  4. lemma OAI.CriticalSK.edgeLength_pos line 40
  5. lemma OAI.CriticalSK.edgeLength_cast_pos line 42
  6. lemma OAI.CriticalSK.edgeLength_cube line 44
  7. lemma OAI.CriticalSK.naturalEdgeScale_pos line 49
  8. lemma OAI.CriticalSK.naturalEdgeScale_base line 52
  9. lemma OAI.CriticalSK.formConstant_pos line 58
  10. lemma OAI.CriticalSK.formA_edgeLength line 60
  11. lemma OAI.CriticalSK.formA_natural_scale line 93
  12. lemma OAI.CriticalSK.orderedJacobiGaps_top_bound line 106
  13. lemma OAI.CriticalSK.edgeLength_tendsto line 115
  14. lemma OAI.CriticalSK.edgeLength_sq_div_bound line 126
  15. lemma OAI.CriticalSK.edgeLength_sq_div_tendsto line 133
  16. lemma OAI.CriticalSK.edgeLength_div_sqrt_tendsto line 138
  17. lemma OAI.CriticalSK.naturalEdgeScale_tendsto line 143
  18. lemma OAI.CriticalSK.formB_natural_scale_tendsto line 147
  19. lemma OAI.CriticalSK.formC_natural_scale_tendsto line 154
  20. lemma OAI.CriticalSK.naturalEdgeScale_space line 162
  21. lemma OAI.CriticalSK.formB_tendsto line 181
  22. lemma OAI.CriticalSK.formC_tendsto line 184
  23. lemma OAI.CriticalSK.formA_tendsto line 188
  24. lemma OAI.CriticalSK.edgeLength_tents_eventually line 193
  25. lemma OAI.CriticalSK.orderedJacobiGaps_natural_top line 203
  26. lemma OAI.CriticalSK.orderedJacobiGaps_le_four line 221
  27. lemma OAI.CriticalSK.spectralGood_resolvent line 236
  28. def OAI.CriticalSK.traceCost line 274
  29. lemma OAI.CriticalSK.traceCost_nonneg line 278
  30. lemma OAI.CriticalSK.traceCost_antitone line 284
  31. lemma OAI.CriticalSK.traceError_eq_cost line 302
  32. lemma OAI.CriticalSK.spectralGood_relative_trace line 314
  33. lemma OAI.CriticalSK.traceCost_small line 325
  34. def OAI.CriticalSK.edgeFixedCost line 345
  35. lemma OAI.CriticalSK.edgeFixedCost_tendsto line 348
  36. lemma OAI.CriticalSK.traceCost_natural_le line 356
  37. lemma OAI.CriticalSK.traceCost_natural_eventually line 368
  38. lemma OAI.CriticalSK.exists_natural_edge_parameters line 378
  39. lemma OAI.CriticalSK.spectralGood_relative_error line 386
  40. lemma OAI.CriticalSK.spectralGood_bounded line 395
  41. lemma OAI.CriticalSK.spectralGood_top_upper line 408
  42. lemma OAI.CriticalSK.spectralGood_top_close line 416
  43. lemma OAI.CriticalSK.finite_cover_sum line 435
  44. lemma OAI.CriticalSK.dyadic_real_cover line 456
  45. lemma OAI.CriticalSK.rpow_dyadic_shell line 465
  46. lemma OAI.CriticalSK.fractional_resolvent_counting line 479
  47. lemma OAI.CriticalSK.rpow_three_halves line 565
  48. lemma OAI.CriticalSK.jacobi_fractional_resolvent line 570
  49. lemma OAI.CriticalSK.semicircleResolvent_deficit_lower line 587
  50. lemma OAI.CriticalSK.sum_pair_tail_real line 595
  51. def OAI.CriticalSK.fixedEdgeVariance line 601
  52. lemma OAI.CriticalSK.fixedEdgeVariance_coe line 604
  53. lemma OAI.CriticalSK.fixedEdgeVariance_pos line 609
  54. lemma OAI.CriticalSK.fixedEdgeVariance_inverse line 614
  55. lemma OAI.CriticalSK.bulk_fixedTilt_bounds line 619
  56. lemma OAI.CriticalSK.fixedEdgeVariance_upper line 671
  57. lemma OAI.CriticalSK.fixedEdgeVariance_lower line 679
  58. lemma OAI.CriticalSK.spectralGood_fixed_variance line 686
  59. lemma OAI.CriticalSK.spectralGood_fixed_bulk line 712