OAI/Geometry/SmoothYau/Spectrum/VaryingSpectralResolventBase.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingShift_base_comp_resolvent line 34
  2. def OAI.YauCounterexamples.CompactMetricAtlas.varyingResolvent line 46
  3. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingResolvent_equation line 53
  4. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingResolvent_base line 69
  5. def OAI.YauCounterexamples.CompactMetricAtlas.varyingSpectralResolvent line 75
  6. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingSpectralResolvent_compact line 82
  7. theorem OAI.YauCounterexamples.CompactMetricAtlas.varyingResolvent_tendsto line 90
  8. lemma OAI.YauCounterexamples.laplaceBeltrami_const_mul_C2 line 115
  9. theorem OAI.YauCounterexamples.CompactMetricAtlas.represented_eigenfunction_smooth line 129
  10. theorem OAI.YauCounterexamples.CompactMetricAtlas.shiftedInverse_eigenfunction line 155
  11. theorem OAI.YauCounterexamples.CompactMetricAtlas.realSpectralResolvent_eigenfunction line 188
  12. lemma OAI.YauCounterexamples.MetricIntegralAtlas.eigen_mean_laplace_difference line 214
  13. def OAI.YauCounterexamples.CompactMetricAtlas.scalarTestCLM line 243
  14. lemma OAI.YauCounterexamples.CompactMetricAtlas.scalarTestCLM_apply line 249
  15. def OAI.YauCounterexamples.laplaceFamilyBCF line 258
  16. def OAI.YauCounterexamples.laplaceDerivativeBCF line 261
  17. lemma OAI.YauCounterexamples.laplaceFamilyBCF_first_quotient line 269
  18. def OAI.YauCounterexamples.CompactMetricAtlas.laplaceVariationTest line 279
  19. lemma OAI.YauCounterexamples.CompactMetricAtlas.laplaceVariationTest_limit line 282
  20. lemma OAI.YauCounterexamples.CompactMetricAtlas.laplaceVariationTest_eigen_zero line 289
  21. lemma OAI.YauCounterexamples.real_positive_shift_solution_unique line 317
  22. lemma OAI.YauCounterexamples.smoothMetric_eq_of_inner_eq line 332
  23. lemma OAI.YauCounterexamples.pinnedMetric_at_zero line 339
  24. theorem OAI.YauCounterexamples.CompactMetricAtlas.shiftedInverse_of_smooth_eigenfunction line 356
  25. def OAI.YauCounterexamples.CompactMetricAtlas.realSmoothRepresentativeLM line 384
  26. lemma OAI.YauCounterexamples.CompactMetricAtlas.realSmoothRepresentativeLM_injective line 396
  27. theorem OAI.YauCounterexamples.CompactMetricAtlas.smoothFamily_resolvent_tendsto line 406
  28. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingSpectralResolvent_base line 440
  29. lemma OAI.YauCounterexamples.CompactMetricAtlas.varyingSpectralResolvent_eq_base line 448
  30. lemma OAI.YauCounterexamples.CompactMetricAtlas.scalarTestCLM_pinned_deriv line 456
  31. theorem OAI.YauCounterexamples.CompactMetricAtlas.actual_pinned_eventually_simple line 472