OAI/Analysis/MassAction/AffineLocalConstructor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Turn the output of the finite layer construction into the canonical local certificate. The finite family admits one common stronger decay exponent.

   theorem localCertificate_of_layers {d : ℕ} (hd : 0 < d)
       {a t b : ℝ} (htb : t < b) (E : (Fin d → ℝ) → ℝ)
       (hE₀ : 0 < E (fun _ => t))
       (hmake : ∀ k : ℕ, 0 < k → k < d → ∀ β : ℝ, t < β → β < b →
         ∃ F : Finset (Label d), LayerCertificate t b E k β F) :
       Nonempty (LocalCertificate d a b t E) := by
   …

   Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.LayerCertificate, OAI.Problem326.Affine.LocalCertificate