LocalCertificate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Problem356.LocalGeometry.LocalSupportingCharts line 20
Source documentation
A local exact supporting certificate, with the stationary branches retained as analytic local diffeomorphisms and both domains shrunk to metric balls.
```
structure LocalSupportingCharts (F : E × (E × E) → ℝ)
    (G : E × (E × E) → E × E) (p : E) (s : E × E) where
…
```

theorem OAI.Problem356.LocalGeometry.nonempty_localSupportingCharts line 40

Source documentation

Positive Hessian at the base point, together with separate local branch invertibility, yields the full neighborhood-level supporting certificate.

theorem nonempty_localSupportingCharts [CompleteSpace E] [FiniteDimensional ℝ E]
    {F : E × (E × E) → ℝ} {G : E × (E × E) → E × E}
    {D : E → (E × E) → (E × E) →L[ℝ] ℝ}
    {H : E → (E × E) → (E × E) →L[ℝ] ((E × E) →L[ℝ] ℝ)}
    {p : E} {s : E × E}
    (C : LocalImplicit.AnalyticStationaryCharts G p s)
    (hF : ContDiffAt ℝ ω F (p, s))
    (hD : ∀ᶠ q in 𝓝 (p, s), HasFDerivAt (fun z => F (q.1, z)) (D q.1 q.2) q.2)
    (hH : ∀ᶠ q in 𝓝 (p, s), HasFDerivAt (D q.1) (H q.1 q.2) q.2)
    (hHcont : ContinuousAt (fun q : E × (E × E) => H q.1 q.2) (p, s))
    (hHpos : ∀ v : E × E, v ≠ 0 → 0 < H p s v v)
    (hcompatible : ∀ q : E × (E × E), G q = 0 → D q.1 q.2 = 0) :
…

Mentions: OAI.Problem356.LocalImplicit.AnalyticStationaryCharts

theorem OAI.Problem356.LocalGeometry.LocalSupportingCharts.exists_shrink line 149

Source documentation

A local certificate survives arbitrary further neighborhood restrictions. First shrink the state ball, and only then shrink the parameter ball so that both branches still land in the new state ball. The functions and value are unchanged, so previously established center values are preserved.

theorem LocalSupportingCharts.exists_shrink [CompleteSpace E]
    {F : E × (E × E) → ℝ} {G : E × (E × E) → E × E} {p : E} {s : E × E}
    (C : LocalSupportingCharts F G p s) (rp rs : ℝ) (hp : 0 < rp) (hs : 0 < rs) :
    ∃ D : LocalSupportingCharts F G p s,
      D.charts.central.source ⊆ C.charts.central.source ∩ Metric.ball p rp ∧
      D.charts.stateDomain ⊆ C.charts.stateDomain ∩ Metric.ball s rs ∧
      (D.charts.central : E → E) = C.charts.central ∧
      (D.charts.opposite : E → E) = C.charts.opposite ∧ D.value = C.value := by
…

Mentions: OAI.Problem356.LocalGeometry.LocalSupportingCharts