OAI/Geometry/QuadricBundles/DualForms.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuadricCounterexample.affineP1_one line 13
2. lemma OAI.QuadricCounterexample.projective_usc_of_affine_usc line 16
3. theorem OAI.QuadricCounterexample.projective_subharmonic_const line 34
4. structure OAI.QuadricCounterexample.EqualizerData.PshDualForm line 63
5. lemma OAI.QuadricCounterexample.coordinateOverlap_of_affine_eq line 71
6. lemma OAI.QuadricCounterexample.coordinateChange_of_affine_eq line 76
7. lemma OAI.QuadricCounterexample.exists_projective_gluing line 80
8. def OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstNorm line 90
9. def OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondNorm line 92
10. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstNorm_change line 95
11. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondNorm_change line 102
12. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstNorm_same_ruling line 120
13. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondNorm_same_ruling line 128
14. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.nonneg line 136
15. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.scalar line 142
16. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstNorm_psh line 151
17. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondNorm_psh line 158
18. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstNorm_ruling_const line 169
19. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondNorm_ruling_const line 180
20. structure OAI.QuadricCounterexample.PshLine24 line 193
21. def OAI.QuadricCounterexample.otherIndex line 201
22. def OAI.QuadricCounterexample.homogeneousCoordinate line 203
23. lemma OAI.QuadricCounterexample.homogeneousCoordinate_smul line 206
24. lemma OAI.QuadricCounterexample.homogeneousRepresentative line 211
25. lemma OAI.QuadricCounterexample.homogeneousCoordinate_overlap line 217
26. lemma OAI.QuadricCounterexample.homogeneousCoordinate_change line 222
27. lemma OAI.QuadricCounterexample.homogeneousCoordinate_factor line 228
28. lemma OAI.QuadricCounterexample.PshLine24.zero line 237
29. lemma OAI.QuadricCounterexample.PshLine24.coordinate_independent line 240
30. def OAI.QuadricCounterexample.PshLine24.homogeneousNorm line 247
31. lemma OAI.QuadricCounterexample.PshLine24.homogeneousNorm_chart line 251
32. lemma OAI.QuadricCounterexample.PshLine24.homogeneousNorm_zero line 261
33. lemma OAI.QuadricCounterexample.PshLine24.homogeneousNorm_nonneg line 264
34. lemma OAI.QuadricCounterexample.PshLine24.homogeneousNorm_scalar line 268
35. lemma OAI.QuadricCounterexample.PshLine24.value_weighted_chart line 280
36. lemma OAI.QuadricCounterexample.PshLine24.weightedChart_differentiableAt line 284
37. lemma OAI.QuadricCounterexample.PshLine24.weightedNorm_usc line 293
38. lemma OAI.QuadricCounterexample.PshLine24.homogeneousNorm_usc line 310
39. lemma OAI.QuadricCounterexample.PshLine24.homogeneousNorm_disk line 316
40. lemma OAI.QuadricCounterexample.PshLine24.homogeneousMetric line 352
41. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstNorm_scalar line 366
42. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondNorm_scalar line 374
43. def OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstLine line 382
44. def OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondLine line 393
45. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.firstLine_value line 404
46. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.secondLine_value line 408
47. lemma OAI.QuadricCounterexample.matrixBranchDenominator_homogeneous line 414
48. lemma OAI.QuadricCounterexample.matrixGraphValue_homogeneous line 422
49. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.graph_identifies_homogeneous line 436
50. lemma OAI.QuadricCounterexample.source_matrices_zero line 470
51. lemma OAI.QuadricCounterexample.source_matrices_one line 471
52. lemma OAI.QuadricCounterexample.source_matrices_two line 472
53. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.source_lines_identical line 477
54. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.source_first_homogeneous_zero line 483
55. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.source_second_homogeneous_zero line 502
56. lemma OAI.QuadricCounterexample.homogeneousCoordinate_affineRepresentative line 508
57. lemma OAI.QuadricCounterexample.PshLine24.value_zero_of_homogeneous_zero line 512
58. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.source_firstNorm_zero line 524
59. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.source_secondNorm_zero line 529
60. lemma OAI.QuadricCounterexample.EqualizerData.PshDualForm.source_value_zero_off_divisor line 534
61. lemma OAI.QuadricCounterexample.DiskPshOn.eq_zero_of_off_polynomial line 562
62. theorem OAI.QuadricCounterexample.EqualizerData.PshDualForm.source_value_zero line 598