OAI/Geometry/SmoothYau/Estimates/PhaseFormMatrix.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.continuous_quadratic_coercive line 35
  2. def OAI.YauCounterexamples.realQuadratic line 76
  3. def OAI.YauCounterexamples.squareSum line 79
  4. lemma OAI.YauCounterexamples.realQuadratic_hom line 81
  5. lemma OAI.YauCounterexamples.matrix_positive_coercive line 90
  6. lemma OAI.YauCounterexamples.squareSum_nonneg line 115
  7. lemma OAI.YauCounterexamples.abs_mul_le_squareSum line 118
  8. lemma OAI.YauCounterexamples.realQuadratic_abs_bound line 126
  9. lemma OAI.YauCounterexamples.realQuadratic_add line 142
  10. lemma OAI.YauCounterexamples.realQuadratic_sub line 145
  11. lemma OAI.YauCounterexamples.continuous_matrix_lower_near line 149
  12. def OAI.YauCounterexamples.phaseProjection line 202
  13. def OAI.YauCounterexamples.continuedPhaseMatrix line 205
  14. lemma OAI.YauCounterexamples.phaseProjection_transpose line 209
  15. lemma OAI.YauCounterexamples.phaseProjection_annihilates line 213
  16. lemma OAI.YauCounterexamples.continuedPhaseMatrix_transpose line 217
  17. lemma OAI.YauCounterexamples.continuedPhaseMatrix_annihilates line 222
  18. lemma OAI.YauCounterexamples.continuedPhaseMatrix_eq line 228
  19. lemma OAI.YauCounterexamples.continuous_phaseProjection line 238
  20. lemma OAI.YauCounterexamples.continuous_continuedPhaseMatrix line 246
  21. lemma OAI.YauCounterexamples.strict_real_quadratic_coercive line 252
  22. lemma OAI.YauCounterexamples.continuous_real_quadratic_coercive_near line 272
  23. theorem OAI.YauCounterexamples.phase_matrix_continuation line 290
  24. def OAI.YauCounterexamples.phaseFormMatrix line 364
  25. def OAI.YauCounterexamples.complexPhaseVector line 367
  26. def OAI.YauCounterexamples.complexPhaseMatrix line 370
  27. lemma OAI.YauCounterexamples.phaseFormMatrix_mulVec line 374
  28. lemma OAI.YauCounterexamples.realQuadratic_phaseFormMatrix line 385
  29. lemma OAI.YauCounterexamples.complexPhaseMatrix_re line 406
  30. lemma OAI.YauCounterexamples.complexPhaseMatrix_transpose line 412
  31. lemma OAI.YauCounterexamples.complexPhaseMatrix_annihilates line 421
  32. lemma OAI.YauCounterexamples.complexPhaseVector_square line 448
  33. theorem OAI.YauCounterexamples.actual_complex_phase_matrix line 472