OAI/Geometry/SmoothYau/Smoothness/ComplexPolarWeight.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.smoothFiniteWave_cutoff_germ_at line 44
  2. theorem OAI.YauCounterexamples.generated_cutoff_waves_near_center line 51
  3. def OAI.YauCounterexamples.phaseFrameMatrix line 151
  4. lemma OAI.YauCounterexamples.phaseFrameMatrix_gram line 154
  5. lemma OAI.YauCounterexamples.phaseFrameMatrix_det_sq line 164
  6. def OAI.YauCounterexamples.physicalWaveJetMatrix line 172
  7. lemma OAI.YauCounterexamples.physicalWaveJetMatrix_det line 177
  8. lemma OAI.YauCounterexamples.phaseFrameMatrix_det_lower line 183
  9. lemma OAI.YauCounterexamples.physicalWaveJetMatrix_det_lower line 197
  10. lemma OAI.YauCounterexamples.physicalWaveJetMatrix_bound line 206
  11. theorem OAI.YauCounterexamples.physical_wave_smallBall_uniform line 229
  12. def OAI.YauCounterexamples.complexWaveJet line 307
  13. def OAI.YauCounterexamples.leadingComplexJet line 312
  14. def OAI.YauCounterexamples.selectedComplexJetMatrix line 315
  15. lemma OAI.YauCounterexamples.selectedComplexJetMatrix_leading line 320
  16. lemma OAI.YauCounterexamples.selectedComplexJetMatrix_error line 333
  17. lemma OAI.YauCounterexamples.complexWaveJet_error line 353
  18. theorem OAI.YauCounterexamples.generated_selected_columns_near_center line 364
  19. lemma OAI.YauCounterexamples.complex_polar_weight line 447
  20. lemma OAI.YauCounterexamples.complexWaveJet_factor line 454
  21. lemma OAI.YauCounterexamples.phase_weight_lower line 472