OAI/Geometry/SmoothYau/Estimates/GeneratedCutoffWaveEndpointRatio.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.normalize_vector_error line 16
  2. lemma OAI.YauCounterexamples.norm_normalize_vector line 34
  3. def OAI.YauCounterexamples.complexValueVector line 42
  4. lemma OAI.YauCounterexamples.complexValueVector_inner line 45
  5. lemma OAI.YauCounterexamples.complexValueVector_norm_sq line 53
  6. lemma OAI.YauCounterexamples.complexValueVector_sub line 63
  7. lemma OAI.YauCounterexamples.complexValueVector_real_smul line 69
  8. lemma OAI.YauCounterexamples.complexValueVector_nonzero line 75
  9. def OAI.YauCounterexamples.rotatedWaveValues line 85
  10. lemma OAI.YauCounterexamples.complexValueVector_rotated_norm line 88
  11. lemma OAI.YauCounterexamples.complexValueVector_rotated_inner line 96
  12. lemma OAI.YauCounterexamples.exponential_packet_relative_error line 119
  13. lemma OAI.YauCounterexamples.exponential_wave_ratio_bound line 152
  14. lemma OAI.YauCounterexamples.complexValueVector_relative_error line 168
  15. theorem OAI.YauCounterexamples.finite_wave_endpoint_ratio line 189
  16. theorem OAI.YauCounterexamples.generated_cutoff_wave_endpoint_ratio line 245