OAI/Algebra/DepthFive/ScheduleEnds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.BalancedSchedule.leftLayer line 10

   Source documentation

   The layer immediately left of an internal vertex.

   def leftLayer {n : ℕ} (v : Fin (n - 1)) : Fin n := ⟨v.val, by omega⟩

2. def OAI.Problem335.BalancedSchedule.rightLayer line 13

   Source documentation

   The layer immediately right of an internal vertex.

   def rightLayer {n : ℕ} (v : Fin (n - 1)) : Fin n := ⟨v.val + 1, by omega⟩

3. lemma OAI.Problem335.BalancedSchedule.adjacent_left_right line 15
4. lemma OAI.Problem335.BalancedSchedule.internalEnds_cases line 18
5. def OAI.Problem335.BalancedSchedule.nnInternalEnds line 25

   Source documentation

   Internal ends at which both incident layers have type N (false).

   def nnInternalEnds {n : ℕ} (τ : Fin n → Bool) (i : Fin n) : Finset (Fin (n - 1)) :=
   …

6. lemma OAI.Problem335.BalancedSchedule.nnInternalEnds_subset line 28
7. lemma OAI.Problem335.BalancedSchedule.nnInternalEnds_card_le_two line 31
8. lemma OAI.Problem335.BalancedSchedule.nnInternalEnds_nonempty_iff line 35
9. lemma OAI.Problem335.BalancedSchedule.one_le_nnInternalEnds_card line 64

   Source documentation

   A nonisolated N layer has at least one NN internal end.

   lemma one_le_nnInternalEnds_card {n : ℕ} (τ : Fin n → Bool) (i : Fin n)
       (hi : τ i = false) (hnot : ¬ ∀ j, adjacent i j → τ j = true) :
       1 ≤ (nnInternalEnds τ i).card := by
   …

   Mentions: OAI.Problem335.BalancedSchedule.adjacent, OAI.Problem335.BalancedSchedule.nnInternalEnds

10. lemma OAI.Problem335.BalancedSchedule.nnInternalEnds_eq_empty_of_all_neighbors_D line 73
11. lemma OAI.Problem335.BalancedSchedule.nnInternalEnds_disjoint line 82
12. lemma OAI.Problem335.BalancedSchedule.adjacent_symm line 89
13. lemma OAI.Problem335.BalancedSchedule.nnInternalEnds_congr line 92

    Source documentation

    The coincidence set depends only on the layer and its immediate neighbors.

    lemma nnInternalEnds_congr {n : ℕ} {τ υ : Fin n → Bool} (i : Fin n)
        (hsame : τ i = υ i) (hadj : ∀ j, adjacent i j → τ j = υ j) :
        nnInternalEnds τ i = nnInternalEnds υ i := by
    …

    Mentions: OAI.Problem335.BalancedSchedule.adjacent, OAI.Problem335.BalancedSchedule.nnInternalEnds

14. lemma OAI.Problem335.BalancedSchedule.nnInternalEnds_flip_subset line 115

    Source documentation

    Flipping other V positions cannot change an unflipped V layer's NN ends.

    lemma nnInternalEnds_flip_subset {k : ℕ} (hk : 0 < k) (s : ℕ)
        (τ : Fin (2 * k + s) → Bool) (S : Finset (Fin (2 * k + s)))
        (hS : S ⊆ vLayers hk s) {i : Fin (2 * k + s)}
        (hi : i ∈ vLayers hk s) (hiS : i ∉ S) :
        nnInternalEnds (fun j => if j ∈ S then true else τ j) i = nnInternalEnds τ i := by
    …

    Mentions: OAI.Problem335.BalancedSchedule.vLayers, OAI.Problem335.BalancedSchedule.nnInternalEnds