OAI/Geometry/QuadricBundles/PointwiseRepresentative.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuadricCounterexample.upperSemicontinuousOn_aestronglyMeasurable line 16
2. lemma OAI.QuadricCounterexample.DiskPshOn.le_of_ae line 24
3. lemma OAI.QuadricCounterexample.DiskPshOn.eqOn_of_ae line 64
4. lemma OAI.QuadricCounterexample.UpperSemicontinuousOn.integrableOn_compact_nonneg line 81
5. lemma OAI.QuadricCounterexample.DiskPshOn.integrableOn_ball_nonneg line 95
6. lemma OAI.QuadricCounterexample.DiskPshOn.le_of_averages line 101
7. lemma OAI.QuadricCounterexample.DiskPshOn.eqOn_of_averages line 133
8. def OAI.QuadricCounterexample.ExtractedTrace.value line 146
9. lemma OAI.QuadricCounterexample.ExtractedTrace.base_psh line 148
10. lemma OAI.QuadricCounterexample.ExtractedTrace.value_nonneg line 151
11. lemma OAI.QuadricCounterexample.ExtractedTrace.exhaustion_value_eq line 154
12. def OAI.QuadricCounterexample.traceLevel line 185
13. lemma OAI.QuadricCounterexample.mem_traceInterior_level line 186
14. def OAI.QuadricCounterexample.ExtractedTrace.globalMatrix line 197
15. def OAI.QuadricCounterexample.ExtractedTrace.globalValue line 199
16. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_eq_value line 201
17. lemma OAI.QuadricCounterexample.ExtractedTrace.globalMatrix_positive line 205
18. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_nonneg line 207
19. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_upperSemicontinuous line 210
20. lemma OAI.QuadricCounterexample.ExtractedTrace.exists_traceInterior_of_compact line 224
21. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_psh line 234