OAI/Geometry/SmoothYau/Spectrum/ContinuousRealQuadraticCoerciveNear.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.continuousAt_real_quadratic_coercive_near line 37
2. theorem OAI.YauCounterexamples.phase_matrix_continuation_at line 62
3. def OAI.YauCounterexamples.transverseProjection line 107
4. def OAI.YauCounterexamples.normalizedTransverse line 109
5. lemma OAI.YauCounterexamples.transverseProjection_eq line 112
6. lemma OAI.YauCounterexamples.transverseProjection_orthogonal line 115
7. lemma OAI.YauCounterexamples.continuous_transverseProjection line 120
8. lemma OAI.YauCounterexamples.normalizedTransverse_eq line 125
9. lemma OAI.YauCounterexamples.normalizedTransverse_orthogonal line 131
10. lemma OAI.YauCounterexamples.normalizedTransverse_norm_sq line 135
11. lemma OAI.YauCounterexamples.continuousAt_normalizedTransverse line 142