OAI/Geometry/SmoothYau/Spectrum/ProductFrequencyTop.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.sphereFrequency line 37
  2. def OAI.YauCounterexamples.inverseFrequency line 38
  3. lemma OAI.YauCounterexamples.sphereFrequency_atTop line 40
  4. lemma OAI.YauCounterexamples.inverseFrequency_zero line 43
  5. lemma OAI.YauCounterexamples.inverseFrequency_pow_zero line 45
  6. lemma OAI.YauCounterexamples.sphereFrequency_mul_pow line 48
  7. lemma OAI.YauCounterexamples.sphereFrequency_mul_pow_zero line 54
  8. lemma OAI.YauCounterexamples.sphereFrequency_ratio line 65
  9. theorem OAI.YauCounterexamples.positive_factor_rates line 76
  10. lemma OAI.YauCounterexamples.eventual_output_rate line 110
  11. def OAI.YauCounterexamples.threeComplexPower line 134
  12. def OAI.YauCounterexamples.threePower line 136
  13. lemma OAI.YauCounterexamples.threeComplexPower_smooth line 138
  14. lemma OAI.YauCounterexamples.threePower_smooth line 146
  15. lemma OAI.YauCounterexamples.threeComplexPower_chart line 149
  16. lemma OAI.YauCounterexamples.threePower_chart line 165
  17. def OAI.YauCounterexamples.productFrequency line 173
  18. lemma OAI.YauCounterexamples.productFrequency_pos line 174
  19. theorem OAI.YauCounterexamples.threePower_eigen line 179
  20. def OAI.YauCounterexamples.productWaveFrequency line 214
  21. lemma OAI.YauCounterexamples.productFrequency_nonneg line 215
  22. lemma OAI.YauCounterexamples.productWaveFrequency_equation line 218
  23. lemma OAI.YauCounterexamples.productWaveFrequency_bounds line 223
  24. lemma OAI.YauCounterexamples.productWaveFrequency_tendsto line 231
  25. lemma OAI.YauCounterexamples.productWaveFrequency_ratio_formula line 235
  26. lemma OAI.YauCounterexamples.productWaveFrequency_ratio_tendsto line 243
  27. lemma OAI.YauCounterexamples.productFrequency_atTop line 257
  28. lemma OAI.YauCounterexamples.productFrequency_mul_pow line 260
  29. lemma OAI.YauCounterexamples.productFrequency_mul_pow_zero line 267
  30. lemma OAI.YauCounterexamples.productFrequency_ratio line 279
  31. theorem OAI.YauCounterexamples.product_positive_factor_rates line 290
  32. theorem OAI.YauCounterexamples.CompactMetricAtlas.eventually_product_positive_factor_of_jets line 331
  33. theorem OAI.YauCounterexamples.CompactMetricAtlas.eventually_product_positive_factor_of_eventual_jets line 379