OAI/Geometry/SmoothYau/Spectrum/JointLocalLaplacian.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.differentiableAt_metricFlux line 42
  2. lemma OAI.YauCounterexamples.localLaplacian_change line 58
  3. lemma OAI.YauCounterexamples.laplaceBeltrami_inChart line 84
  4. lemma OAI.YauCounterexamples.contDiffAt_metricFlux line 128
  5. lemma OAI.YauCounterexamples.contDiffAt_localLaplacian line 140
  6. lemma OAI.YauCounterexamples.contMDiff_laplaceBeltrami line 152
  7. lemma OAI.YauCounterexamples.round_metricCoefficients line 207
  8. lemma OAI.YauCounterexamples.round_metricCoefficients_zero line 214
  9. lemma OAI.YauCounterexamples.round_metricCoefficients_first line 220
  10. lemma OAI.YauCounterexamples.round_metricFirstCoefficient_zero line 225
  11. theorem OAI.YauCounterexamples.round_laplace_at_center line 233
  12. def OAI.YauCounterexamples.roundPower line 278
  13. lemma OAI.YauCounterexamples.roundPower_smooth line 281
  14. lemma OAI.YauCounterexamples.complex_inverse_gram_trace line 287
  15. lemma OAI.YauCounterexamples.roundPower_complex_hessian_trace line 295
  16. theorem OAI.YauCounterexamples.roundPower_eigen line 337
  17. theorem OAI.YauCounterexamples.laplaceBeltrami_chart_metric line 369
  18. theorem OAI.YauCounterexamples.laplaceBeltrami_manifoldChartPush line 397
  19. lemma OAI.YauCounterexamples.laplaceBeltrami_metric_congr_nhds line 449
  20. theorem OAI.YauCounterexamples.roundPower_residual_tsupport line 474
  21. lemma OAI.YauCounterexamples.joint_localLaplacian line 512
  22. lemma OAI.YauCounterexamples.joint_laplaceBeltrami_chart line 540
  23. lemma OAI.YauCounterexamples.contDiffAt_partial_time_deriv line 551
  24. lemma OAI.YauCounterexamples.continuous_joint_of_chart line 564
  25. lemma OAI.YauCounterexamples.continuous_joint_laplaceBeltrami line 584
  26. lemma OAI.YauCounterexamples.continuous_joint_laplaceBeltrami_time_deriv line 590
  27. lemma OAI.YauCounterexamples.hasDerivAt_laplaceBeltrami_time line 597