OAI/Geometry/SmoothYau/Smoothness/ContDiffSmoothFiniteWave.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.contDiff_frameChristoffel line 55
  2. lemma OAI.YauCounterexamples.contDiff_normalJetFamily line 64
  3. lemma OAI.YauCounterexamples.contDiff_normalMetricFamily_apply line 72
  4. theorem OAI.YauCounterexamples.compact_normal_coordinate_radius line 82
  5. lemma OAI.YauCounterexamples.normal_iteratedFDeriv_comp_clm_at line 164
  6. lemma OAI.YauCounterexamples.parameter_iteratedFDeriv line 176
  7. lemma OAI.YauCounterexamples.continuousAt_parameter_iteratedFDeriv line 189
  8. lemma OAI.YauCounterexamples.parameter_fderiv_apply line 238
  9. lemma OAI.YauCounterexamples.contDiff_parameter_fderiv_apply line 245
  10. lemma OAI.YauCounterexamples.continuous_parameter_iteratedFDeriv line 250
  11. lemma OAI.YauCounterexamples.contDiff_matrix_det line 257
  12. lemma OAI.YauCounterexamples.contDiff_matrix_adjugate line 268
  13. lemma OAI.YauCounterexamples.contDiffOn_matrix_inv line 282
  14. abbrev OAI.YauCounterexamples.NormalWaveSpace line 324
  15. abbrev OAI.YauCounterexamples.NormalWaveParameter line 325
  16. def OAI.YauCounterexamples.normalWaveMetric line 327
  17. lemma OAI.YauCounterexamples.contDiff_normalWaveMetric line 332
  18. lemma OAI.YauCounterexamples.normalWaveMetric_zero line 336
  19. lemma OAI.YauCounterexamples.normalWaveMetric_first_jet line 346
  20. lemma OAI.YauCounterexamples.hasFDerivAt_matrix_inv_zero line 354
  21. lemma OAI.YauCounterexamples.normalWaveInverse_first_jet line 373
  22. theorem OAI.YauCounterexamples.exists_normal_inverse_extension line 378
  23. def OAI.YauCounterexamples.normalWaveFirstCoefficient line 415
  24. lemma OAI.YauCounterexamples.normalWaveMetric_det_first_jet line 423
  25. lemma OAI.YauCounterexamples.normalWaveFirstCoefficient_zero line 432
  26. theorem OAI.YauCounterexamples.exists_normal_wave_coefficients line 446
  27. lemma OAI.YauCounterexamples.density_first_derivative line 539
  28. lemma OAI.YauCounterexamples.normalWaveDensity_firstCoefficient line 553
  29. lemma OAI.YauCounterexamples.compact_family_positive_radius line 573
  30. lemma OAI.YauCounterexamples.compact_normal_density_radius line 590
  31. abbrev OAI.YauCounterexamples.normalWaveEquiv line 637
  32. lemma OAI.YauCounterexamples.normalWaveEquiv_single line 640
  33. theorem OAI.YauCounterexamples.exists_normal_wave_pi_coefficients line 645
  34. lemma OAI.YauCounterexamples.normal_profile_family_smooth line 695
  35. lemma OAI.YauCounterexamples.contDiff_smoothFiniteWave line 737
  36. lemma OAI.YauCounterexamples.contDiff_canonicalCutoffWave line 745
  37. def OAI.YauCounterexamples.normalWavePiOperator line 753
  38. lemma OAI.YauCounterexamples.normalWavePiOperator_eq line 760
  39. lemma OAI.YauCounterexamples.normalWavePiOperator_eq_extension line 775