OAI/Analysis/MassAction/CompleteAffine.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.Affine.fullCertificate_exists line 12

   Source documentation

   Full arbitrary-tolerance affine approximation, with both the dimension induction and the finite interval gluing discharged.

   theorem fullCertificate_exists :
       ∀ 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