Search.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Two-order finite refinement search

structure OAI.FourierLLogL.Compress.Arena line 16
Source documentation
Normalized potentials. A can only move down in time. Across indices A moves up while the low and high potentials are margins of disjoint intervals that move down.
```
structure Arena (S : Type u) where
…
```
Mentions: OAI.FourierLLogL.Compress.S
lemma OAI.FourierLLogL.Compress.Arena.dummy line 46
lemma OAI.FourierLLogL.Compress.Arena.H_index line 48
lemma OAI.FourierLLogL.Compress.Arena.L_index line 52
lemma OAI.FourierLLogL.Compress.Arena.budget_index line 57

lemma OAI.FourierLLogL.Compress.Arena.budget_ascending line 137

Source documentation

Forward search through adjacent blocks [o+i*m,o+(i+1)m). Fully failed blocks consume width.

lemma budget_ascending (s : S) (G : S → Prop)
    (o n m : ℕ) (hm : 0 < m) (hn : 0 < n) (hb : o+n*m ≤ d.N)
    (a b δ : ℝ) (ha : 0 < a) (hδ : 1 < n*δ)
    (hstep : ∀ (t) (_h : d.mov s t) i (_hi : i<n), ∃ q, d.mov t q ∧
      ((G q ∧ d.topc t-d.topc q ≤ a*(d.H (o+i*m) t-d.L (o+(i+1)*m-1) q)+b) ∨
        (d.topc t-d.topc q)+a*δ ≤ a*(d.H (o+i*m) t-d.L (o+(i+1)*m-1) q))) :
    ∃ t, d.mov s t ∧ G t ∧ d.topc s-d.topc t ≤ a*(d.H o s-d.L (o+n*m-1) t)+b := by
…

Mentions: OAI.FourierLLogL.Compress.S

lemma OAI.FourierLLogL.Compress.Arena.budget_sub line 192

lemma OAI.FourierLLogL.Compress.Arena.budget_macro line 223

Source documentation

The macro-scale scan goes from right to left through small blocks. Skip if lower-to-upper width is too large, unless goal encountered.

lemma budget_macro (s : S) (o q n : ℕ) (hn : 0 < n) (hq : 0 < q)
    (hb : o+q*n ≤ d.N)
    (u a δ η α ε : ℝ) (hu : 0 < u) (ha : 0 < a) (hδ : 0 < δ)
    (hη : δ*exp (2*u/a) ≤ η) (hnδ : 1 < (n:ℝ)*δ)
    (ha' : 0 < α) (he : 0 < ε) (hb' : 2*(a/α) ≤ 1)
    (hc : (ε+η)*exp (2*(a/α)*q) ≤ 1) (hqu : 1 < (q:ℝ)*u) :
    ∃ t, d.mov s t ∧
      ((d.found t ∧ d.topc s-d.topc t ≤ α+a*(1+η)) ∨
        (d.topc s-d.topc t)+α*ε ≤ α*(d.H o s-d.L (o+q*n-1) t)) := by
…

Mentions: OAI.FourierLLogL.Compress.S

lemma OAI.FourierLLogL.Compress.Arena.complete_search line 325