Schedule.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Using the refinement search

lemma OAI.FourierLLogL.Compress.any_above line 13
lemma OAI.FourierLLogL.Compress.exists_offer line 22
structure OAI.FourierLLogL.Compress.Schedule line 51
Source documentation
Parameters of the two-order search.
```
structure Schedule where
…
```
def OAI.FourierLLogL.Compress.Schedule.size line 77
def OAI.FourierLLogL.Compress.Schedule.loss line 78
lemma OAI.FourierLLogL.Compress.Schedule.loss_pos line 79
lemma OAI.FourierLLogL.Compress.offer_at line 86

theorem OAI.FourierLLogL.Compress.reach line 145

Source documentation

Reach a long, low-cost block length.

theorem reach (tag : A → G) (hi : Injective tag) (c : G → ℝ) (_hc0 : ∀ x, 0 ≤ c x)
    (S : Labelled A) (D F : ℝ) (hd : 0 < D) (hf : 0 < F) (B : Schedule)
    (m : ℕ) (l u r : ℕ → ℕ) (hm : 0 < m)
    (hl : ∀ i, i < B.size → l i ≤ u i ∧ u i ≤ m)
    (hp : ∀ i j, i < j → j < B.size → u j ≤ l i ∧ r i ≤ r j)
    (hG : ∀ i, i<B.size → fundG tag S (u i) ≤ D)
    (hI : ∀ i, i<B.size → fundI tag S (r i) ≤ D) :
    ∃ T, refines T S ∧ fundG tag S 1 - fundG tag T 1 ≤ B.loss*D*D/F ∧
      ∃ i, i < B.size ∧ fundK tag c T (u i) (r i) ≤ F+fundK tag c T (l i) (r i) := by
…

Mentions: OAI.FourierLLogL.Compress.S, OAI.FourierLLogL.Compress.Labelled, OAI.FourierLLogL.Compress.Schedule, OAI.FourierLLogL.Compress.fundG, OAI.FourierLLogL.Compress.fundI, OAI.FourierLLogL.Compress.refines, OAI.FourierLLogL.Compress.fundK