ShortScales.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SmoothObstruction.ScaleHierarchy.lower_bound line 12
lemma OAI.SmoothObstruction.ScaleHierarchy.square_dominates line 23
lemma OAI.SmoothObstruction.ScaleHierarchy.ratio_tendsto_zero line 33

theorem OAI.SmoothObstruction.ScaleHierarchy.polynomial_decay line 44

Source documentation

General separated-power budget. The floor and the original time scale are unchanged; every fixed polynomial cost and exponential b^q n cost is absorbed.

theorem polynomial_decay {ι : Type*} {l : Filter ι} {b n : ι → ℝ}
    {p q c C : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (hqp : p < q) (hc : 0 < c)
    (hbpos : ∀ᶠ k in l, 0 < b k) (hb : Tendsto b l (𝓝 0))
    (hn : Tendsto n l atTop)
    (hfloor : ∀ᶠ k in l, n k ^ (-1 / 10 : ℝ) ≤ b k) (m : ℕ) :
    Tendsto (fun k => n k ^ m * Real.exp (C * b k ^ q * n k - c * b k ^ p * n k))
      l (𝓝 0) := by
…

lemma OAI.SmoothObstruction.ShortBin.bvp_nonneg line 83
lemma OAI.SmoothObstruction.ShortBin.bvp_cost line 88

theorem OAI.SmoothObstruction.ShortBin.bvp_decay line 146

Source documentation

Explicit BVP cost is absorbed by the prescribed spatial exponent.

theorem bvp_decay {ι : Type*} {l : Filter ι} {b : ι → ℝ} {n : ι → ℕ}
    {K a : ι → ℝ} {p q c D : ℝ}
    (hp : 0≤p) (hp1 : p≤1) (hpq : p<q) (hc : 0<c)
    (hbpos : ∀ᶠ k in l,0<b k) (hb : Tendsto b l (𝓝 0))
    (hn : Tendsto (fun k => (n k:ℝ)) l atTop)
    (hfloor : ∀ᶠ k in l,(n k:ℝ)^(-1/10:ℝ)≤b k)
    (hK : ∀ᶠ k in l,0≤K k ∧ K k≤D*b k^q*n k)
    (ha : ∀ᶠ k in l,0≤a k ∧ a k≤D*b k^q) :
    Tendsto (fun k => bvpInverseBound (K k) (a k) (n k)*
      Real.exp (-c*b k^p*n k)) l (𝓝 0) := by
…

Mentions: OAI.SmoothObstruction.ShortBin.bvpInverseBound

theorem OAI.SmoothObstruction.ShortBin.bvp_spatial_budgets line 178

Source documentation

Both nonlinear-contraction budgets hold at the original scales, with no rescaling of r, δ or the horizon.

theorem bvp_spatial_budgets {ι : Type*} {l : Filter ι} {b : ι → ℝ} {n : ι → ℕ}
    {K a : ι → ℝ} {D C : ℝ}
    (hbpos : ∀ᶠ k in l,0<b k) (hb : Tendsto b l (𝓝 0))
    (hn : Tendsto (fun k => (n k:ℝ)) l atTop)
    (hfloor : ∀ᶠ k in l,(n k:ℝ)^(-1/10:ℝ)≤b k)
    (hK : ∀ᶠ k in l,0≤K k ∧ K k≤D*b k^(1/2:ℝ)*n k)
    (ha : ∀ᶠ k in l,0≤a k ∧ a k≤D*b k^(1/2:ℝ)) :
    ∀ᶠ k in l,
      bvpInverseBound (K k) (a k) (n k)*C*Real.exp (-(3/2:ℝ)*b k^(1/8:ℝ)*n k)≤1/4 ∧
      bvpInverseBound (K k) (a k) (n k)*C*Real.exp (-2*b k^(1/8:ℝ)*n k)≤
        Real.exp (-(3/2:ℝ)*b k^(1/8:ℝ)*n k)/4 := by
…

Mentions: OAI.SmoothObstruction.ShortBin.bvpInverseBound

theorem OAI.SmoothObstruction.ShortBin.bvp_power_decay line 216

Source documentation

Polynomial powers of the actual BVP inverse cost remain absorbable.

theorem bvp_power_decay {ι : Type*} {l : Filter ι} {b : ι → ℝ} {n : ι → ℕ}
    {K a : ι → ℝ} {p q c D J : ℝ}
    (hp : 0≤p) (hp1 : p≤1) (hpq : p<q) (hc : 0<c)
    (hbpos : ∀ᶠ k in l,0<b k) (hb : Tendsto b l (𝓝 0))
    (hn : Tendsto (fun k => (n k:ℝ)) l atTop)
    (hfloor : ∀ᶠ k in l,(n k:ℝ)^(-1/10:ℝ)≤b k)
    (hK : ∀ᶠ k in l,0≤K k ∧ K k≤D*b k^q*n k)
    (ha : ∀ᶠ k in l,0≤a k ∧ a k≤D*b k^q) (m : ℕ) :
    Tendsto (fun k => (bvpInverseBound (K k) (a k) (n k))^m *
      Real.exp (J*b k^q*n k-c*b k^p*n k)) l (𝓝 0) := by
…

Mentions: OAI.SmoothObstruction.ShortBin.bvpInverseBound

theorem OAI.SmoothObstruction.ShortBin.spatial_switch_limits line 245

Source documentation

The sharp join radius and ideal-cell exchange error at the literal source spatial scales. The error is measured after applying the inverse product basis.

theorem spatial_switch_limits {ι : Type*} {l : Filter ι} {b : ι → ℝ} {n : ι → ℕ}
    {ε : ι → ℝ} (hbpos : ∀ᶠ k in l,0<b k) (hb : Tendsto b l (𝓝 0))
    (hn : Tendsto (fun k => (n k:ℝ)) l atTop)
    (hfloor : ∀ᶠ k in l,(n k:ℝ)^(-1/10:ℝ)≤b k)
    (hε : ∀ᶠ k in l,0≤ε k ∧ ε k≤Real.exp (-b k^(3/4:ℝ)*n k))
    (Dg A C₀ : ℝ) (hDg : 0≤Dg) (hA : 0≤A) :
    let B (k : ι) := Dg*(b k*n k)
…

theorem OAI.SmoothObstruction.ShortBin.spatial_ready line 344

Source documentation

Scalar hypotheses of the genuine switch, at the unchanged source scales. Both grid widths are fixed multiples of the original h0 and r.

theorem spatial_ready {ι : Type*} {l : Filter ι} {b : ι → ℝ} {n : ι → ℕ}
    (hbpos : ∀ᶠ k in l,0<b k) (hb : Tendsto b l (𝓝 0))
    (hn : Tendsto (fun k => (n k:ℝ)) l atTop)
    (hfloor : ∀ᶠ k in l,(n k:ℝ)^(-1/10:ℝ)≤b k)
    (Dg A C₀ C₁ Cg K₀F K₀B r₀ rg σ r₁ rμ Ac Ap : ℝ)
    (hDg : 0≤Dg) (hA : 0≤A) (hC₀ : 1≤C₀)
    (hr₀ : 0<r₀) (hrg : 0<rg) (hσ : 0<σ) (hr₁ : 0<r₁) (hrμ : 0<rμ)
    (hAc : 0<Ac) (hAp : 0<Ap) :
    let B (k : ι) := Dg*(b k*n k)
…