OAI/Geometry/QuadricBundles/HomogeneousClassification.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuadricCounterexample.invariant_mul_zpow line 15
2. lemma OAI.QuadricCounterexample.exists_rescale_mem_annulus line 34
3. lemma OAI.QuadricCounterexample.complex_punctured_preconnected line 45
4. theorem OAI.QuadricCounterexample.LocalDiskSubmeanOn.eq_const_of_dilation line 57
5. structure OAI.QuadricCounterexample.HomogeneousLocalPshMetric24 line 90
6. lemma OAI.QuadricCounterexample.HomogeneousLocalPshMetric24.zero line 98
7. lemma OAI.QuadricCounterexample.HomogeneousLocalPshMetric24.normalized_subharmonic line 102
8. theorem OAI.QuadricCounterexample.HomogeneousLocalPshMetric24.hyperbolic_classification line 124
9. lemma OAI.QuadricCounterexample.HomogeneousLocalPshMetric24.pullback line 201
10. lemma OAI.QuadricCounterexample.metric_zero_pair_preserved line 226
11. lemma OAI.QuadricCounterexample.conjugate_pair_contradiction line 254
12. lemma OAI.QuadricCounterexample.local_homogeneous_metric_zero_of_diagonal_product line 285
13. lemma OAI.QuadricCounterexample.source_expanding_gt_one line 313
14. lemma OAI.QuadricCounterexample.source_eigenbasis_diagonalizes_inv line 319
15. lemma OAI.QuadricCounterexample.source_eigenbasis_diagonal_action line 342
16. theorem OAI.QuadricCounterexample.source_invariant_local_homogeneous_metric_zero line 355