OAI/Geometry/SmoothYau/Smoothness/SmoothFiniteWaveSum.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.UniformJetBounds line 38
  2. lemma OAI.YauCounterexamples.UniformJetBounds.mono line 41
  3. lemma OAI.YauCounterexamples.UniformJetBounds.const line 48
  4. lemma OAI.YauCounterexamples.UniformJetBounds.add line 57
  5. lemma OAI.YauCounterexamples.UniformJetBounds.sum line 71
  6. lemma OAI.YauCounterexamples.UniformJetBounds.mul line 88
  7. lemma OAI.YauCounterexamples.UniformJetBounds.common line 109
  8. lemma OAI.YauCounterexamples.uniformJetBounds_of_continuous_jets line 122
  9. lemma OAI.YauCounterexamples.totalDegree_pderiv_le line 136
  10. lemma OAI.YauCounterexamples.uniformJetBounds_realPolyEval line 153
  11. lemma OAI.YauCounterexamples.uniformJetBounds_smoothPolynomialLaplacian line 159
  12. lemma OAI.YauCounterexamples.uniformJetBounds_smoothEikonalResidual line 192
  13. lemma OAI.YauCounterexamples.uniformJetBounds_smoothPhaseTransportVector line 221
  14. lemma OAI.YauCounterexamples.uniformJetBounds_smoothPhaseTransportScalar line 238
  15. lemma OAI.YauCounterexamples.uniformJetBounds_smoothWaveTransport line 251
  16. lemma OAI.YauCounterexamples.uniformJetBounds_finiteWaveTransport line 273
  17. lemma OAI.YauCounterexamples.UniformJetBounds.finite_common line 322
  18. lemma OAI.YauCounterexamples.uniformJetBounds_polynomialWaveRemainder line 337
  19. theorem OAI.YauCounterexamples.generated_wave_uniform_jets line 360
  20. lemma OAI.YauCounterexamples.norm_iteratedFDeriv_waveDeriv line 443
  21. lemma OAI.YauCounterexamples.UniformJetBounds.waveDeriv line 452
  22. lemma OAI.YauCounterexamples.UniformJetBounds.fixed line 463
  23. lemma OAI.YauCounterexamples.SmoothJetZero.congr_eventually line 471
  24. lemma OAI.YauCounterexamples.contDiff_waveGradientPair line 479
  25. lemma OAI.YauCounterexamples.contDiff_waveCoordinateOperator line 486
  26. lemma OAI.YauCounterexamples.contDiff_finiteWaveTransport line 494
  27. lemma OAI.YauCounterexamples.UniformJetBounds.gradientPair line 503
  28. lemma OAI.YauCounterexamples.UniformJetBounds.coordinateOperator line 523
  29. lemma OAI.YauCounterexamples.UniformJetBounds.transport line 555
  30. def OAI.YauCounterexamples.smoothFiniteWave line 605
  31. def OAI.YauCounterexamples.smoothWaveRemainder line 608
  32. def OAI.YauCounterexamples.smoothWaveEikonal line 613
  33. lemma OAI.YauCounterexamples.contDiff_smoothWaveEikonal line 616
  34. lemma OAI.YauCounterexamples.contDiff_smoothWaveRemainder line 621
  35. lemma OAI.YauCounterexamples.smooth_wave_residual_expansion line 631
  36. lemma OAI.YauCounterexamples.waveDeriv_congr_eventually line 657
  37. lemma OAI.YauCounterexamples.waveGradientPair_congr_eventually line 662
  38. lemma OAI.YauCounterexamples.waveCoordinateOperator_congr_eventually line 672
  39. lemma OAI.YauCounterexamples.finiteWaveTransport_congr_eventually line 684
  40. lemma OAI.YauCounterexamples.smoothWaveRemainder_congr_eventually line 693
  41. theorem OAI.YauCounterexamples.smooth_wave_uniform_residual_bound line 733
  42. lemma OAI.YauCounterexamples.smoothWaveEikonal_realPolyEval line 831
  43. lemma OAI.YauCounterexamples.smoothWaveRemainder_realPolyEval line 835
  44. lemma OAI.YauCounterexamples.cutoff_polynomial_remainders_vanish line 845
  45. lemma OAI.YauCounterexamples.uniformJetBounds_smoothWaveEikonal line 869
  46. lemma OAI.YauCounterexamples.uniformJetBounds_smoothWaveRemainder line 881
  47. theorem OAI.YauCounterexamples.cutoff_polynomial_wave_residual_bound line 902
  48. lemma OAI.YauCounterexamples.smoothFiniteWave_eq_sum line 976
  49. lemma OAI.YauCounterexamples.smoothFiniteWave_cutoff line 986
  50. lemma OAI.YauCounterexamples.smoothFiniteWave_cutoff_support line 995
  51. lemma OAI.YauCounterexamples.smoothFiniteWave_cutoff_compact line 1001
  52. theorem OAI.YauCounterexamples.smooth_finite_wave_uniform_derivatives line 1006