OAI/Geometry/SmoothYau/Estimates/RealPhaseLinear.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.PhaseSpace line 34
  2. abbrev OAI.YauCounterexamples.ComplexPhaseMatrix line 35
  3. def OAI.YauCounterexamples.shiftedPhaseImag line 37
  4. def OAI.YauCounterexamples.transverseAngleSq line 40
  5. def OAI.YauCounterexamples.PhaseMatrixValid line 43
  6. def OAI.YauCounterexamples.ThreePhaseData line 48
  7. lemma OAI.YauCounterexamples.PhaseMatrixValid.mono line 58
  8. lemma OAI.YauCounterexamples.ThreePhaseData.mono line 65
  9. lemma OAI.YauCounterexamples.squareSum_pos line 73
  10. lemma OAI.YauCounterexamples.complexPhaseVector_continuousAt line 84
  11. lemma OAI.YauCounterexamples.aligned_phase_square line 95
  12. lemma OAI.YauCounterexamples.shiftedPhaseImag_zero line 102
  13. lemma OAI.YauCounterexamples.shiftedPhaseImag_eq_normalized line 106
  14. lemma OAI.YauCounterexamples.shifted_phase_square line 115
  15. lemma OAI.YauCounterexamples.real_phase_linear line 160
  16. lemma OAI.YauCounterexamples.real_phase_quadratic line 167
  17. lemma OAI.YauCounterexamples.phase_squareSum line 181
  18. lemma OAI.YauCounterexamples.phase_linear_perturbation line 185
  19. lemma OAI.YauCounterexamples.phase_matrix_gaussian_gap line 194
  20. lemma OAI.YauCounterexamples.phase_vector_ne_zero line 204
  21. lemma OAI.YauCounterexamples.phase_matrix_annihilation line 208