LocalCertificateRadius.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Affine.LocalCertificate.exists_radius line 17
Source documentation
A fixed-minimum certificate supplies a common neighborhood radius with both approximation throughout the band and the stronger offset decay used by the interval-gluing construction.
```
theorem LocalCertificate.exists_radius
    {d : ℕ} (hd : 0 < d) {a b t : ℝ} {E : (Fin d → ℝ) → ℝ}
    (C : LocalCertificate d a b t E) :
    ∃ ρ : ℝ, 0 < ρ ∧
      (∀ L ∈ C.labels,
        L.offset =o[𝓝[>] (0 : ℝ)] (fun h => h ^ (t + ρ))) ∧
      ∀ s : ℝ, |s - t| < ρ → ApproximatesAtMinimum C.labels a b s E := by
…
```
Mentions: OAI.Problem326.Affine.LocalCertificate, OAI.Problem326.Affine.ApproximatesAtMinimum