OAI/Geometry/SmoothYau/Smoothness/PolynomialFiniteWave.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.smoothPolynomialLaplacian line 37
  2. lemma OAI.YauCounterexamples.contDiff_smoothPolynomialLaplacian line 43
  3. lemma OAI.YauCounterexamples.waveDeriv_realPolyEval_single line 51
  4. lemma OAI.YauCounterexamples.smoothPolynomialLaplacian_eq_operator line 56
  5. def OAI.YauCounterexamples.smoothPhaseTransportVector line 64
  6. def OAI.YauCounterexamples.smoothPhaseTransportScalar line 68
  7. lemma OAI.YauCounterexamples.contDiff_smoothPhaseTransportVector line 73
  8. lemma OAI.YauCounterexamples.contDiff_smoothPhaseTransportScalar line 79
  9. lemma OAI.YauCounterexamples.smoothPhaseTransportVector_zero line 85
  10. lemma OAI.YauCounterexamples.sum_transport_product line 95
  11. lemma OAI.YauCounterexamples.smoothWaveTransport_eq_finite line 107
  12. def OAI.YauCounterexamples.smoothTransportPolynomial line 118
  13. lemma OAI.YauCounterexamples.smoothTransportPolynomial_spec line 123
  14. def OAI.YauCounterexamples.smoothPhasePolynomial line 143
  15. lemma OAI.YauCounterexamples.smoothPhasePolynomial_spec line 148
  16. def OAI.YauCounterexamples.smoothWaveAmplitudes line 177
  17. lemma OAI.YauCounterexamples.smoothWaveAmplitudes_zero_spec line 187
  18. lemma OAI.YauCounterexamples.smoothWaveAmplitudes_succ_spec line 205
  19. lemma OAI.YauCounterexamples.smoothWaveAmplitudes_spec line 225
  20. lemma OAI.YauCounterexamples.CoeffContinuous.C line 292
  21. lemma OAI.YauCounterexamples.multilinearPolynomial_coeffContinuous line 300
  22. lemma OAI.YauCounterexamples.realTaylorPolynomial_coeffContinuous line 309
  23. def OAI.YauCounterexamples.formalPolynomialLaplacian line 317
  24. def OAI.YauCounterexamples.formalPhaseTransportVector line 321
  25. def OAI.YauCounterexamples.formalPhaseTransportScalar line 325
  26. lemma OAI.YauCounterexamples.formalPolynomialLaplacian_coeffContinuous line 330
  27. lemma OAI.YauCounterexamples.formalPhaseTransportVector_coeffContinuous line 341
  28. lemma OAI.YauCounterexamples.formalPhaseTransportVector_constant line 348
  29. lemma OAI.YauCounterexamples.smoothPolynomialLaplacian_approx line 358
  30. lemma OAI.YauCounterexamples.smoothPhaseTransportVector_approx line 396
  31. lemma OAI.YauCounterexamples.smoothWaveTransport_jet_approx line 424
  32. def OAI.YauCounterexamples.symbolWaveAmplitudes line 460
  33. lemma OAI.YauCounterexamples.symbolWaveAmplitudes_spec line 467
  34. lemma OAI.YauCounterexamples.symbolWaveAmplitudes_coeffContinuous line 495
  35. lemma OAI.YauCounterexamples.symbolWaveAmplitudes_genuine line 511
  36. def OAI.YauCounterexamples.uniformSmoothWaveAmplitudes line 559
  37. lemma OAI.YauCounterexamples.uniformSmoothWaveAmplitudes_genuine line 564
  38. lemma OAI.YauCounterexamples.wavePhaseSeed_coeffContinuous line 589
  39. lemma OAI.YauCounterexamples.smoothPhasePolynomial_coeffContinuous line 600
  40. lemma OAI.YauCounterexamples.uniformSmoothWaveAmplitudes_coeffContinuous line 610
  41. lemma OAI.YauCounterexamples.wavePhaseSeed_degree line 622
  42. lemma OAI.YauCounterexamples.smoothPhasePolynomial_degree line 643
  43. def OAI.YauCounterexamples.polynomialFiniteWave line 684
  44. def OAI.YauCounterexamples.polynomialWaveRemainder line 689
  45. lemma OAI.YauCounterexamples.contDiff_polynomialWaveRemainder line 698
  46. lemma OAI.YauCounterexamples.smoothEikonalResidual_eq_gradientPair line 710
  47. lemma OAI.YauCounterexamples.polynomial_wave_residual_expansion line 717
  48. lemma OAI.YauCounterexamples.generated_wave_remainders_vanish line 750