OAI/Geometry/SmoothYau/Spectrum/ScalarCompDirectional.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.laplaceBeltrami_neg line 26
  2. theorem OAI.YauCounterexamples.laplaceBeltrami_nonpos_at_localMax line 32
  3. theorem OAI.YauCounterexamples.laplaceBeltrami_nonneg_at_localMin line 55
  4. theorem OAI.YauCounterexamples.positive_shift_kernel_eq_zero line 63
  5. lemma OAI.YauCounterexamples.contDiffAt_inChart_C2 line 95
  6. lemma OAI.YauCounterexamples.fderiv_inChart_change_C2 line 101
  7. lemma OAI.YauCounterexamples.metricFlux_change_C2 line 122
  8. lemma OAI.YauCounterexamples.differentiableAt_metricFlux_C2 line 148
  9. lemma OAI.YauCounterexamples.localLaplacian_change_C2 line 164
  10. lemma OAI.YauCounterexamples.laplaceBeltrami_inChart_C2 line 190
  11. lemma OAI.YauCounterexamples.localLaplacian_expansion_C2 line 199
  12. theorem OAI.YauCounterexamples.laplaceBeltrami_nonpos_at_localMax_C2 line 262
  13. theorem OAI.YauCounterexamples.laplaceBeltrami_nonneg_at_localMin_C2 line 285
  14. theorem OAI.YauCounterexamples.positive_shift_kernel_eq_zero_C2 line 293
  15. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_inChart line 330
  16. lemma OAI.YauCounterexamples.complex_positive_shift_kernel_eq_zero line 380
  17. lemma OAI.YauCounterexamples.contDiffAt_complex_inChart line 409
  18. lemma OAI.YauCounterexamples.contMDiff_const_mul_complex line 418
  19. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_add line 423
  20. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_const_mul line 434
  21. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_zero line 442
  22. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_congr line 447
  23. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_sum line 459
  24. lemma OAI.YauCounterexamples.contMDiff_chartLift_order line 477
  25. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_chartLift line 491
  26. lemma OAI.YauCounterexamples.second_fderiv_mul_at line 513
  27. def OAI.YauCounterexamples.coordinateGradientPair line 544
  28. lemma OAI.YauCounterexamples.laplaceBeltrami_mul line 549
  29. lemma OAI.YauCounterexamples.weightedLaplacian_expansion line 612
  30. lemma OAI.YauCounterexamples.weightedLaplacian_product_formula line 667
  31. lemma OAI.YauCounterexamples.scalar_comp_directional line 683
  32. lemma OAI.YauCounterexamples.scalar_comp_second_directional line 688
  33. lemma OAI.YauCounterexamples.localLaplacian_expansion_at line 721
  34. theorem OAI.YauCounterexamples.laplaceBeltrami_comp_at line 784