PointwiseMetricIteration.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite pointwise metric iteration

At a fixed point and direction, the map update supplies the metric increment and the diagonal second-derivative recurrence. Field estimates, inverse costs, cumulative budgets, and a leading comparison then control the coordinate metric.

def OAI.RegularPointCoordinates.pointwiseIterationCoefficient line 24
Source documentation
A common coefficient for the linear, inverse, squared, and recurrence errors.
```
def pointwiseIterationCoefficient (C : ℝ) : ℝ := C + 2 * C ^ 2 + 5 * C ^ 4
```
theorem OAI.RegularPointCoordinates.pointwiseIterationCoefficient_bounds line 26
theorem OAI.RegularPointCoordinates.sqrt_weighted_defect line 40

theorem OAI.RegularPointCoordinates.fderiv_clm_update_increment line 46

Source documentation

The first derivative increment of the actual operator-field update.

theorem fderiv_clm_update_increment {h v : E → E} {K : E → E →L[ℝ] E} {x : E}
    (hh : DifferentiableAt ℝ h x) (hK : DifferentiableAt ℝ K x)
    (hv : DifferentiableAt ℝ v x) (xi : E) :
    fderiv ℝ (fun y => h y + K y (v y)) x xi - fderiv ℝ h x xi =
      K x (fderiv ℝ v x xi) + fderiv ℝ K x xi (v x) := by
…

theorem OAI.RegularPointCoordinates.inverse_diagonal_error_le line 58

Source documentation

The inverse linear error is measured by the normalized old diagonal second derivative and the weighted defect.

theorem inverse_diagonal_error_le (K : E →L[ℝ] E) (dual : E → ℝ) (old v : E)
    {C epsilon r q energy : ℝ} (hC : 1 ≤ C)
    (hepsilon : 0 ≤ epsilon) (hepsilon1 : epsilon ≤ 1)
    (hr : 0 < r) (hq : 0 < q) (henergy : 0 ≤ energy)
    (hK : ∀ w, ‖K w‖ ≤ C * dual w)
    (hv : dual v ≤ C * Real.sqrt epsilon * r * Real.sqrt energy) :
    |⟪old, K v⟫_ℝ| ≤ C ^ 2 * (r / q * ‖old‖) * Real.sqrt (energy * q ^ 2) := by
…

theorem OAI.RegularPointCoordinates.pointwise_metric_iteration line 84

Source documentation

The actual maps satisfy the finite metric comparison once their explicit analytic estimates and geometric scalar budgets are supplied.

theorem pointwise_metric_iteration
    (h v : ℕ → E → E) (e : ℕ → E ≃L[ℝ] E)
    (principal : ℕ → E →L[ℝ] E) (dual : ℕ → E → ℝ)
    (x xi : E) (q r z energy : ℕ → ℝ) (k : ℕ)
    {C T epsilon Q : ℝ} (hC : 1 ≤ C) (hT : 1 ≤ T)
    (hepsilon : 0 ≤ epsilon) (hepsilon1 : epsilon ≤ 1) (hQ : 0 ≤ Q)
    (hq : ∀ i, 0 < q i) (hr : ∀ i, 0 < r i)
    (hz : ∀ i, 0 ≤ z i) (henergy : ∀ i, 0 ≤ energy i)
    (hregular : ∀ i < k, ContDiffAt ℝ 3 (h i) x)
    (vregular : ∀ i < k, ContDiffAt ℝ 2 (v i) x)
    (hJacobian : ∀ i < k, fderiv ℝ (h i) x = (e i : E →L[ℝ] E))
    (hupdate : ∀ i < k, h (i + 1) = fun y => h i y +
…