BalancedSchedule.lean`

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.BalancedSchedule.chunkLength line 13
Source documentation
Number of U layers following the ith V layer.
```
def chunkLength (k s i : ℕ) : ℕ :=
…
```
lemma OAI.Problem335.BalancedSchedule.quotient_mono line 16
lemma OAI.Problem335.BalancedSchedule.chunkLength_pos line 20
lemma OAI.Problem335.BalancedSchedule.chunkLength_le_two line 24
lemma OAI.Problem335.BalancedSchedule.chunkLength_eq_one_or_two line 35
lemma OAI.Problem335.BalancedSchedule.sum_chunkLength line 42
Source documentation
The number of U layers in consecutive complete chunks.
```
lemma sum_chunkLength (k s a r : ℕ) :
    (∑ j ∈ Finset.range r, chunkLength k s (a + j)) =
      r + ((a + r) * s / k - a * s / k) := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.chunkLength
lemma OAI.Problem335.BalancedSchedule.sum_all_chunkLength line 56
lemma OAI.Problem335.BalancedSchedule.complete_chunks_discrepancy_lt line 61
Source documentation
A complete-chunk block has discrepancy strictly less than ρ = k / (k+s).
```
lemma complete_chunks_discrepancy_lt {k : ℕ} (hk : 0 < k) (s a r : ℕ) :
    (r : ℝ) - (k : ℝ) / (k + s) *
      (∑ j ∈ Finset.range r, (chunkLength k s (a + j) : ℝ)) <
      (k : ℝ) / (k + s) := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.chunkLength
def OAI.Problem335.BalancedSchedule.rho line 89
Source documentation
The relative density used in the mixed rank measure.
```
def rho (k s : ℕ) : ℝ := (k : ℝ) / (k + s)
```
def OAI.Problem335.BalancedSchedule.chunk line 92
Source documentation
true denotes a V layer and false denotes a U layer.
```
def chunk (k s i : ℕ) : List Bool :=
…
```
def OAI.Problem335.BalancedSchedule.wordPrefix line 96
Source documentation
The first r complete chunks of the balanced schedule.
```
def wordPrefix (k s : ℕ) : ℕ → List Bool
  | 0 => []
  | r + 1 => wordPrefix k s r ++ chunk k s r

/-- The complete balanced layer schedule. -/
```
Mentions: OAI.Problem335.BalancedSchedule.chunk
def OAI.Problem335.BalancedSchedule.word line 101
Source documentation
The complete balanced layer schedule.
```
def word (k s : ℕ) : List Bool := wordPrefix k s k
```
Mentions: OAI.Problem335.BalancedSchedule.wordPrefix
def OAI.Problem335.BalancedSchedule.discrepancy line 104
Source documentation
The number of V layers minus ρ times the number of U layers.
```
def discrepancy (k s : ℕ) (w : List Bool) : ℝ :=
…
```
lemma OAI.Problem335.BalancedSchedule.count_true_chunk line 107
lemma OAI.Problem335.BalancedSchedule.count_false_chunk line 110
lemma OAI.Problem335.BalancedSchedule.count_true_wordPrefix line 114
lemma OAI.Problem335.BalancedSchedule.count_false_wordPrefix line 120
lemma OAI.Problem335.BalancedSchedule.discrepancy_nil line 130
lemma OAI.Problem335.BalancedSchedule.discrepancy_append line 133
lemma OAI.Problem335.BalancedSchedule.discrepancy_chunk line 138
lemma OAI.Problem335.BalancedSchedule.discrepancy_wordPrefix_eq_mod line 142
lemma OAI.Problem335.BalancedSchedule.discrepancy_wordPrefix_nonneg line 154
lemma OAI.Problem335.BalancedSchedule.discrepancy_wordPrefix_lt_rho line 159
lemma OAI.Problem335.BalancedSchedule.take_chunk_discrepancy line 167
lemma OAI.Problem335.BalancedSchedule.take_wordPrefix_discrepancy_bounds line 173
Source documentation
Every prefix of the balanced schedule stays in a strip of width 1+ρ.
```
lemma take_wordPrefix_discrepancy_bounds {k : ℕ} (hk : 0 < k) (s r p : ℕ) :
    0 ≤ discrepancy k s ((wordPrefix k s r).take p) ∧
      discrepancy k s ((wordPrefix k s r).take p) < 1 + rho k s := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.discrepancy, OAI.Problem335.BalancedSchedule.wordPrefix, OAI.Problem335.BalancedSchedule.rho
lemma OAI.Problem335.BalancedSchedule.interval_discrepancy_lt line 198
Source documentation
Every interval of layers has discrepancy strictly less than 1+ρ.
```
lemma interval_discrepancy_lt {k : ℕ} (hk : 0 < k) (s r a len : ℕ) :
    discrepancy k s (((wordPrefix k s r).drop a).take len) < 1 + rho k s := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.discrepancy, OAI.Problem335.BalancedSchedule.wordPrefix, OAI.Problem335.BalancedSchedule.rho
lemma OAI.Problem335.BalancedSchedule.infix_discrepancy_lt line 205
lemma OAI.Problem335.BalancedSchedule.word_count_true line 212
lemma OAI.Problem335.BalancedSchedule.word_count_false line 215
lemma OAI.Problem335.BalancedSchedule.word_length line 219
lemma OAI.Problem335.BalancedSchedule.discrepancy_word line 224
lemma OAI.Problem335.BalancedSchedule.chunk_head line 229
lemma OAI.Problem335.BalancedSchedule.chunk_last line 231
lemma OAI.Problem335.BalancedSchedule.wordPrefix_head line 235
lemma OAI.Problem335.BalancedSchedule.wordPrefix_last line 247
lemma OAI.Problem335.BalancedSchedule.replicate_no_adjacent_V line 253
lemma OAI.Problem335.BalancedSchedule.chunk_no_adjacent_V line 258
lemma OAI.Problem335.BalancedSchedule.wordPrefix_no_adjacent_V line 269
Source documentation
No two V layers are adjacent, a key independence property of the schedule.
```
lemma wordPrefix_no_adjacent_V (k s r : ℕ) :
    (wordPrefix k s r).IsChain (fun a b => a = false ∨ b = false) := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.wordPrefix
lemma OAI.Problem335.BalancedSchedule.word_no_adjacent_V line 284
def OAI.Problem335.BalancedSchedule.indexedWord line 289
Source documentation
Finite-indexed form of the balanced layer partition.
```
def indexedWord {k : ℕ} (hk : 0 < k) (s : ℕ) : Fin (2 * k + s) → Bool :=
…
```
def OAI.Problem335.BalancedSchedule.vLayers line 293
Source documentation
The finite set of the V layers.
```
def vLayers {k : ℕ} (hk : 0 < k) (s : ℕ) : Finset (Fin (2 * k + s)) :=
…
```
def OAI.Problem335.BalancedSchedule.uLayers line 297
Source documentation
The finite set of the U layers.
```
def uLayers {k : ℕ} (hk : 0 < k) (s : ℕ) : Finset (Fin (2 * k + s)) :=
…
```
lemma OAI.Problem335.BalancedSchedule.card_vLayers line 300
lemma OAI.Problem335.BalancedSchedule.card_uLayers line 306
lemma OAI.Problem335.BalancedSchedule.layer_partition line 312
lemma OAI.Problem335.BalancedSchedule.layer_disjoint line 319
lemma OAI.Problem335.BalancedSchedule.indexedWord_no_adjacent_V line 327
def OAI.Problem335.BalancedSchedule.adjacent line 337
Source documentation
Adjacent layer positions in either order.
```
def adjacent {n : ℕ} (i j : Fin n) : Prop := i.val + 1 = j.val ∨ j.val + 1 = i.val
```
lemma OAI.Problem335.BalancedSchedule.vLayers_independent line 339
def OAI.Problem335.BalancedSchedule.internalEnds line 352
Source documentation
Internal vertices adjacent to a layer. Vertex j is between layers j and j+1.
```
def internalEnds {n : ℕ} (i : Fin n) : Finset (Fin (n - 1)) :=
…
```
lemma OAI.Problem335.BalancedSchedule.internalEnds_disjoint_of_not_adjacent line 355
lemma OAI.Problem335.BalancedSchedule.vLayers_internalEnds_disjoint line 367
Source documentation
Distinct selected V layers depend on disjoint internal-vertex coordinates.
```
lemma vLayers_internalEnds_disjoint {k : ℕ} (hk : 0 < k) (s : ℕ)
    {i j : Fin (2 * k + s)} (hi : i ∈ vLayers hk s) (hj : j ∈ vLayers hk s)
    (hne : i ≠ j) : Disjoint (internalEnds i) (internalEnds j) := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.vLayers, OAI.Problem335.BalancedSchedule.internalEnds
lemma OAI.Problem335.BalancedSchedule.mem_internalEnds_left line 374
Source documentation
The left end of an interior layer is an internal vertex.
```
lemma mem_internalEnds_left {n : ℕ} (i : Fin n) (hi : 0 < i.val) :
    (⟨i.val - 1, by omega⟩ : Fin (n - 1)) ∈ internalEnds i := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.internalEnds
lemma OAI.Problem335.BalancedSchedule.mem_internalEnds_right line 381
Source documentation
The right end of a nonfinal layer is an internal vertex.
```
lemma mem_internalEnds_right {n : ℕ} (i : Fin n) (hi : i.val + 1 < n) :
    (⟨i.val, by omega⟩ : Fin (n - 1)) ∈ internalEnds i := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.internalEnds
lemma OAI.Problem335.BalancedSchedule.card_internalEnds_le_two line 385