OAI/Geometry/SmoothYau/Smoothness/BoundedDegreeMonomials.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.SmoothJetZero line 19
  2. lemma OAI.YauCounterexamples.SmoothJetZero.mono line 23
  3. lemma OAI.YauCounterexamples.SmoothJetZero.zero line 25
  4. lemma OAI.YauCounterexamples.SmoothJetZero.order_zero line 28
  5. lemma OAI.YauCounterexamples.SmoothJetZero.add line 29
  6. lemma OAI.YauCounterexamples.SmoothJetZero.neg line 36
  7. lemma OAI.YauCounterexamples.SmoothJetZero.sub line 39
  8. lemma OAI.YauCounterexamples.SmoothJetZero.sum line 44
  9. lemma OAI.YauCounterexamples.SmoothJetZero.mul line 52
  10. lemma OAI.YauCounterexamples.SmoothJetZero.mul_right line 70
  11. lemma OAI.YauCounterexamples.SmoothJetZero.mul_left line 74
  12. lemma OAI.YauCounterexamples.SmoothJetZero.fderiv line 79
  13. def OAI.YauCounterexamples.waveDirectionalDerivative line 101
  14. theorem OAI.YauCounterexamples.waveDirectionalDerivative_apply line 105
  15. theorem OAI.YauCounterexamples.waveDirectionalDerivative_X line 117
  16. theorem OAI.YauCounterexamples.waveDirectionalDerivative_C line 123
  17. theorem OAI.YauCounterexamples.waveDirectionalDerivative_homogeneous line 127
  18. theorem OAI.YauCounterexamples.waveDirectionalDerivative_degree_zero line 135
  19. def OAI.YauCounterexamples.wavePrimitiveTerm line 141
  20. theorem OAI.YauCounterexamples.wavePrimitiveTerm_homogeneous line 148
  21. theorem OAI.YauCounterexamples.wavePrimitiveTerm_derivative line 168
  22. def OAI.YauCounterexamples.waveNormSq line 191
  23. theorem OAI.YauCounterexamples.waveNormSq_pos line 193
  24. def OAI.YauCounterexamples.waveLinearCoordinate line 201
  25. theorem OAI.YauCounterexamples.waveLinearCoordinate_homogeneous line 204
  26. theorem OAI.YauCounterexamples.waveLinearCoordinate_derivative line 211
  27. theorem OAI.YauCounterexamples.wave_homogeneous_primitive line 232
  28. def OAI.YauCounterexamples.CoeffContinuous line 247
  29. theorem OAI.YauCounterexamples.CoeffContinuous.const line 252
  30. theorem OAI.YauCounterexamples.CoeffContinuous.add line 255
  31. theorem OAI.YauCounterexamples.CoeffContinuous.neg line 260
  32. theorem OAI.YauCounterexamples.CoeffContinuous.sub line 265
  33. theorem OAI.YauCounterexamples.CoeffContinuous.smul line 269
  34. theorem OAI.YauCounterexamples.CoeffContinuous.mul line 274
  35. theorem OAI.YauCounterexamples.CoeffContinuous.pow line 283
  36. theorem OAI.YauCounterexamples.CoeffContinuous.sum line 289
  37. theorem OAI.YauCounterexamples.CoeffContinuous.pderiv line 296
  38. theorem OAI.YauCounterexamples.CoeffContinuous.homogeneousComponent line 301
  39. theorem OAI.YauCounterexamples.waveDirectionalDerivative_coeffContinuous line 314
  40. theorem OAI.YauCounterexamples.waveLinearCoordinate_coeffContinuous line 321
  41. theorem OAI.YauCounterexamples.wavePrimitiveTerm_coeffContinuous line 332
  42. theorem OAI.YauCounterexamples.canonical_wavePrimitive_coeffContinuous line 343
  43. def OAI.YauCounterexamples.VanishTo line 355
  44. theorem OAI.YauCounterexamples.VanishTo.zero line 360
  45. theorem OAI.YauCounterexamples.VanishTo.order_zero line 364
  46. theorem OAI.YauCounterexamples.VanishTo.mono line 368
  47. theorem OAI.YauCounterexamples.VanishTo.add line 371
  48. theorem OAI.YauCounterexamples.VanishTo.neg line 376
  49. theorem OAI.YauCounterexamples.VanishTo.sub line 381
  50. theorem OAI.YauCounterexamples.VanishTo.sum line 385
  51. theorem OAI.YauCounterexamples.VanishTo.mul line 391
  52. theorem OAI.YauCounterexamples.VanishTo.mul_left line 406
  53. theorem OAI.YauCounterexamples.VanishTo.mul_right line 410
  54. theorem OAI.YauCounterexamples.VanishTo.smul line 414
  55. theorem OAI.YauCounterexamples.VanishTo.pderiv line 418
  56. theorem OAI.YauCounterexamples.VanishTo.of_homogeneous line 424
  57. theorem OAI.YauCounterexamples.VanishTo.of_constantCoeff_eq_zero line 427
  58. theorem OAI.YauCounterexamples.VanishTo.constantCoeff_eq_zero line 433
  59. theorem OAI.YauCounterexamples.VanishTo.constantCoeff_sub line 437
  60. theorem OAI.YauCounterexamples.VanishTo.remove_component line 442
  61. theorem OAI.YauCounterexamples.VanishTo.of_constant_and_linear line 451
  62. def OAI.YauCounterexamples.waveQuadratic line 469
  63. theorem OAI.YauCounterexamples.waveQuadratic_linearization line 472
  64. def OAI.YauCounterexamples.eikonalResidual line 514
  65. theorem OAI.YauCounterexamples.eikonal_initial_order line 517
  66. theorem OAI.YauCounterexamples.eikonal_linearization line 531
  67. theorem OAI.YauCounterexamples.eikonal_raise_order line 542
  68. theorem OAI.YauCounterexamples.finite_eikonal_completion line 566
  69. def OAI.YauCounterexamples.waveTransport line 600
  70. theorem OAI.YauCounterexamples.waveTransport_add line 603
  71. theorem OAI.YauCounterexamples.transport_linearization line 608
  72. theorem OAI.YauCounterexamples.transport_raise_order line 623
  73. theorem OAI.YauCounterexamples.finite_transport_completion line 645
  74. def OAI.YauCounterexamples.wavePhaseSeed line 666
  75. theorem OAI.YauCounterexamples.wavePhaseSeed_constantCoeff line 671
  76. theorem OAI.YauCounterexamples.wavePhaseSeed_gradient line 675
  77. theorem OAI.YauCounterexamples.wavePhaseSeed_hessian line 680
  78. theorem OAI.YauCounterexamples.wavePhaseSeed_eikonal line 686
  79. def OAI.YauCounterexamples.wavePrimitive line 702
  80. theorem OAI.YauCounterexamples.wavePrimitive_homogeneous line 705
  81. theorem OAI.YauCounterexamples.wavePrimitive_derivative line 712
  82. def OAI.YauCounterexamples.eikonalCorrection line 719
  83. theorem OAI.YauCounterexamples.eikonalCorrection_homogeneous line 723
  84. theorem OAI.YauCounterexamples.eikonalCorrection_raises line 732
  85. def OAI.YauCounterexamples.eikonalIter line 752
  86. theorem OAI.YauCounterexamples.eikonalIter_spec line 758
  87. theorem OAI.YauCounterexamples.eikonalResidual_coeffContinuous line 794
  88. theorem OAI.YauCounterexamples.eikonalIter_coeffContinuous line 805
  89. theorem OAI.YauCounterexamples.vanishing_jet_norm_bound line 836
  90. theorem OAI.YauCounterexamples.vanishing_jet_local_bound line 871
  91. theorem OAI.YauCounterexamples.realPolyEval_at_zero line 906
  92. theorem OAI.YauCounterexamples.realTaylorPolynomial_constant line 910
  93. theorem OAI.YauCounterexamples.realTaylorPolynomial_linear line 917
  94. theorem OAI.YauCounterexamples.realTaylorPolynomial_remainder line 926
  95. theorem OAI.YauCounterexamples.VanishTo.realPolyEval line 936
  96. def OAI.YauCounterexamples.smoothEikonalResidual line 942
  97. theorem OAI.YauCounterexamples.contDiff_smoothEikonalResidual line 947
  98. theorem OAI.YauCounterexamples.smoothEikonalResidual_jet line 957
  99. theorem OAI.YauCounterexamples.smooth_finite_eikonal line 993
  100. def OAI.YauCounterexamples.smoothWaveTransport line 1026
  101. theorem OAI.YauCounterexamples.contDiff_smoothWaveTransport line 1031
  102. theorem OAI.YauCounterexamples.smoothWaveTransport_jet line 1038
  103. theorem OAI.YauCounterexamples.smooth_finite_transport line 1078
  104. def OAI.YauCounterexamples.boundedDegreeMonomials line 1124
  105. theorem OAI.YauCounterexamples.bounded_degree_expansion line 1127
  106. theorem OAI.YauCounterexamples.realPolyEval_bounded_degree line 1138
  107. theorem OAI.YauCounterexamples.continuous_polynomial_jets line 1149
  108. theorem OAI.YauCounterexamples.compact_uniform_polynomial_jets line 1168