SupportNorm.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The norm obtained from weighted nilpotent boxes

For a bracket-word basis, each generator occurs with a positive integral multiplicity. Unimodularity says that the corresponding weighted sum of characters is zero. The support exponent of a segment is the maximum, over these bases, of the weighted positive parts of the characters. This finite data yields the support norm identities.

structure OAI.PolycyclicRecognition.SupportDatum line 27
Source documentation
The finite algebraic data of the segment-support formula.
```
structure SupportDatum (W I B : Type*) [AddCommGroup W] [Module ℝ W]
    [Fintype I] [Fintype B] where
…
```
def OAI.PolycyclicRecognition.SupportDatum.basisSupport line 40
Source documentation
The support exponent contributed by one bracket-word basis.
```
noncomputable def basisSupport (b : B) (w : W) : ℝ :=
…
```
def OAI.PolycyclicRecognition.SupportDatum.segmentSupport line 44
Source documentation
The support exponent of the segment from zero to w.
```
noncomputable def segmentSupport (w : W) : ℝ :=
…
```
theorem OAI.PolycyclicRecognition.SupportDatum.basisSupport_nonneg line 48
theorem OAI.PolycyclicRecognition.SupportDatum.basisSupport_le line 51
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_le line 55
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_nonneg line 59
theorem OAI.PolycyclicRecognition.SupportDatum.basisSupport_zero line 64
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_zero line 67
theorem OAI.PolycyclicRecognition.SupportDatum.basisSupport_neg line 72
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_neg line 83
theorem OAI.PolycyclicRecognition.SupportDatum.basisSupport_add_le line 88
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_add_le line 98
theorem OAI.PolycyclicRecognition.SupportDatum.basisSupport_smul_of_nonneg line 106
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_smul_of_nonneg line 117
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_smul line 130
theorem OAI.PolycyclicRecognition.SupportDatum.weight_eq_zero_of_basisSupport_eq_zero line 138
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_eq_zero_iff line 153
theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupport_pos line 165
theorem OAI.PolycyclicRecognition.SupportDatum.normCore line 171
Source documentation
The segment support is an actual real vector-space norm. This construction does not install a new topology on a space carrying an existing norm.
```
theorem normCore : letI : Norm W := ⟨D.segmentSupport⟩; NormedSpace.Core ℝ W := by
…
```