OAI/Algebra/DepthFive/LowerSchedule.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.LowerParameters.balancedWord line 12

   Source documentation

   The actual balanced schedule for the rank-measure parameters of degree n.

   def balancedWord (n : ℕ) : List Bool := BalancedSchedule.word (k n) (s n)

   Mentions: OAI.Problem335.BalancedSchedule.word, OAI.Problem335.LowerParameters.k, OAI.Problem335.LowerParameters.s

2. lemma OAI.Problem335.LowerParameters.balancedWord_length line 14
3. def OAI.Problem335.LowerParameters.balancedLayer line 18

   Source documentation

   true selects derivative layers and false selects multiplication layers.

   def balancedLayer {n : ℕ} (hn : 4 ≤ n) : Fin n → Bool := fun i =>
   …

4. lemma OAI.Problem335.LowerParameters.balancedLayer_ofFn line 21
5. lemma OAI.Problem335.LowerParameters.balancedLayer_card_true line 28
6. lemma OAI.Problem335.LowerParameters.balancedLayer_card_false line 36
7. lemma OAI.Problem335.LowerParameters.balancedSchedule_rho line 44
8. lemma OAI.Problem335.LowerParameters.balancedLayer_infix_discrepancy line 47
9. lemma OAI.Problem335.LowerParameters.balancedLayer_no_adjacent line 60
10. lemma OAI.Problem335.LowerParameters.balancedLayer_independent line 70
11. lemma OAI.Problem335.LowerParameters.balancedLayer_first line 79
12. lemma OAI.Problem335.LowerParameters.balancedLayer_final line 87
13. lemma OAI.Problem335.LowerParameters.balancedLayer_internalEnds_disjoint line 97

    Source documentation

    The actual V-layer coincidence events use pairwise disjoint vertex coordinates.

    lemma balancedLayer_internalEnds_disjoint {n : ℕ} (hn : 4 ≤ n) {i j : Fin n}
        (hi : balancedLayer hn i = true) (hj : balancedLayer hn j = true) (hne : i ≠ j) :
        Disjoint (BalancedSchedule.internalEnds i) (BalancedSchedule.internalEnds j) :=
    …

    Mentions: OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.BalancedSchedule.internalEnds

14. def OAI.Problem335.LowerParameters.layerVariableEquiv line 103

    Source documentation

    Layer-restricted IMM variables are a product of selected layers and matrix entries.

    def layerVariableEquiv {n : ℕ} (p : Fin n → Bool) (b : Bool) :
        {x : Fin n × Fin n × Fin n // p x.1 = b} ≃
          {i : Fin n // p i = b} × Fin n × Fin n where
    …

    Mentions: OAI.Problem335.LowerParameters.b

15. lemma OAI.Problem335.LowerParameters.balancedVariable_card_true line 111
16. lemma OAI.Problem335.LowerParameters.balancedVariable_card_false line 119