ConePolarTemplate.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Polar templates and their exact vanishing directions

The compact unit slice of the negative polar has support zero on the cone and strictly positive support at every functional outside the cone. These are the widths used in the cone-ideal covering argument.

def OAI.PolycyclicRecognition.conePolarTemplate line 25
Source documentation
The unit-ball slice of the negative polar of the closed weight cone.
```
def conePolarTemplate (C : ProperCone ℝ (StrongDual ℝ W)) : Set W :=
…
```
theorem OAI.PolycyclicRecognition.zero_mem_conePolarTemplate line 29
theorem OAI.PolycyclicRecognition.isCompact_conePolarTemplate line 33
theorem OAI.PolycyclicRecognition.convex_conePolarTemplate line 44
theorem OAI.PolycyclicRecognition.exists_pos_on_conePolarTemplate line 60
Source documentation
Separation and rescaling supply a point with strictly positive evaluation.
```
theorem exists_pos_on_conePolarTemplate (C : ProperCone ℝ (StrongDual ℝ W))
    {β : StrongDual ℝ W} (hβ : β ∉ C) :
    ∃ x ∈ conePolarTemplate C, 0 < β x := by
…
```
Mentions: OAI.PolycyclicRecognition.conePolarTemplate
def OAI.PolycyclicRecognition.conePolarWidth line 79
theorem OAI.PolycyclicRecognition.conePolarWidth_nonneg line 82
theorem OAI.PolycyclicRecognition.conePolarWidth_eq_zero line 87
theorem OAI.PolycyclicRecognition.conePolarWidth_pos line 97
theorem OAI.PolycyclicRecognition.conePolarWidth_eq_zero_iff line 103
theorem OAI.PolycyclicRecognition.conePolarWidth_smul line 110
Source documentation
Dilating the polar template multiplies every supporting width by the same scalar, so a maximizing word basis works for every positive radius.
```
theorem conePolarWidth_smul (C : ProperCone ℝ (StrongDual ℝ W))
    (β : StrongDual ℝ W) {a : ℝ} (ha : 0 ≤ a) :
    sSup (β '' ((fun x : W => a • x) '' conePolarTemplate C)) =
      a * conePolarWidth C β := by
…
```
Mentions: OAI.PolycyclicRecognition.conePolarTemplate, OAI.PolycyclicRecognition.conePolarWidth