OAI/Analysis/MassAction/AffineExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.Affine.exists_fullCertificate line 13

   Source documentation

   The full affine approximation certificate, obtained by dimension induction and finite interval gluing. The tolerance need not be continuous.

   theorem exists_fullCertificate :
       ∀ d : ℕ, ∀ a b : ℝ, ∀ E : (Fin d → ℝ) → ℝ,
         a < b → (∀ r, Cube a b r → 0 < E r) →
         Nonempty (FullCertificate d a b E) := by
   …

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