ScheduleIntervals.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem335.BalancedSchedule.card_get_eq_count line 9

lemma OAI.Problem335.BalancedSchedule.count_slice_eq_card line 14

Source documentation

Counting a contiguous list interval equals counting its finite-indexed layers.

lemma count_slice_eq_card (w : List Bool) (a len : ℕ) (b : Bool) :
    ((w.drop a).take len).count b =
      (Finset.univ.filter (fun i : Fin w.length =>
        a ≤ i.val ∧ i.val < a + len ∧ w.get i = b)).card := by
…

lemma OAI.Problem335.BalancedSchedule.ofFn_indexedWord line 55
Source documentation
Pulling the finite-indexed partition back to a list gives the constructed schedule.
```
lemma ofFn_indexedWord {k : ℕ} (hk : 0 < k) (s : ℕ) :
    List.ofFn (indexedWord hk s) = word k s := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.indexedWord, OAI.Problem335.BalancedSchedule.word
def OAI.Problem335.BalancedSchedule.intervalLayers line 63
Source documentation
A finite interval of the schedule, with a specified layer type.
```
def intervalLayers {k : ℕ} (hk : 0 < k) (s a len : ℕ) (b : Bool) :
    Finset (Fin (2 * k + s)) :=
…
```
lemma OAI.Problem335.BalancedSchedule.card_intervalLayers line 67
lemma OAI.Problem335.BalancedSchedule.intervalLayers_discrepancy_lt line 89
Source documentation
The balanced interval discrepancy in the finite-set form used for run bounds.
```
lemma intervalLayers_discrepancy_lt {k : ℕ} (hk : 0 < k) (s a len : ℕ) :
    ((intervalLayers hk s a len true).card : ℝ) - rho k s *
      ((intervalLayers hk s a len false).card : ℝ) < 1 + rho k s := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.intervalLayers, OAI.Problem335.BalancedSchedule.rho
lemma OAI.Problem335.BalancedSchedule.indexed_infix_discrepancy_lt line 96
Source documentation
RunLayerWeights' precise countP interface for a contiguous finite-index interval.
```
lemma indexed_infix_discrepancy_lt {k : ℕ} (hk : 0 < k) (s : ℕ)
    (b : List (Fin (2 * k + s))) (hb : b <:+: List.ofFn id) :
    (b.countP (indexedWord hk s) : ℝ) - rho k s *
      (b.countP (fun i => !indexedWord hk s i) : ℝ) < 1 + rho k s := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.indexedWord, OAI.Problem335.BalancedSchedule.rho