OAI/Analysis/MatrixSigning/Optimization/Lookup.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.RationalFace.lookup line 10
  2. lemma OAI.CurrentKS.RationalFace.lookup_some line 13
  3. lemma OAI.CurrentKS.RationalFace.lookup_none_iff line 18
  4. lemma OAI.CurrentKS.RationalFace.lookup_self line 22
  5. def OAI.CurrentKS.RationalFace.extend line 31
  6. lemma OAI.CurrentKS.RationalFace.extend_at line 34
  7. lemma OAI.CurrentKS.RationalFace.extend_outside line 38
  8. lemma OAI.CurrentKS.RationalFace.extend_self line 43
  9. lemma OAI.CurrentKS.RationalFace.map_extend line 51
  10. def OAI.CurrentKS.RationalFace.activeIndices line 58
  11. def OAI.CurrentKS.RationalFace.activeIndex line 61
  12. lemma OAI.CurrentKS.RationalFace.activeIndices_mem line 64
  13. lemma OAI.CurrentKS.RationalFace.activeIndex_injective line 67
  14. lemma OAI.CurrentKS.RationalFace.activeIndex_range line 70
  15. lemma OAI.CurrentKS.RationalFace.activeIndex_interior line 75
  16. lemma OAI.CurrentKS.RationalFace.activeIndices_length_le line 78
  17. lemma OAI.CurrentKS.RationalFace.extend_cube line 83
  18. lemma OAI.CurrentKS.RationalFace.extended_difference_bound line 91
  19. lemma OAI.CurrentKS.RationalFace.sum_lookup line 102
  20. lemma OAI.CurrentKS.RationalFace.sum_extend line 113
  21. lemma OAI.CurrentKS.RationalFace.real_active_outside_endpoint line 123