AsymptoticSplitting.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SmoothObstruction.EuclideanSplitting.segment_toEuclidean line 16

theorem OAI.SmoothObstruction.EuclideanSplitting.actual_interval_exterior line 25

Source documentation

No product bounds are assumed: every interval follows from the actual coordinate derivative equations and the uniformly bounded finite gauges.

theorem actual_interval_exterior
    (A U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
    (S : Finset (Fin d)) (N : ℕ) {γ g K C : ℝ}
    (hUV : ∀ t, U t * V t = 1) (hVU : ∀ t, V t * U t = 1)
    (hA : ∀ t < N, A t * U t = U (t+1) * rate lam 1)
    (hg : 0 ≤ g) (hK : 0 ≤ K) (hC : 0 ≤ C)
    (hfast : ∀ j ∈ S, γ + g ≤ lam j) (hslow : ∀ j ∉ S, lam j ≤ γ - g)
    (hU : ∀ t ≤ N, ‖U t‖ ≤ Real.exp K) (hV : ∀ t ≤ N, ‖V t‖ ≤ Real.exp K)
    (hpoly : ∀ A : EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d),
      ‖exterior S.card A‖ ≤ C * (max 1 ‖A‖)^S.card)
    (s l : ℕ) (hsl : s + l ≤ N) :
    ‖exterior S.card (segment (fun t => Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ) (A t)) s l)‖ ≤
…

Mentions: OAI.SmoothObstruction.EuclideanSplitting.rate

lemma OAI.SmoothObstruction.EuclideanSplitting.absorb_prefactor line 46

theorem OAI.SmoothObstruction.EuclideanSplitting.exists_uniform_interval_constant line 71

Source documentation

One exponential constant works for every possible fast rank, including zero. Dimension dependent polynomial norms and gauge prefactors are derived, not added as assumptions about the derivative cocycle.

theorem exists_uniform_interval_constant (d : ℕ) (D : ℝ) (hD : 0 ≤ D) :
    ∃ C₁ : ℝ, 0 ≤ C₁ ∧ ∀ (A U V : ℕ → Matrix (Fin d) (Fin d) ℝ)
      (lam : Fin d → ℝ) (S : Finset (Fin d)) (N : ℕ) (γ g K z : ℝ),
      1 ≤ z → 0 ≤ g → 0 ≤ K → K ≤ D*z →
      (∀ t, U t * V t = 1) → (∀ t, V t * U t = 1) →
      (∀ t < N, A t * U t = U (t+1) * rate lam 1) →
      (∀ j ∈ S, γ+g ≤ lam j) → (∀ j ∉ S, lam j ≤ γ-g) →
      (∀ t ≤ N, ‖U t‖ ≤ Real.exp K) → (∀ t ≤ N, ‖V t‖ ≤ Real.exp K) →
      ∀ s l : ℕ, s+l ≤ N →
        ‖exterior S.card (segment (fun t => Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ) (A t)) s l)‖ ≤
…

Mentions: OAI.SmoothObstruction.EuclideanSplitting.rate

lemma OAI.SmoothObstruction.EuclideanSplitting.rate_sum_abs_le line 118

theorem OAI.SmoothObstruction.EuclideanSplitting.uniform_relative_gauged line 131

Source documentation

Choice-independent relative stability on ALL actual gauged intervals at once. The only perturbation hypothesis is the genuine one-step derivative error; all subinterval exterior bounds are proved from the gauge equations. The same numerical envelope works for every fast rank and every witness.

theorem uniform_relative_gauged (d : ℕ) (K₀ D : ℝ) (hD : 0 ≤ D) :
    ∃ C C₁ : ℝ, 0 ≤ C ∧ 0 ≤ C₁ ∧
      ∀ (A U V : ℕ → Matrix (Fin d) (Fin d) ℝ)
        (T : ℕ → EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d))
        (lam : Fin d → ℝ) (S : Finset (Fin d)) (m : ℕ)
        (γ g K b n C₀ R C₃ ε : ℝ),
        0 ≤ b → 0 ≤ n → 1 ≤ b*n → 0 ≤ C₀ → 0 ≤ R → 0 ≤ C₃ →
        0 ≤ g → 0 ≤ K → K ≤ D*(b*n) → (m:ℝ) ≤ 2*n →
        (∀ t, U t*V t=1) → (∀ t,V t*U t=1) →
        (∀ t < m,A t*U t=U (t+1)*rate lam 1) →
        (∀ i,|lam i| ≤ R) →
        (∀ j ∈ S, γ+g ≤ lam j) → (∀ j ∉ S, lam j ≤ γ-g) →
…

Mentions: OAI.SmoothObstruction.EuclideanSplitting.rate

theorem OAI.SmoothObstruction.EuclideanSplitting.actual_uniform_relative line 176

Source documentation

The uniform, all-rank, choice-independent relative error for derivatives of actual nonlinear orbit compositions. All interval bounds are derived from the genuine gauge equations, and the perturbations from the one-step C² bounds and the orbit tube. No long-iterate regularity bound is assumed.

theorem actual_uniform_relative (d : ℕ) (K₀ Dg : ℝ) (hDg : 0 ≤ Dg) :
    ∃ C C₁ : ℝ, 0 ≤ C ∧ 0 ≤ C₁ ∧
      ∀ (f : ℕ → EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d))
        (x y : ℕ → EuclideanSpace ℝ (Fin d)) (s : ℕ → Set (EuclideanSpace ℝ (Fin d)))
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (S : Finset (Fin d)) (m : ℕ) (γ g K b n C₀ R D : ℝ),
        0 ≤ b → 0 ≤ n → 1 ≤ b*n → 0 ≤ C₀ → 0 ≤ R → 0 ≤ D →
        0 ≤ g → 0 ≤ K → K ≤ Dg*(b*n) → (m:ℝ) ≤ 2*n →
        (∀ t, U t*V t=1) → (∀ t,V t*U t=1) →
        (∀ t < m, (Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
…

theorem OAI.SmoothObstruction.ManifoldCoordinates.iterate_localMap_germ line 241
Source documentation
The nonautonomous chart composition has exactly the same germ as the actual long iterate in the two endpoint charts. Intermediate chart codes therefore never have to be encoded in the partition or switch labels.
```
theorem iterate_localMap_germ (S : Diffeomorph I I M M ∞) (a : ℕ → M) (x : M)
    (N : ℕ) (hx : ∀ t≤N,(S^[t]) x∈(extChartAt I (a t)).source)
    (hint : (extChartAt I (a 0)) x∈interior (range I)) :
    ShortDerivative.iterate (fun t => localMap I S (a t) (a (t+1))) N =ᶠ[𝓝 ((extChartAt I (a 0)) x)]
      extChartAt I (a N) ∘ S^[N] ∘ (extChartAt I (a 0)).symm := by
…
```
Mentions: OAI.SmoothObstruction.ShortDerivative.iterate, OAI.SmoothObstruction.ManifoldCoordinates.localMap

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_endpoint_relative line 281

Source documentation

The relative exterior estimate for the ACTUAL long iterate, in the old input's endpoint charts. The constants are uniform over all ranks, rates, gauges and selectors. The tube condition is imposed on the genuine new orbit; no assumed derivative or determinant estimate is used.

theorem actual_endpoint_relative (hclosed : IsClosed (range I))
    (S : Diffeomorph I I M M ∞) (a : ι → M) (L : ι → Set M)
    (hL : ∀ i,IsCompact (L i)) (hLU : ∀ i,L i⊆(chartAt H (a i)).source)
    (Dg : ℝ) (hDg : 0≤Dg) :
    ∃ r K₀ C C₁ : ℝ,0<r ∧ 1≤K₀ ∧ 0≤C ∧ 0≤C₁ ∧
      ∀ (c : M → ι) (x y : M) (m : ℕ)
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (T : Finset (Fin d)) (γ g K b n C₀ R : ℝ),
        (∀ z,z∈L (c z)) → 0≤b → 0≤n → 1≤b*n → 0≤C₀ → 0≤R →
        0≤g → 0≤K → K≤Dg*(b*n) → (m:ℝ)≤2*n →
        (∀ t,U t*V t=1) → (∀ t,V t*U t=1) →
        (∀ t < m,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
…

lemma OAI.SmoothObstruction.ShortDerivative.contDiffAt_iterate line 370

lemma OAI.SmoothObstruction.EuclideanSplitting.derivative_transition line 392

Source documentation

A gauge for the actual one-step differentials identifies the derivative of the true orbit composition with its genuine transition matrix.

lemma derivative_transition (f : ℕ → E → E) (x : ℕ → E)
    (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ) (N : ℕ)
    (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
    (hx : ∀ t<N,f t (x t)=x (t+1))
    (hd : ∀ t<N,DifferentiableAt ℝ (f t) (x t))
    (hstep : ∀ t<N,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
…

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_endpoint_smooth line 419

Source documentation

Regularity of the actual endpoint expression in the old charts, not a formal composition with unrelated derivatives.

theorem actual_endpoint_smooth (S : Diffeomorph I I M M ∞) (a : ℕ → M) (x : M) (n : ℕ)
    (hx : ∀ t ≤ n,S^[t] x∈(extChartAt I (a t)).source)
    (hi : ∀ t ≤ n,(extChartAt I (a t)) (S^[t] x)∈interior (range I)) :
    ContDiffAt ℝ ∞ (extChartAt I (a n) ∘ S^[n] ∘ (extChartAt I (a 0)).symm)
      ((extChartAt I (a 0)) x) := by
…

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_endpoint_differential line 441

Source documentation

The old endpoint differential is exactly the transition of its real one-step gauge. This equality permits relative exterior control to feed the leading-minor estimate at zero rank as well as positive rank.

theorem actual_endpoint_differential (S : Diffeomorph I I M M ∞) (a : ℕ → M)
    (x : M) (n : ℕ) (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
    (hx : ∀ t ≤ n,S^[t] x∈(extChartAt I (a t)).source)
    (hi : ∀ t ≤ n,(extChartAt I (a t)) (S^[t] x)∈interior (range I))
    (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
    (hstep : ∀ t < n,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
…