OAI/Geometry/QuadricBundles/Noncollapse.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuadricCounterexample.norm_matrix_pair_le line 12
2. lemma OAI.QuadricCounterexample.quadraticValue_sub_bound line 30
3. theorem OAI.QuadricCounterexample.quadraticValue_moving_vector line 50
4. lemma OAI.QuadricCounterexample.nonnegative_usc_integrableOn_ball line 68
5. theorem OAI.QuadricCounterexample.moving_points_force_nonzero_limit line 87
6. lemma OAI.QuadricCounterexample.ExtractedTrace.averages_globalValue line 131
7. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_nonzero_of_sequence line 150
8. theorem OAI.QuadricCounterexample.ExtractedTrace.globalValue_nonzero line 190
9. def OAI.QuadricCounterexample.ExtractedTrace.pshDualForm line 232
10. theorem OAI.QuadricCounterexample.no_unbounded_positive_metrics line 240
11. theorem OAI.QuadricCounterexample.source_eventually_no_positive_metric line 252