SupportPolytope.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The finite covector body of the segment support norm

The positive-part formula is the maximum of finitely many actual linear forms, obtained by choosing subsets of the weights in a word basis. This constructs the support body used to define the finite height-label group.

def OAI.PolycyclicRecognition.SupportDatum.supportForm line 28
Source documentation
A linear piece in the positive-part expression for segment support.
```
def supportForm (b : B) (S : Finset I) : W →L[ℝ] ℝ :=
…
```
theorem OAI.PolycyclicRecognition.SupportDatum.supportForm_apply line 32
def OAI.PolycyclicRecognition.SupportDatum.supportForms line 37
Source documentation
The explicitly finite set of all linear pieces.
```
def supportForms : Finset (W →L[ℝ] ℝ) := by
…
```
theorem OAI.PolycyclicRecognition.SupportDatum.mem_supportForms line 42
theorem OAI.PolycyclicRecognition.SupportDatum.supportForm_le line 46
theorem OAI.PolycyclicRecognition.SupportDatum.exists_supportForm_eq line 61
Source documentation
Every support value is attained by a member of the finite covector set.
```
theorem exists_supportForm_eq (w : W) :
    ∃ φ ∈ D.supportForms, φ w = D.segmentSupport w := by
…
```
theorem OAI.PolycyclicRecognition.SupportDatum.supportForms_le line 78
theorem OAI.PolycyclicRecognition.SupportDatum.supportForms_separate line 85
Source documentation
The finite pieces still separate the entire height space.
```
theorem supportForms_separate (w : W)
    (hw : ∀ φ ∈ D.supportForms, φ w = 0) : w = 0 := by
…
```
theorem OAI.PolycyclicRecognition.SupportDatum.supportForms_span line 91
Source documentation
The concrete support forms span the continuous dual height space.
```
theorem supportForms_span : Submodule.span ℝ (D.supportForms : Set (W →L[ℝ] ℝ)) = ⊤ := by
…
```
theorem OAI.PolycyclicRecognition.SupportDatum.mem_supportBody_iff line 113
Source documentation
The finite convex body is exactly the set of covectors dominated by the segment support. This is the polarity step used to detect its symmetries.
```
theorem mem_supportBody_iff (φ : W →L[ℝ] ℝ) :
    φ ∈ convexHull ℝ (D.supportForms : Set (W →L[ℝ] ℝ)) ↔
      ∀ w, φ w ≤ D.segmentSupport w := by
…
```