OAI/Analysis/SegmentLenses/HeadRanges.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite-head ranges, dimensions, and outside-head density

  1. theorem OAI.SegmentLenses.primalHead_range line 22
  2. theorem OAI.SegmentLenses.dualHead_range line 41
  3. theorem OAI.SegmentLenses.primalHead_finiteDimensional line 59
  4. theorem OAI.SegmentLenses.dualHead_finiteDimensional line 64
  5. theorem OAI.SegmentLenses.predualHead_finiteDimensional line 82
  6. theorem OAI.SegmentLenses.predual_kernel_finite_approx line 101
  7. theorem OAI.SegmentLenses.exists_test_of_primalHead_eq line 142