GlueLocalCertificates.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Affine.glue_localCertificates line 16
Source documentation
The exact gluing interface used by the dimension induction. Local certificates are first extended to nearby minimum levels with a common stronger decay radius, then the finite interval construction glues them into one full certificate.
```
theorem glue_localCertificates {d : ℕ} (hd : 0 < d)
    {a b : ℝ} (hab : a ≤ b) (E : (Fin d → ℝ) → ℝ)
    (hlocal : ∀ t : ℝ, a ≤ t → t ≤ b →
      Nonempty (LocalCertificate d a b t E)) :
    Nonempty (FullCertificate d a b E) := by
…
```
Mentions: OAI.Problem326.Affine.LocalCertificate, OAI.Problem326.Affine.FullCertificate