AffineCertificateGluing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.Affine.fullCertificate_glue line 12
Source documentation
The complete gluing argument in the exact certificate interface consumed by fullCertificate_of_local_and_glue. No gluing assumption remains in this theorem.
```
theorem fullCertificate_glue
    (d : ℕ) (hd : 0 < d) (a b : ℝ) (E : (Fin d → ℝ) → ℝ)
    (hab : a < b) (_hE : ∀ r, Cube a b r → 0 < E r)
    (hlocal : ∀ t : ℝ, a ≤ t → t ≤ b → Nonempty (LocalCertificate d a b t E)) :
    Nonempty (FullCertificate d a b E) := by
…
```
Mentions: OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.LocalCertificate, OAI.Problem326.Affine.FullCertificate

theorem OAI.Problem326.Affine.fullCertificate_of_local_constructor line 39

Source documentation

The full affine approximation theorem now reduces solely to constructing fixed-minimum certificates from lower-dimensional full certificates.

theorem fullCertificate_of_local_constructor
    (construct : ∀ d : ℕ, 0 < d →
      (∀ k : ℕ, k < d → ∀ a b : ℝ, ∀ E : (Fin k → ℝ) → ℝ,
        a < b → (∀ r, Cube a b r → 0 < E r) → Nonempty (FullCertificate k a b E)) →
      ∀ a b : ℝ, ∀ E : (Fin d → ℝ) → ℝ,
        a < b → (∀ r, Cube a b r → 0 < E r) →
        ∀ t : ℝ, a ≤ t → t ≤ b → Nonempty (LocalCertificate d a b t E)) :
    ∀ d : ℕ, ∀ a b : ℝ, ∀ E : (Fin d → ℝ) → ℝ,
      a < b → (∀ r, Cube a b r → 0 < E r) → Nonempty (FullCertificate d a b E) :=
…

Mentions: OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.FullCertificate, OAI.Problem326.Affine.LocalCertificate