IterationLimit.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The metric iteration produces the limiting chart estimates

Finite-stage differential estimates imply geometric increment and Taylor bounds. Pair geometry controls the original coordinates, the selected scale, and the frozen metrics along each coordinate-value segment.

theorem OAI.RegularPointCoordinates.AnalyticIterationData.energy_le line 27

def OAI.RegularPointCoordinates.AnalyticIterationData.withLargerParameter line 34

Source documentation

Increasing the permitted defect changes no maps or metrics.

def withLargerParameter {Ω : Set E} {r0 T F B epsilon delta : ℝ}
    (d : AnalyticIterationData Ω r0 T F B epsilon) (hr0 : 0 < r0)
    (hF : 0 ≤ F) (hB : 0 < B) (hed : epsilon ≤ delta) :
    AnalyticIterationData Ω r0 T F B delta where
…

Mentions: OAI.RegularPointCoordinates.AnalyticIterationData

structure OAI.RegularPointCoordinates.FiniteIterationControl line 71
Source documentation
Only the second normalized jet is needed for the final pair estimate.
```
structure FiniteIterationControl {Ω : Set E} {r0 T F B epsilon : ℝ}
    (d : AnalyticIterationData Ω r0 T F B epsilon) : Prop where
…
```
Mentions: OAI.RegularPointCoordinates.AnalyticIterationData

theorem OAI.RegularPointCoordinates.second_derivative_le_of_normalized_jet line 84

Source documentation

Recover the actual second directional derivative from the normalized second jet, without an ambient operator norm or condition-number loss.

theorem second_derivative_le_of_normalized_jet
    {h : E → E} {x : E} {r B : ℝ} (hr : 0 < r) (T : E ≃L[ℝ] E)
    (hh : ContDiffAt ℝ 2 h x)
    (hjet : ‖iteratedFDeriv ℝ 2 (normalizedCoordinates r T x h) 0‖ ≤ 8 * B)
    (xi : E) :
    ‖fderiv ℝ (fderiv ℝ h) x xi xi‖ ≤ 8 * B / r * ‖T xi‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.normalizedCoordinates

theorem OAI.RegularPointCoordinates.metricIterate_step_le line 110

Source documentation

The correction value and coercivity give a genuine geometric increment bound for the recursively defined maps.

theorem metricIterate_step_le [FiniteDimensional ℝ E]
    {Ω : Set E} {r0 T F B epsilon : ℝ} (d : AnalyticIterationData Ω r0 T F B epsilon)
    (hT : 1 ≤ T) (hF : 0 ≤ F) (hepsilon : 0 ≤ epsilon) (hr0 : 0 < r0)
    (hc : FiniteIterationControl d) (i : ℕ) (x : E) (hx : x ∈ Ω) :
    dist (metricIterate d.correction i x) (metricIterate d.correction (i + 1) x) ≤
      (4 * T) * F * epsilon * iterationRadius r0 i := by
…

Mentions: OAI.RegularPointCoordinates.AnalyticIterationData, OAI.RegularPointCoordinates.FiniteIterationControl, OAI.RegularPointCoordinates.metricIterate, OAI.RegularPointCoordinates.iterationRadius

theorem OAI.RegularPointCoordinates.linear_comparison_of_frozen_metric line 148

Source documentation

A convenient non-sharp constant for converting metric squares to linear separation. It avoids introducing a square root into the final chart ratio.

theorem linear_comparison_of_frozen_metric
    (T : E ≃L[ℝ] E) (J : E →L[ℝ] E) {A G t : ℝ} (hA : 1 ≤ A) (hG : 1 ≤ G)
    (ht : 0 ≤ t) (w : E)
    (hmetric : ∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖J xi‖ ^ 2 ∧
      ‖J xi‖ ^ 2 ≤ A * ‖T xi‖ ^ 2)
    (hlower : G⁻¹ * t ≤ ‖T w‖) (hupper : ‖T w‖ ≤ G * t) :
    (2 * (A * G))⁻¹ * t ≤ ‖J w‖ ∧ ‖J w‖ ≤ 2 * (A * G) * t := by
…

def OAI.RegularPointCoordinates.iterationChartRatio line 182
Source documentation
The chart ratio and pair radius are fixed before the final smallness parameter is chosen.
```
def iterationChartRatio (T G : ℝ) : ℝ := (4 * T) * G
```
def OAI.RegularPointCoordinates.iterationPairMultiplier line 184

theorem OAI.RegularPointCoordinates.exists_iteration_pair_scale line 188

Source documentation

A diameter restriction supplies the required dyadic pair scale.

theorem exists_iteration_pair_scale {r0 L t : ℝ} (hr0 : 0 < r0) (hL : 0 < L)
    (ht : 0 < t) (hdiam : L * t ≤ r0) :
    ∃ i, L * t ≤ iterationRadius r0 i ∧ iterationRadius r0 i ≤ 2 * L * t := by
…

Mentions: OAI.RegularPointCoordinates.iterationRadius

def OAI.RegularPointCoordinates.IterationPairGeometry line 204
Source documentation
Raw geometric information about the original coordinates and frozen metrics. No derivative, increment, or Taylor estimate occurs here.
```
def IterationPairGeometry {X E : Type*} [MetricSpace X]
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (u : X → E) (Ω : Set E) (frozen : ℕ → E → E ≃L[ℝ] E)
    (r0 T B G : ℝ) : Prop :=
…
```

theorem OAI.RegularPointCoordinates.iterationPairGeometry_of_all_scales line 219

Source documentation

Uniform geometric estimates at comparable scales, together with a diameter bound, construct the pair-selected data.

theorem iterationPairGeometry_of_all_scales {X E : Type*} [MetricSpace X]
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    (u : X → E) (Ω : Set E) (frozen : ℕ → E → E ≃L[ℝ] E)
    {r0 T B G : ℝ} (hr0 : 0 < r0) (hT : 1 ≤ T) (hB : 1 ≤ B) (hG : 1 ≤ G)
    (hdiam : ∀ x z : X, iterationPairMultiplier T B G * dist x z ≤ r0)
    (hgeometry : ∀ i x z, x ≠ z →
      iterationPairMultiplier T B G * dist x z ≤ iterationRadius r0 i →
      iterationRadius r0 i ≤ 2 * iterationPairMultiplier T B G * dist x z →
      G⁻¹ * dist x z ≤ ‖frozen i (u x) (u z - u x)‖ ∧
      ‖frozen i (u x) (u z - u x)‖ ≤ G * dist x z ∧
      segment ℝ (u x) (u z) ⊆ Ω ∧
      ∀ y ∈ segment ℝ (u x) (u z),
…

Mentions: OAI.RegularPointCoordinates.iterationPairMultiplier, OAI.RegularPointCoordinates.iterationRadius

theorem OAI.RegularPointCoordinates.exists_limit_dist_bounds_of_analytic_iteration line 246

Source documentation

Analytic iteration bounds and pair geometry supply scale-selected Taylor estimates for the limit.

theorem exists_limit_dist_bounds_of_analytic_iteration
    {Ω : Set (Euclidean n)} {r0 T F B G epsilon : ℝ}
    (d : AnalyticIterationData Ω r0 T F B epsilon)
    (hT : 1 ≤ T) (hF : 1 ≤ F) (hB : 1 ≤ B) (hG : 1 ≤ G)
    (hr0 : 0 < r0) (hepsilon : 0 ≤ epsilon) (hc : FiniteIterationControl d)
    (u : X → Euclidean n) (hu : ∀ x, u x ∈ Ω)
    (hgeometry : IterationPairGeometry u Ω d.frozen r0 T B G)
    (hsmall : 8 * (4 * T) * F * epsilon * iterationPairMultiplier T B G ≤
      (8 * iterationChartRatio T G)⁻¹) :
    ∃ H : X → Euclidean n,
      (∀ x, Tendsto (fun i => metricIterate d.correction i (u x)) atTop (𝓝 (H x))) ∧
      ∀ x z, (4 * iterationChartRatio T G)⁻¹ * dist x z ≤ dist (H x) (H z) ∧
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.AnalyticIterationData, OAI.RegularPointCoordinates.FiniteIterationControl, OAI.RegularPointCoordinates.IterationPairGeometry, OAI.RegularPointCoordinates.iterationPairMultiplier, OAI.RegularPointCoordinates.iterationChartRatio, OAI.RegularPointCoordinates.metricIterate

theorem OAI.RegularPointCoordinates.exists_analytic_iteration_limit_chart line 337

Source documentation

One small parameter controls the analytic iteration, Taylor errors, and limiting tails; invariance of domain gives the open image.

theorem exists_analytic_iteration_limit_chart
    (hIOD : EuclideanInvarianceOfDomain n) {T F B G : ℝ}
    (hT : 1 ≤ T) (hF : 1 ≤ F) (hB : 1 ≤ B) (hG : 1 ≤ G) :
    ∃ epsilon : ℝ, 0 < epsilon ∧ epsilon ≤ 1 ∧
      ∀ (p : X) (Ω : Set (Euclidean n)), IsOpen Ω →
      ∀ (U : Set X), IsOpen U → p ∈ U →
      ∀ (O : Set (Euclidean n)), IsOpen O → O ⊆ Ω → ∀ u : U ≃ₜ O,
      ∀ (r0 : ℝ), 0 < r0 → ∀ d : AnalyticIterationData Ω r0 T F B epsilon,
      IterationPairGeometry (fun x : U => (u x : Euclidean n)) Ω d.frozen r0 T B G →
      HasOpenBilipschitzChart n p := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanInvarianceOfDomain, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.AnalyticIterationData, OAI.RegularPointCoordinates.IterationPairGeometry, OAI.RegularPointCoordinates.HasOpenBilipschitzChart