OAI/Analysis/MassAction/CanonicalLocalConstructor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The lower-dimensional full certificates construct the canonical local certificate in dimension d, with no additional existence hypothesis.

   theorem localCertificate_of_lower_fullCertificates
       (d : ℕ) (hd : 0 < d)
       (ih : ∀ 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 → ℝ) → ℝ)
       (_hab : a < b) (hE : ∀ r, Cube a b r → 0 < E r)
       (t : ℝ) (hat : a ≤ t) (htb : t ≤ b) :
       Nonempty (LocalCertificate d a b t E) := by
   …

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