ShortDerivative.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.RelativeProduct.segment line 20
Source documentation
Later times multiply on the left, as in the manuscript.
```
def segment [Monoid R] (A : ℕ → R) (s : ℕ) : ℕ → R
  | 0 => 1
  | n + 1 => A (s + n) * segment A s n
```
theorem OAI.SmoothObstruction.RelativeProduct.segment_zero line 24
theorem OAI.SmoothObstruction.RelativeProduct.segment_succ line 27

theorem OAI.SmoothObstruction.RelativeProduct.difference line 31

Source documentation

Exact variation-of-constants expansion; no commutativity is used.

theorem difference [Ring R] (A B : ℕ → R) (s n : ℕ) :
    segment B s n - segment A s n =
      ∑ j ∈ Finset.range n,
        segment A (s + j + 1) (n - (j + 1)) *
          (B (s + j) - A (s + j)) * segment B s j := by
…

Mentions: OAI.SmoothObstruction.RelativeProduct.segment

theorem OAI.SmoothObstruction.RelativeProduct.norm_difference_le line 58

Source documentation

Uniform subinterval bounds yield a relative error, rather than a bound obtained by multiplying one-step bounds.

theorem norm_difference_le [NormedRing R] (A B : ℕ → R)
    (s m : ℕ) (L δ : ℝ) (hL : 0 ≤ L) (hδ : 0 ≤ δ)
    (hA : ∀ t k : ℕ, s ≤ t → t + k ≤ s + m → ‖segment A t k‖ ≤ L)
    (hBA : ∀ t : ℕ, s ≤ t → t < s + m → ‖B t - A t‖ ≤ δ) :
    ‖segment B s m - segment A s m‖ ≤ L * ((1 + L * δ) ^ m - 1) := by
…

Mentions: OAI.SmoothObstruction.RelativeProduct.segment

theorem OAI.SmoothObstruction.RelativeProduct.segment_smul line 104
Source documentation
Scalar normalization of a whole interval.
```
theorem segment_smul [NormedRing R] [NormedAlgebra ℝ R]
    (A : ℕ → R) (c : ℝ) (s n : ℕ) :
    segment (fun t => c • A t) s n = c ^ n • segment A s n := by
…
```
Mentions: OAI.SmoothObstruction.RelativeProduct.segment
theorem OAI.SmoothObstruction.RelativeProduct.exp_cancel line 112

theorem OAI.SmoothObstruction.RelativeProduct.norm_difference_le_exp_exact line 119

Source documentation

The relative perturbation bound with its exact exponential weight.

theorem norm_difference_le_exp_exact [NormedRing R] [NormedAlgebra ℝ R]
    (A B : ℕ → R) (s m : ℕ) (σ a δ : ℝ) (hδ : 0 ≤ δ)
    (hA : ∀ t k : ℕ, s ≤ t → t + k ≤ s + m →
      ‖segment A t k‖ ≤ Real.exp (σ * k + a))
    (hBA : ∀ t : ℕ, s ≤ t → t < s + m → ‖B t - A t‖ ≤ δ) :
    ‖segment B s m - segment A s m‖ ≤
      Real.exp (σ * m + a) * ((1 + δ * Real.exp (a - σ)) ^ m - 1) := by
…

Mentions: OAI.SmoothObstruction.RelativeProduct.segment

theorem OAI.SmoothObstruction.RelativeProduct.norm_difference_le_exp line 162

Source documentation

Quantitative core of the source exterior-product perturbation lemma. Applying this to exterior powers with one-step error δ = C * ε gives exactly its stated finite-product bound.

theorem norm_difference_le_exp [NormedRing R] [NormedAlgebra ℝ R]
    (A B : ℕ → R) (s m : ℕ) (σ a δ : ℝ) (hδ : 0 ≤ δ)
    (hA : ∀ t k : ℕ, s ≤ t → t + k ≤ s + m →
      ‖segment A t k‖ ≤ Real.exp (σ * k + a))
    (hBA : ∀ t : ℕ, s ≤ t → t < s + m → ‖B t - A t‖ ≤ δ) :
    ‖segment B s m - segment A s m‖ ≤
      Real.exp (σ * m + a) * ((1 + δ * Real.exp (a + |σ|)) ^ m - 1) := by
…

Mentions: OAI.SmoothObstruction.RelativeProduct.segment

lemma OAI.SmoothObstruction.RelativeProduct.segment_norm_le line 179
lemma OAI.SmoothObstruction.RelativeProduct.short_difference line 192
Source documentation
Ordinary C¹ telescoping on a short interval. Unlike the long-window relative exterior estimate this bound pays the one-step bound, precisely where the manuscript permits an exp(CL) loss.
```
lemma short_difference (A B : ℕ → R) (N : ℕ) (hOne : ‖(1:R)‖≤1) {K δ : ℝ}
    (hK : 1≤K) (hδ : 0≤δ)
    (hA : ∀ t<N,‖A t‖≤K) (hB : ∀ t<N,‖B t‖≤K)
    (hBA : ∀ t<N,‖B t-A t‖≤δ) :
    ‖segment B 0 N-segment A 0 N‖≤N*K^N*δ := by
…
```
Mentions: OAI.SmoothObstruction.RelativeProduct.segment

def OAI.SmoothObstruction.ShortDerivative.iterate line 226

Source documentation

Actual nonautonomous coordinate composition.

def iterate (f : ℕ → E → E) : ℕ → E → E
  | 0 => id
  | n+1 => f n ∘ iterate f n

omit [NormedAddCommGroup E] [NormedSpace ℝ E] in

lemma OAI.SmoothObstruction.ShortDerivative.orbit_eq_iterate line 231
lemma OAI.SmoothObstruction.ShortDerivative.derivative_iterate line 240

theorem OAI.SmoothObstruction.ShortDerivative.short_c1_stability line 258

Source documentation

Nearby genuine coordinate orbits have exponentially close short products, under uniform first and second derivative bounds on convex patches. No derivative of the long iterate is bounded by fiat.

theorem short_c1_stability (f : ℕ → E → E) (x y : ℕ → E)
    (s : ℕ → Set E) (N : ℕ) {K D : ℝ} (hK : 1≤K) (hD : 0≤D)
    (hx : ∀ t<N,f t (x t)=x (t+1)) (hy : ∀ t<N,f t (y t)=y (t+1))
    (hxs : ∀ t<N,x t∈s t) (hys : ∀ t<N,y t∈s t)
    (hs : ∀ t<N,Convex ℝ (s t))
    (hf : ∀ t<N,∀ a∈s t,DifferentiableAt ℝ (f t) a)
    (hff : ∀ t<N,∀ a∈s t,DifferentiableAt ℝ (fderiv ℝ (f t)) a)
    (hfirst : ∀ t<N,∀ a∈s t,‖fderiv ℝ (f t) a‖≤K)
    (hsecond : ∀ t<N,∀ a∈s t,‖fderiv ℝ (fderiv ℝ (f t)) a‖≤D) :
    (∀ t≤N,‖y t-x t‖≤K^t*‖y 0-x 0‖) ∧
    ‖fderiv ℝ (iterate f N) (y 0)-fderiv ℝ (iterate f N) (x 0)‖≤
      N*D*K^(2*N)*‖y 0-x 0‖ := by
…

Mentions: OAI.SmoothObstruction.ShortDerivative.iterate

theorem OAI.SmoothObstruction.ShortDerivative.uniform_short_boundary line 315

Source documentation

Bootstrap nearby genuine local-map orbits into the carried domains, using only one-sided C2 bounds on a convex closed model (in particular a half-space). No extension across the boundary is assumed. The only smallness required is C^N times the initial displacement; no long-iterate derivative estimate or continued domain membership is assumed.

theorem uniform_short_boundary (f : ι → E → E) (K U : ι → Set E)
    (H : Set E) (hK : ∀ i,IsCompact (K i)) (hU : ∀ i,IsOpen (U i))
    (hH : IsClosed H) (hconvH : Convex ℝ H) (hKU : ∀ i,K i⊆U i)
    (huniq : ∀ i,UniqueDiffOn ℝ (U i∩H))
    (hf : ∀ i,ContDiffOn ℝ ∞ (f i) (U i∩H)) :
    ∃ r C : ℝ,0 < r ∧ 1 ≤ C ∧ ∀ (a : ℕ → ι) (x y : ℕ → E) (N : ℕ),
      (∀ t<N,x t∈K (a t)) →
      (∀ t<N,x t∈interior H ∧ y t∈interior H) →
      (∀ t<N,f (a t) (x t)=x (t+1)) →
      (∀ t<N,f (a t) (y t)=y (t+1)) →
      C^N*‖y 0-x 0‖ ≤ r →
      (∀ t≤N,‖y t-x t‖ ≤ C^t*‖y 0-x 0‖) ∧
…

theorem OAI.SmoothObstruction.ShortDerivative.uniform_short_interior line 383

Source documentation

theorem uniform_short_interior (f : ι → E → E) (K U : ι → Set E)
    (H : Set E) (hK : ∀ i,IsCompact (K i)) (hU : ∀ i,IsOpen (U i))
    (hH : IsClosed H) (hconvH : Convex ℝ H) (hKU : ∀ i,K i⊆U i)
    (huniq : ∀ i,UniqueDiffOn ℝ (U i∩H))
    (hf : ∀ i,ContDiffOn ℝ ∞ (f i) (U i∩H))
    (hmaps : ∀ i,MapsTo (f i) (U i∩interior H) (interior H)) :
    ∃ r C : ℝ,0 < r ∧ 1 ≤ C ∧ ∀ (a : ℕ → ι) (x y : ℕ → E) (N : ℕ),
      (∀ t<N,x t∈K (a t)) →
      (∀ t<N,x t∈interior H) → y 0∈interior H →
      (∀ t<N,f (a t) (x t)=x (t+1)) →
      (∀ t<N,f (a t) (y t)=y (t+1)) →
      C^N*‖y 0-x 0‖ ≤ r →
…

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_short_comparison line 459

Source documentation

The C1 comparison is for genuine manifold orbits in one fixed carried chart sequence. Neither continued chart membership nor staying in the interior is assumed for the perturbed orbit: both are proved. The constants are uniform over every sequence of reference charts, orbit and length.

theorem actual_short_comparison (hclosed : IsClosed (range I))
    (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
    ∃ r C : ℝ,0 < r ∧ 1 ≤ C ∧ ∀ (c : ℕ → ι) (x y : M) (N : ℕ),
      (∀ t≤N,S^[t] x∈K (c t)) → I.IsInteriorPoint x → I.IsInteriorPoint y →
      y∈(chartAt H (a (c 0))).source →
      C ^ N*‖(extChartAt I (a (c 0))) y-(extChartAt I (a (c 0))) x‖ ≤ r →
      (∀ t≤N,S^[t] y∈(chartAt H (a (c t))).source ∧
        ‖(extChartAt I (a (c t))) (S^[t] y)-(extChartAt I (a (c t))) (S^[t] x)‖ ≤
          C ^ t*‖(extChartAt I (a (c 0))) y-(extChartAt I (a (c 0))) x‖) ∧
      ‖fderiv ℝ (ShortDerivative.iterate (fun t => localMap I S (a (c t)) (a (c (t+1)))) N)
          ((extChartAt I (a (c 0))) y)-
…

Mentions: OAI.SmoothObstruction.ShortDerivative.iterate, OAI.SmoothObstruction.ManifoldCoordinates.localMap