OAI/Geometry/SmoothYau/Spectrum/FiniteWaveAmplitude.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.finiteWaveAmplitude line 42
  2. lemma OAI.YauCounterexamples.contDiff_finiteWaveAmplitude line 45
  3. lemma OAI.YauCounterexamples.finiteWaveAmplitude_zero line 50
  4. lemma OAI.YauCounterexamples.norm_inv_frequency_pow line 54
  5. theorem OAI.YauCounterexamples.finite_amplitude_near_center line 59
  6. theorem OAI.YauCounterexamples.phase_derivative_near_center line 108
  7. lemma OAI.YauCounterexamples.smoothFiniteWave_normalized_value line 137
  8. lemma OAI.YauCounterexamples.smoothFiniteWave_normalized_derivative line 144
  9. theorem OAI.YauCounterexamples.finite_wave_near_center line 159