OAI/MathematicalPhysics/CriticalSK/OrientationLimits.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.naturalEdgeScale_le_rpow line 70
  2. lemma OAI.CriticalSK.naturalEdgeScale_cutoff_tendsto line 84
  3. lemma OAI.CriticalSK.naturalEdgeScale_cutoff_eventually line 91
  4. lemma OAI.CriticalSK.cutoff_cubic_identity line 110
  5. lemma OAI.CriticalSK.rpow_exp_small_tendsto line 117
  6. lemma OAI.CriticalSK.edgeLength_sq_le_linear line 130
  7. def OAI.CriticalSK.naturalPartitionConstant line 136
  8. def OAI.CriticalSK.naturalPartitionBase line 139
  9. lemma OAI.CriticalSK.naturalPartitionBase_pos line 141
  10. lemma OAI.CriticalSK.naturalPartitionConstant_lower line 145
  11. lemma OAI.CriticalSK.naturalPartitionConstant_pos line 159
  12. def OAI.CriticalSK.naturalOrientationTail line 162
  13. lemma OAI.CriticalSK.naturalOrientationTail_bound line 166
  14. lemma OAI.CriticalSK.naturalOrientationTail_scaled_tendsto line 194
  15. structure OAI.CriticalSK.OrientationInputs line 208
  16. lemma OAI.CriticalSK.orthogonal_equal_norm_pair line 221
  17. lemma OAI.CriticalSK.largeL_space line 230
  18. lemma OAI.CriticalSK.naturalOrientationInputs line 235
  19. lemma OAI.CriticalSK.spectralGood_orientation_variance line 303
  20. lemma OAI.CriticalSK.edgeLength_rpow_lower line 321
  21. lemma OAI.CriticalSK.edgeLength_rpow_upper line 328
  22. lemma OAI.CriticalSK.naturalEdgeScale_sqrt line 339
  23. lemma OAI.CriticalSK.natural_smallBall_rate line 343
  24. def OAI.CriticalSK.naturalOverlapRate line 348
  25. def OAI.CriticalSK.naturalOverlapConstant line 351
  26. lemma OAI.CriticalSK.naturalOverlapRate_nonneg line 354
  27. lemma OAI.CriticalSK.naturalOverlapRate_scaled_bound line 358