OAI/Geometry/QuadricBundles/TraceExtraction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuadricCounterexample.TraceIndex line 14
  2. abbrev OAI.QuadricCounterexample.CoefficientSpace line 15
  3. abbrev OAI.QuadricCounterexample.CoefficientL2 line 16
  4. def OAI.QuadricCounterexample.traceInterior line 17
  5. def OAI.QuadricCounterexample.traceDomain line 18
  6. def OAI.QuadricCounterexample.traceSupport line 19
  7. def OAI.QuadricCounterexample.traceBound line 20
  8. lemma OAI.QuadricCounterexample.traceBound_nonneg line 22
  9. lemma OAI.QuadricCounterexample.traceBound_spec line 24
  10. def OAI.QuadricCounterexample.cutoffTrace line 31
  11. lemma OAI.QuadricCounterexample.cutoffTrace_eq line 34
  12. lemma OAI.QuadricCounterexample.traceDomain_subset_support line 37
  13. lemma OAI.QuadricCounterexample.traceInterior_subset_domain line 39
  14. structure OAI.QuadricCounterexample.ExtractedTrace line 42
  15. lemma OAI.QuadricCounterexample.exists_extractedTrace line 61