OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactSupportSlack.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_above_compact_support line 16

   Source documentation

   A compact template strictly inside an open domain has a point above its support in every nonzero weight direction. This supplies the interior switch hypothesis for each finitely generated probe path.

   theorem exists_above_compact_support
       {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
       (β : W →L[ℝ] ℝ) (hβ : β ≠ 0)
       (E U : Set W) (hE : IsCompact E) (hEne : E.Nonempty)
       (hU : IsOpen U) (hEU : E ⊆ U) :
       ∃ y ∈ U, sSup (β '' E) < β y := by
   …