OAI/Geometry/SmoothYau/Spectrum/BilinearCoordinateMatrixPosDef.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.bilinearCoordinateMatrix line 47
  2. lemma OAI.YauCounterexamples.bilinearCoordinateMatrix_comp line 51
  3. lemma OAI.YauCounterexamples.coordinateMetricLaplacian_reindex line 68
  4. lemma OAI.YauCounterexamples.mixed_jacobianMatrix_id_isUnit line 87
  5. lemma OAI.YauCounterexamples.coordinateVector_self line 98
  6. lemma OAI.YauCounterexamples.metricCoefficients_self line 104
  7. lemma OAI.YauCounterexamples.laplaceBeltrami_self line 109
  8. lemma OAI.YauCounterexamples.bilinearCoordinateMatrix_posDef line 156
  9. lemma OAI.YauCounterexamples.contDiff_bilinearCoordinateMatrix line 173
  10. lemma OAI.YauCounterexamples.selfMetricMatrix_pullback line 183
  11. lemma OAI.YauCounterexamples.selfMetricMatrix_change_basis line 191
  12. lemma OAI.YauCounterexamples.coordinateMetricLaplacian_basis_independent line 198
  13. theorem OAI.YauCounterexamples.laplaceBeltrami_self_any_basis line 209
  14. lemma OAI.YauCounterexamples.normalWaveMetric_pullback line 225
  15. theorem OAI.YauCounterexamples.laplaceBeltrami_normal_coordinates line 236
  16. lemma OAI.YauCounterexamples.clm_fderiv_apply line 290
  17. lemma OAI.YauCounterexamples.clm_second_fderiv line 296
  18. def OAI.YauCounterexamples.complexLaplaceBeltrami line 314
  19. def OAI.YauCounterexamples.complexCoordinateMetricLaplacian line 321
  20. lemma OAI.YauCounterexamples.complexCoordinateMetricLaplacian_expansion line 327
  21. lemma OAI.YauCounterexamples.normalWaveJacobian_isUnit line 369
  22. lemma OAI.YauCounterexamples.normalWave_complexCoordinate_expansion line 380
  23. lemma OAI.YauCounterexamples.complexCoordinateMetricLaplacian_normal_coordinates line 402
  24. theorem OAI.YauCounterexamples.complexLaplaceBeltrami_normal_coordinates line 423
  25. def OAI.YauCounterexamples.selfWaveMatrix line 482
  26. lemma OAI.YauCounterexamples.contDiff_selfWaveMatrix line 485
  27. lemma OAI.YauCounterexamples.selfWaveMatrix_det_pos line 489
  28. lemma OAI.YauCounterexamples.contDiff_selfWaveInverse line 494
  29. lemma OAI.YauCounterexamples.contDiff_selfWaveFirst line 502
  30. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_self_expansion line 514
  31. lemma OAI.YauCounterexamples.contDiff_complexLaplaceBeltrami_self line 531
  32. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_self_sum line 539
  33. lemma OAI.YauCounterexamples.complexLaplaceBeltrami_self_const_mul line 547
  34. lemma OAI.YauCounterexamples.finiteWaveSuperposition_residual line 554
  35. lemma OAI.YauCounterexamples.linearPullbackMetric_laplace line 588
  36. lemma OAI.YauCounterexamples.bilinearCoordinateMatrix_posDef_normed line 630
  37. lemma OAI.YauCounterexamples.coordinateMetricLaplacian_change_basis_normed line 645
  38. lemma OAI.YauCounterexamples.laplaceBeltrami_any_basis_univ line 677