OAI/Combinatorics/Sensitivity/RecursiveDefinitions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Paper320.recursiveChild line 13
2. def OAI.Paper320.gateIndex line 17
3. theorem OAI.Paper320.gateIndex_lt_last line 19
4. theorem OAI.Paper320.gateIndex_antitone line 22
5. theorem OAI.Paper320.gateIndex_strictAnti line 26
6. def OAI.Paper320.rowClause line 31

   Source documentation

   A clause uses every target in its own row and one labeled gate per outgoing edge.

   def rowClause {k r h : ℕ} {I : Type} (T : Tournament k)
       (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool)
       (q : Fin h) (x : ((Fin k × Fin r) × I) → Bool) (i : Fin k) : Bool :=
   …

   Mentions: OAI.Paper320.Tournament

7. def OAI.Paper320.recursiveFamily line 38

   Source documentation

   The next-level predicate is the disjunction of the literal row clauses.

   def recursiveFamily {k r h : ℕ} {I : Type} (T : Tournament k)
       (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool)
       (q : Fin h) (x : ((Fin k × Fin r) × I) → Bool) : Bool :=
   …

   Mentions: OAI.Paper320.Tournament

8. theorem OAI.Paper320.rowClause_eq_true_iff line 43
9. theorem OAI.Paper320.recursiveFamily_eq_true_iff line 51
10. theorem OAI.Paper320.recursiveFamily_eq_false_iff line 57
11. theorem OAI.Paper320.rowClause_nested line 63
12. theorem OAI.Paper320.recursiveFamily_nested line 72
13. theorem OAI.Paper320.recursiveFamily_zero line 81
14. theorem OAI.Paper320.recursive_coordinates_card line 95