WeightedWordNorm.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Norms obtained by assigning costs to group elements

The infimum of the costs of finite product expressions is subadditive. A pre-existing group norm below the costs guarantees separation.

def OAI.PolycyclicRecognition.productCost line 21
Source documentation
Total cost of a product expression.
```
def productCost (l : List G) : ℝ≥0 := (l.map c).sum
```
theorem OAI.PolycyclicRecognition.productCost_nil line 23
theorem OAI.PolycyclicRecognition.productCost_cons line 24
theorem OAI.PolycyclicRecognition.productCost_append line 26
def OAI.PolycyclicRecognition.weightedWordNorm line 33
Source documentation
Weighted word norm, allowing every finite product expression.
```
def weightedWordNorm (g : G) : ℝ≥0 :=
…
```
instance OAI.PolycyclicRecognition.productExpression_nonempty line 36
theorem OAI.PolycyclicRecognition.weightedWordNorm_le_cost line 39
theorem OAI.PolycyclicRecognition.weightedWordNorm_le line 46
theorem OAI.PolycyclicRecognition.weightedWordNorm_one line 49
theorem OAI.PolycyclicRecognition.weightedWordNorm_mul line 52
theorem OAI.PolycyclicRecognition.exists_productCost_lt line 59
theorem OAI.PolycyclicRecognition.productCost_inv_reverse line 69
theorem OAI.PolycyclicRecognition.weightedWordNorm_inv_le line 78
theorem OAI.PolycyclicRecognition.weightedWordNorm_inv line 87
def OAI.PolycyclicRecognition.weightedWordSeminorm line 91
theorem OAI.PolycyclicRecognition.seminorm_product_le_cost line 97
theorem OAI.PolycyclicRecognition.seminorm_le_weightedWordNorm line 105
def OAI.PolycyclicRecognition.weightedWordGroupNorm line 113
Source documentation
A norm below the assigned costs makes the weighted seminorm a norm.
```
def weightedWordGroupNorm (p : GroupNorm G) (hc : ∀ g, p g ≤ c g) : GroupNorm G where
…
```