SmoothScales.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SmoothObstruction.SmoothScales.gap_scale_lower line 15
Source documentation
The source floor forces the gap×short-time scale to infinity. This is g L ≥ b^(3/4)n for g = sqrt b, L = ceil(b^(1/4)n).
```
lemma gap_scale_lower {b n : ℝ} (hn : 1≤n) (hb : n^(-1/10:ℝ)≤b) :
    n^(37/40:ℝ)≤b^(3/4:ℝ)*n := by
…
```

theorem OAI.SmoothObstruction.SmoothScales.gap_cost_absorption line 29

Source documentation

All fixed exponential gauge losses are absorbed by the genuine spectral gap×short-time exponent. Neither the gap nor the rates need be bounded away from zero.

theorem gap_cost_absorption {α : Type*} {l : Filter α} {b n : α → ℝ}
    (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)
    (C : ℝ) {c : ℝ} (hc : 0<c) :
    Tendsto (fun k => Real.exp (C*b k*n k-c*b k^(3/4:ℝ)*n k)) l (𝓝 0) := by
…

theorem OAI.SmoothObstruction.SmoothScales.weighted_gap_error line 70

Source documentation

Uniform exponentially small common-projector errors absorb every fixed gauge cost. This is the form needed by the finite leading-minor lower bound.

theorem weighted_gap_error {α : Type*} {l : Filter α} {b n δ : α → ℝ}
    (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)
    {c A : ℝ} (hc : 0<c) (hA : 0≤A) (C : ℝ)
    (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤Real.exp (-c*b k^(3/4:ℝ)*n k)) :
    Tendsto (fun k => A*Real.exp (C*b k*n k)*δ k) l (𝓝 0) := by
…

theorem OAI.SmoothObstruction.SmoothScales.common_frame_budget line 97

Source documentation

The literal dimension/gauge cost in the common-fast leading-minor proof is eventually small. Its parameters are fixed before bins and frames are selected, and the good-frame error has the source gap×short-time scale.

theorem common_frame_budget {α : Type*} {l : Filter α} {b n δ : α → ℝ}
    (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)
    {c F C N : ℝ} (hc : 0<c) (hF : 0≤F) (hN : 0≤N)
    (K₀ : ℝ) (p : ℕ)
    (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤Real.exp (-c*b k^(3/4:ℝ)*n k)) :
    ∀ᶠ k in l,
      (F*δ k)*(1+((C*(Real.exp (K₀*b k*n k))^p)^2*(C*2^p))*
        (C*(C^2*(Real.exp (K₀*b k*n k))^(2*p)*N)))≤1/2 := by
…

theorem OAI.SmoothObstruction.SmoothScales.weighted_full_gap line 138

Source documentation

The full-time gap dominates the short-time gap scale and every fixed gauge cost. No uniform positive lower bound on the spectral gap is assumed.

theorem weighted_full_gap {α : Type*} {l : Filter α} {b n : α → ℝ}
    (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)
    {c A : ℝ} (hc : 0<c) (hA : 0≤A) (C : ℝ) :
    Tendsto (fun k => A*Real.exp (C*b k*n k)*
      Real.exp (-c*b k^(1/2:ℝ)*n k)) l (𝓝 0) := by
…

theorem OAI.SmoothObstruction.SmoothScales.common_graph_budget line 157

Source documentation

The literal finite-gauge Cramer bound tends to zero, uniformly over all common bins satisfying the same scalar data. Fixed constants account for the dimension, endpoint projections and unit wedge norms.

theorem common_graph_budget {α : Type*} {l : Filter α} {b n δ : α → ℝ}
    (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)
    {c C N V W : ℝ} (hc : 0<c) (hN : 0≤N)
    (hV : 0≤V) (hW : 0≤W) (K₀ : ℝ) (p : ℕ)
    (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤Real.exp (-c*b k^(3/4:ℝ)*n k)) :
    Tendsto (fun k =>
      2*((C*(Real.exp (K₀*b k*n k))^p)^2*(C*2^p))*
        ((C*(C*(Real.exp (K₀*b k*n k))^p)^2*N*V)*
            Real.exp (-2*b k^(1/2:ℝ)*n k)+
         (C*(C^2*(Real.exp (K₀*b k*n k))^(2*p)*N))*W*δ k)) l (𝓝 0) := by
…

theorem OAI.SmoothObstruction.SmoothScales.perturbed_graph_decay line 186

Source documentation

Relative nonlinear errors preserve the vanishing Cramer bound.

theorem perturbed_graph_decay {α : Type*} {l : Filter α} {θ ε : α → ℝ}
    (hθ : Tendsto θ l (𝓝 0)) (hε : Tendsto ε l (𝓝 0)) :
    Tendsto (fun k => (θ k+ε k)/(1-ε k)) l (𝓝 0) := by
…

lemma OAI.SmoothObstruction.SmoothScales.ceil_gap_lower line 200
Source documentation
The manuscript's exact natural short length, including its ceiling.
```
lemma ceil_gap_lower {b n : ℝ} (hb : 0<b) :
    b^(3/4:ℝ)*n≤Real.sqrt b*(Nat.ceil (b^(1/4:ℝ)*n):ℝ) := by
…
```
lemma OAI.SmoothObstruction.SmoothScales.ceil_gap_error line 208

theorem OAI.SmoothObstruction.SmoothScales.common_frame_budget_short line 218

Source documentation

Discharges the literal finite common-frame budget directly from the source's g = sqrt b and L = ceil(b^(1/4)n), without dropping the rounding or imposing a positive gap floor.

theorem common_frame_budget_short {α : Type*} {l : Filter α} {b n δ : α → ℝ}
    (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)
    {c F C N : ℝ} (hc : 0<c) (hF : 0≤F) (hN : 0≤N) (K₀ : ℝ) (p : ℕ)
    (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤
      Real.exp (-c*Real.sqrt (b k)*(Nat.ceil (b k^(1/4:ℝ)*n k):ℝ))) :
    ∀ᶠ k in l,
      (F*δ k)*(1+((C*(Real.exp (K₀*b k*n k))^p)^2*(C*2^p))*
        (C*(C^2*(Real.exp (K₀*b k*n k))^(2*p)*N)))≤1/2 := by
…

theorem OAI.SmoothObstruction.SmoothScales.uniform_common_frame_budget line 238

Source documentation

Uniformity over every possible common-bin rank, including empty groups. Constants may depend on the rank but are fixed before bins, points and times are chosen. Thus no hidden point-dependent large-scale threshold remains.

theorem uniform_common_frame_budget {α : Type*} {l : Filter α} {b n δ : α → ℝ}
    (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)
    (d : ℕ) {c : ℝ} (hc : 0<c)
    (F C N K₀ : Fin (d+1) → ℝ) (hF : ∀ p,0≤F p) (hN : ∀ p,0≤N p)
    (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤
      Real.exp (-c*Real.sqrt (b k)*(Nat.ceil (b k^(1/4:ℝ)*n k):ℝ))) :
    ∀ᶠ k in l,∀ p : Fin (d+1),
      (F p*δ k)*(1+((C p*(Real.exp (K₀ p*b k*n k))^p.val)^2*(C p*2^p.val))*
        (C p*((C p)^2*(Real.exp (K₀ p*b k*n k))^(2*p.val)*N p)))≤1/2 := by
…

theorem OAI.SmoothObstruction.SmoothScales.uniform_common_graph_budget line 254

Source documentation

The actual Cramer error is small for all ranks simultaneously. Fixed rank-dependent costs do not change the source's quantifier order.

theorem uniform_common_graph_budget {α : Type*} {l : Filter α} {b n δ : α → ℝ}
    (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)
    (d : ℕ) {c : ℝ} (hc : 0<c)
    (C N V W K₀ : Fin (d+1) → ℝ)
    (hN : ∀ p,0≤N p) (hV : ∀ p,0≤V p) (hW : ∀ p,0≤W p)
    (hδ : ∀ᶠ k in l,0≤δ k ∧ δ k≤
      Real.exp (-c*Real.sqrt (b k)*(Nat.ceil (b k^(1/4:ℝ)*n k):ℝ)))
    {ε : ℝ} (hε : 0<ε) :
    ∀ᶠ k in l,∀ p : Fin (d+1),
      2*((C p*(Real.exp (K₀ p*b k*n k))^p.val)^2*(C p*2^p.val))*
        ((C p*(C p*(Real.exp (K₀ p*b k*n k))^p.val)^2*N p*V p)*
…

theorem OAI.SmoothObstruction.ExteriorStability.exterior_segment line 284
Source documentation
Exterior powers commute with the source's time-ordered product.
```
theorem exterior_segment (p : ℕ) (A : ℕ → E →L[ℝ] E) (s n : ℕ) :
    exterior p (segment A s n) = segment (fun t => exterior p (A t)) s n := by
…
```
Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

theorem OAI.SmoothObstruction.ExteriorStability.relative_exterior_core line 295

Source documentation

Finite-product assertion of manuscript Lemma lem:relative-exterior, in the canonical exterior Euclidean operator norm. The one-step constant is uniform over all exterior degrees p ≤ d, all products and all lengths. The proof actually does not need a ≥ 0, m ≥ 1, or K ≥ 1; the source assumptions are retained in the final source-specialized statement.

theorem relative_exterior_core (d : ℕ) (K : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (p : ℕ), p ≤ d →
      ∀ (A B : ℕ → E →L[ℝ] E) (m : ℕ) (σ a ε : ℝ),
      0 ≤ ε → ε ≤ 1 →
      (∀ t < m, ‖A t‖ ≤ K) →
      (∀ t < m, ‖B t - A t‖ ≤ ε) →
      (∀ s k : ℕ, s + k ≤ m →
        ‖exterior p (segment A s k)‖ ≤ Real.exp (σ * k + a)) →
      ‖exterior p (segment B 0 m) - exterior p (segment A 0 m)‖ ≤
        Real.exp (σ * m + a) * ((1 + C * ε * Real.exp (a + |σ|)) ^ m - 1) := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

theorem OAI.SmoothObstruction.ExteriorStability.relative_exterior line 319

Source documentation

Exact finite estimate in lem:relative-exterior for real d-dimensional Euclidean operators, hence real matrices in the Euclidean operator norm.

theorem relative_exterior (d : ℕ) (_hd : 1 ≤ d) (K : ℝ) (_hK : 1 ≤ K) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (p : ℕ), p ≤ d →
      ∀ (m : ℕ), 1 ≤ m →
      ∀ (A B : ℕ → EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d))
        (σ a ε : ℝ),
      0 ≤ a → 0 ≤ ε → ε ≤ 1 →
      (∀ t < m, ‖A t‖ ≤ K) →
      (∀ t < m, ‖B t - A t‖ ≤ ε) →
      (∀ s k : ℕ, s + k ≤ m →
        ‖exterior p (segment A s k)‖ ≤ Real.exp (σ * k + a)) →
      ‖exterior p (segment B 0 m) - exterior p (segment A 0 m)‖ ≤
        Real.exp (σ * m + a) * ((1 + C * ε * Real.exp (a + |σ|)) ^ m - 1) := by
…

Mentions: OAI.SmoothObstruction.ExteriorStability.exterior

theorem OAI.SmoothObstruction.ExteriorStability.exterior_zero line 340
theorem OAI.SmoothObstruction.ExteriorStability.exterior_zero_difference line 346
def OAI.SmoothObstruction.SmoothScales.B line 352
Source documentation
The spatial exponent in the manuscript, with its literal positive root.
```
noncomputable def B (b : ℝ) : ℝ := b ^ (1 / 8 : ℝ)
```
lemma OAI.SmoothObstruction.SmoothScales.positive line 354
lemma OAI.SmoothObstruction.SmoothScales.ratio line 356
lemma OAI.SmoothObstruction.SmoothScales.root_sixteen line 362
lemma OAI.SmoothObstruction.SmoothScales.lower_bound line 366
lemma OAI.SmoothObstruction.SmoothScales.square_dominates line 379
lemma OAI.SmoothObstruction.SmoothScales.ratio_tendsto_zero line 389

theorem OAI.SmoothObstruction.SmoothScales.decisive_decay line 401

Source documentation

Quantitative exponential decay used in the relative-minor transfer. It holds for every fixed real coefficient C, including all constants coming from the dimension, charts, and inverse basis bounds.

theorem decisive_decay {α : Type*} {l : Filter α} {b n : α → ℝ}
    (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) (C : ℝ) :
    Tendsto (fun k => n k * Real.exp (-(3 / 2 : ℝ) * B (b k) * n k + C * b k * n k))
      l (𝓝 0) := by
…

Mentions: OAI.SmoothObstruction.SmoothScales.B

lemma OAI.SmoothObstruction.RelativeAsymptotics.exp_sub_one_le line 432
lemma OAI.SmoothObstruction.RelativeAsymptotics.pow_one_add_sub_one_le line 436
lemma OAI.SmoothObstruction.RelativeAsymptotics.normalized_estimate line 444

theorem OAI.SmoothObstruction.RelativeAsymptotics.uniform_relative_small line 473

Source documentation

The little-oh conclusion of the exterior-product lemma. The hypotheses on x are the proved finite estimate, not an asymptotic conclusion. This bound is uniform over all products and all exterior degrees covered by that estimate.

theorem uniform_relative_small {α : Type*} {l : Filter α}
    {b n x σ a ε : α → ℝ} {m : α → ℕ}
    (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)
    (C C₀ C₁ C₂ C₃ : ℝ) (hC : 0 ≤ C) (hC₀ : 0 ≤ C₀)
    (hC₃ : 0 ≤ C₃)
    (hdata : ∀ᶠ k in l,
      0 ≤ x k ∧ 0 ≤ a k ∧ 0 ≤ ε k ∧ (m k : ℝ) ≤ 2 * n k ∧
      a k ≤ C₁ * b k * n k ∧ |σ k| ≤ C₂ ∧
      ε k ≤ C₃ * Real.exp (-(3 / 2 : ℝ) * SmoothScales.B (b k) * n k) ∧
      x k ≤ Real.exp (σ k * m k + a k) *
…

Mentions: OAI.SmoothObstruction.SmoothScales.B

def OAI.SmoothObstruction.RelativeAsymptotics.envelope line 545
Source documentation
A single, choice-independent numerical envelope for all the relative exterior errors at a given dyadic scale.
```
noncomputable def envelope (C C₀ C₁ C₂ C₃ b n : ℝ) : ℝ :=
…
```
lemma OAI.SmoothObstruction.RelativeAsymptotics.uniform_relative_bound line 550
lemma OAI.SmoothObstruction.RelativeAsymptotics.envelope_tendsto line 584