MetricIteration.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Finite analytic coordinate iteration

The maps are defined everywhere. Smoothness and metric estimates are local statements on a fixed open set, derived from analytic field bounds.

def OAI.RegularPointCoordinates.metricIterate line 24
Source documentation
The actual coordinate iteration, starting from the identity.
```
def metricIterate (v : ℕ → E → E) : ℕ → E → E
  | 0 => id
  | i + 1 => fun x => metricIterate v i x +
      operatorInverseTranspose (fderiv ℝ (metricIterate v i) x) (v i x)
```
Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose
theorem OAI.RegularPointCoordinates.metricIterate_zero line 29
theorem OAI.RegularPointCoordinates.metricIterate_succ line 31
theorem OAI.RegularPointCoordinates.contDiffAt_normalizedCoordinates line 37
Source documentation
Local smoothness is preserved by frozen normalization.
```
theorem contDiffAt_normalizedCoordinates {m : ℕ} {r : ℝ} (T : E ≃L[ℝ] E)
    (x : E) {h : E → E} (hh : ContDiffAt ℝ m h x) :
    ContDiffAt ℝ m (normalizedCoordinates r T x h) 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.normalizedCoordinates
theorem OAI.RegularPointCoordinates.contDiffAt_normalizedCovector line 48
Source documentation
Local smoothness is preserved by the dual frozen normalization.
```
theorem contDiffAt_normalizedCovector {m : ℕ} {r : ℝ} (T : E ≃L[ℝ] E)
    (x : E) {v : E → E} (hv : ContDiffAt ℝ m v x) :
    ContDiffAt ℝ m (normalizedCovector r T x v) 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.normalizedCovector

theorem OAI.RegularPointCoordinates.normalizedCoordinates_dyadic line 62

Source documentation

The same map at the next radius is obtained by a contracting metric change and dyadic output scaling.

theorem normalizedCoordinates_dyadic {r : ℝ} (hr : r ≠ 0)
    (T U : E ≃L[ℝ] E) (x : E) (h : E → E) :
    normalizedCoordinates (r / 2) U x h = fun z => (2 : ℝ) •
      normalizedCoordinates r T x h
        ((1 / 2 : ℝ) • (((T : E →L[ℝ] E) ∘L (U.symm : E →L[ℝ] E)) z)) := by
…

Mentions: OAI.RegularPointCoordinates.normalizedCoordinates

theorem OAI.RegularPointCoordinates.iteratedFDeriv_normalized_update line 80

Source documentation

Positive-order jets of the actual normalized update agree with those of the normalized inverse-transpose update. The centering error is a constant and the covariance identity is needed only locally.

theorem iteratedFDeriv_normalized_update {r : ℝ} (hr : r ≠ 0)
    (T : E ≃L[ℝ] E) (x : E) (h v : E → E) (e : E → E ≃L[ℝ] E)
    {m : ℕ} (hm : 0 < m) (hh : ContDiffAt ℝ (m + 1) h x)
    (hv : ContDiffAt ℝ m v x)
    (he : ∀ᶠ y in 𝓝 x, fderiv ℝ h y = (e y : E →L[ℝ] E)) :
    iteratedFDeriv ℝ m (normalizedCoordinates r T x
      (fun y => h y + operatorInverseTranspose (fderiv ℝ h y) (v y))) 0 =
    iteratedFDeriv ℝ m (fun z => normalizedCoordinates r T x h z +
      operatorInverseTranspose (fderiv ℝ (normalizedCoordinates r T x h) z)
        (normalizedCovector r T x v z)) 0 := by
…

Mentions: OAI.RegularPointCoordinates.normalizedCoordinates, OAI.RegularPointCoordinates.operatorInverseTranspose, OAI.RegularPointCoordinates.normalizedCovector

theorem OAI.RegularPointCoordinates.exists_frozen_normalized_jet_step line 130

Source documentation

The next frozen metric preserves a requested jet order, from only source orders through m+1. The small parameter is independent of m.

theorem exists_frozen_normalized_jet_step
    {A B Cv : ℝ} (hA : 1 ≤ A) (hB : 0 < B) (hCv : 0 ≤ Cv) :
    ∃ epsilon : ℝ, 0 < epsilon ∧
      ∀ (r : ℝ), 0 < r → ∀ (T U : E ≃L[ℝ] E) (x : E) (h v : E → E)
        (e : E → E ≃L[ℝ] E) (m : ℕ), 2 ≤ m →
      ContDiffAt ℝ (m + 1) h x → ContDiffAt ℝ m v x →
      (∀ᶠ y in 𝓝 x, fderiv ℝ h y = (e y : E →L[ℝ] E)) →
      (∀ xi, A⁻¹ * ‖T xi‖ ^ 2 ≤ ‖fderiv ℝ h x xi‖ ^ 2) →
      (∀ xi, ‖T xi‖ ≤ ‖U xi‖) →
      (∀ q, 2 ≤ q → q ≤ m + 1 →
        ‖iteratedFDeriv ℝ q (normalizedCoordinates r T x h) 0‖ ≤
          B ^ (q - 1) * (q.factorial : ℝ) ^ 3) →
…

Mentions: OAI.RegularPointCoordinates.normalizedCoordinates

def OAI.RegularPointCoordinates.iterationRadius line 189
Source documentation
Dyadic radii, written without integer exponents.
```
def iterationRadius (r0 : ℝ) (i : ℕ) : ℝ := r0 / (2 : ℝ) ^ i
```
theorem OAI.RegularPointCoordinates.iterationRadius_pos line 191
theorem OAI.RegularPointCoordinates.iterationRadius_succ line 194
structure OAI.RegularPointCoordinates.AnalyticIterationData line 204
Source documentation
Explicit analytic inputs for the finite iteration. The mass and principal comparisons come before construction of the coordinate maps; none of the fields below assumes a coordinate metric or a scalar error recurrence.
```
structure AnalyticIterationData (Ω : Set E) (r0 T F B epsilon : ℝ) where
…
```

theorem OAI.RegularPointCoordinates.exists_local_jacobian_family line 242

Source documentation

An invertible Jacobian representative may be selected locally from coercivity on an open set. No smoothness of the selected representative is needed: it agrees with the actual Jacobian throughout the set.

theorem exists_local_jacobian_family [FiniteDimensional ℝ E]
    {Ω : Set E} (hΩ : IsOpen Ω) (h : E → E) (T : E → E ≃L[ℝ] E)
    {A : ℝ} (hA : 1 ≤ A)
    (hlower : ∀ x ∈ Ω, ∀ xi, A⁻¹ * ‖T x xi‖ ^ 2 ≤ ‖fderiv ℝ h x xi‖ ^ 2) :
    ∃ e : E → E ≃L[ℝ] E, ∀ x ∈ Ω,
      ∀ᶠ y in 𝓝 x, fderiv ℝ h y = (e y : E →L[ℝ] E) := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_id_of_two_le line 260
Source documentation
The identity starts the iteration with all higher jets zero.
```
theorem norm_iteratedFDeriv_id_of_two_le {m : ℕ} (hm : 2 ≤ m) (x : E) :
    ‖iteratedFDeriv ℝ m (id : E → E) x‖ = 0 := by
…
```
theorem OAI.RegularPointCoordinates.exists_small_metric_iteration_parameter line 272
Source documentation
Both the all-order jet threshold and the metric error threshold can be met by a single positive parameter.
```
theorem exists_small_metric_iteration_parameter {C T delta : ℝ}
    (hT : 0 < T) (hdelta : 0 < delta) :
    ∃ epsilon : ℝ, 0 < epsilon ∧ epsilon ≤ 1 ∧ epsilon ≤ delta ∧
      scalarMetricErrorCoefficient (pointwiseIterationCoefficient C) T epsilon ≤ (2 * T)⁻¹ := by
…
```
Mentions: OAI.RegularPointCoordinates.scalarMetricErrorCoefficient, OAI.RegularPointCoordinates.pointwiseIterationCoefficient
theorem OAI.RegularPointCoordinates.exists_analytic_metric_iteration line 296
Source documentation
All finite stages are smooth on the given open set, coercive, and have the same normalized higher-jet bounds. The constants are chosen in order: metric bootstrap 4T, inverse constant, fixed jet base, then a single positive defect parameter.
```
theorem exists_analytic_metric_iteration [FiniteDimensional ℝ E]
    {T F B : ℝ} (hT : 1 ≤ T) (hF : 1 ≤ F) (hB : 1 ≤ B) :
    ∃ epsilon : ℝ, 0 < epsilon ∧ epsilon ≤ 1 ∧
      ∀ (Ω : Set E), IsOpen Ω → ∀ (r0 : ℝ), 0 < r0 →
      ∀ d : AnalyticIterationData (E := E) Ω r0 T F B epsilon,
…
```
Mentions: OAI.RegularPointCoordinates.AnalyticIterationData
theorem OAI.RegularPointCoordinates.exists_analytic_metric_iteration_invertible line 471
Source documentation
Every Jacobian produced by the analytic iteration is a unit. In finite dimension this is a consequence of the proved metric lower bound, rather than an additional input to the construction.
```
theorem exists_analytic_metric_iteration_invertible [FiniteDimensional ℝ E]
    {T F B : ℝ} (hT : 1 ≤ T) (hF : 1 ≤ F) (hB : 1 ≤ B) :
    ∃ epsilon : ℝ, 0 < epsilon ∧ epsilon ≤ 1 ∧
      ∀ (Ω : Set E), IsOpen Ω → ∀ (r0 : ℝ), 0 < r0 →
      ∀ d : AnalyticIterationData (E := E) Ω r0 T F B epsilon,
…
```
Mentions: OAI.RegularPointCoordinates.AnalyticIterationData