IterationOpenness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Direct openness of the analytic coordinate limit

The frozen metrics increase, and the zeroth iterate is the identity. Consequently every finite iterate has the same lower differential bound. The uniform tail bound then passes the open-image property to the limit.

theorem OAI.RegularPointCoordinates.FiniteIterationControl.inverse_differential_bound line 22
Source documentation
The lower bound on the derivative is uniform in the iteration index.
```
theorem FiniteIterationControl.inverse_differential_bound
    {Ω : Set (Euclidean n)} {r0 T F B epsilon : ℝ}
    {d : AnalyticIterationData Ω r0 T F B epsilon}
    (hc : FiniteIterationControl d) (hT : 1 ≤ T)
    (i : ℕ) (x : Euclidean n) (hx : x ∈ Ω) (v : Euclidean n) :
    ‖v‖ ≤ (4*T)*‖fderiv ℝ (metricIterate d.correction i) x v‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.AnalyticIterationData, OAI.RegularPointCoordinates.FiniteIterationControl, OAI.RegularPointCoordinates.metricIterate

theorem OAI.RegularPointCoordinates.exists_analytic_iteration_open_limit_chart line 47

Source documentation

The analytic iteration produces an open limit without a separate invariance-of-domain premise.

theorem exists_analytic_iteration_open_limit_chart
    {X : Type*} [MetricSpace X] {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.Euclidean, OAI.RegularPointCoordinates.AnalyticIterationData, OAI.RegularPointCoordinates.IterationPairGeometry, OAI.RegularPointCoordinates.HasOpenBilipschitzChart