PackedSchedule.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExactFourier.Packing.pack_list line 11

Source documentation

Convert exact slot factorizations to a literal word, retaining the precise call count.

theorem pack_list (J : Matrix γ γ ℂ) (L : List (Matrix α α ℂ))
 (hL : ∀ B∈L,∃ (M : Matrix α α ℂ) (e : γ↪α),MonomialMatrix M ∧ B=M*Embedded.matrix e J) :
 ∃ W : Word (fun _ : Unit=>γ) (fun _=>J) α,W.matrix=L.prod ∧ W.calls.length=L.length := by
…

Mentions: OAI.ExactFourier.L, OAI.ExactFourier.MonomialMatrix, OAI.ExactFourier.Embedded.matrix, OAI.ExactFourier.Packing.Word

theorem OAI.ExactFourier.Packing.packed_schedule line 30
def OAI.ExactFourier.Packing.cyclicStart line 58
Source documentation
Sectors with identical programs start cyclically at the F possible starts.
```
def cyclicStart (F : ℕ) {m : ℕ} (j : Fin m) : ℕ := j.val % F
```
theorem OAI.ExactFourier.Packing.quotient_lt line 60

theorem OAI.ExactFourier.Packing.same_remainder_card line 65

Source documentation

Within any one residue class, division by F is an injective label.

theorem same_remainder_card {m F : ℕ} (S : Finset (Fin m))
    (hS : ∀ i ∈ S, ∀ j ∈ S, i.val % F = j.val % F) : S.card ≤ m / F + 1 := by
…

theorem OAI.ExactFourier.Packing.occurrence_card line 81
Source documentation
Every occurrence of a fixed program has at most floor(m/F)+1 copies in a slot.
```
theorem occurrence_card {m F o t : ℕ} :
    (Finset.univ.filter (fun j : Fin m => cyclicStart F j + o = t)).card ≤ m / F + 1 := by
…
```
Mentions: OAI.ExactFourier.Packing.cyclicStart
theorem OAI.ExactFourier.Packing.occurrence_card_real line 91
def OAI.ExactFourier.Packing.occurrences line 106
Source documentation
Positions of calls of type i within a fixed sector program.
```
def occurrences (P : List τ) (i : τ) : Finset (Fin P.length) :=
…
```
def OAI.ExactFourier.Packing.scheduledLoad line 110
Source documentation
Exact number of calls of a given type at a given time in the cyclic schedule.
```
def scheduledLoad (P : π → List τ) (m : π → ℕ) (F : ℕ) (i : τ) (t : ℕ) : ℕ :=
…
```
def OAI.ExactFourier.Packing.totalCalls line 115
Source documentation
Total calls of a type before scheduling.
```
def totalCalls (P : π → List τ) (m : π → ℕ) (i : τ) : ℕ :=
…
```
theorem OAI.ExactFourier.Packing.scheduledLoad_bound line 120
Source documentation
The additive discrepancy is a constant depending only on the fixed program family, not on sector multiplicities or on the number of slots.
```
theorem scheduledLoad_bound (P : π → List τ) (m : π → ℕ) (F : ℕ) (hF : 0 < F)
    (i : τ) (t : ℕ) :
    (scheduledLoad P m F i t : ℝ) ≤ (totalCalls P m i : ℝ) / F + ∑ p, ((P p).length : ℝ) := by
…
```
Mentions: OAI.ExactFourier.Packing.scheduledLoad, OAI.ExactFourier.Packing.totalCalls
theorem OAI.ExactFourier.Packing.schedule_strict line 147
Source documentation
Chronological order is strict inside every sector, including repeated types.
```
theorem schedule_strict {F m : ℕ} (j : Fin m) :
    StrictMono (fun o : ℕ => cyclicStart F j + o) := by
…
```
Mentions: OAI.ExactFourier.Packing.cyclicStart
theorem OAI.ExactFourier.Packing.schedule_in_range line 154
Source documentation
No occurrence is placed outside the allocated F+L-1 slots.
```
theorem schedule_in_range {F L m : ℕ} (hF : 0 < F) (j : Fin m) (o : Fin L) :
    cyclicStart F j + o.val < F + L - 1 := by
…
```
Mentions: OAI.ExactFourier.L, OAI.ExactFourier.Packing.cyclicStart
theorem OAI.ExactFourier.Packing.scheduledLoad_capacity line 161
theorem OAI.ExactFourier.Packing.framedSlot_type line 181
def OAI.ExactFourier.Packing.subtypeSigmaAll line 198
theorem OAI.ExactFourier.Packing.card_subtype_sigma line 205
theorem OAI.ExactFourier.Packing.slot_card line 213

theorem OAI.ExactFourier.Packing.monotone_fiber_gap line 248

Source documentation

A monotone chronological listing cannot repeat a time after more than its capacity.

theorem monotone_fiber_gap {n T d : ℕ} (f : Fin n→Fin T) (hm : Monotone f)
 (hc : ∀ t,Fintype.card {i // f i=t}<d) {a b : Fin n}
 (hab : a.val+d≤b.val) : f a<f b := by
…

def OAI.ExactFourier.Packing.sigmaFiberEquiv line 266
theorem OAI.ExactFourier.Packing.vacancy_listing line 273

theorem OAI.ExactFourier.Packing.exists_dummy_schedule line 293

Source documentation

Cyclic vacancy allocation; no distribution assumption on the clustering of vacancies.

theorem exists_dummy_schedule {T d h k : ℕ} (c : Fin T→ℕ)
 (hc : ∀ t,c t≤k) (hkd : k<d) (hsum : ∑ t,c t=d*h) :
 ∃ time : Fin d→Fin h→Fin T,(∀ j,StrictMono (time j)) ∧
   ∀ t,Fintype.card {v : Fin d×Fin h // time v.1 v.2=t}=c t := by
…

theorem OAI.ExactFourier.Packing.exists_dummy_framed line 326