WeightedZonotope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

All-word intervals fit in a maximizing box

The normalized coordinate bound controls the whole Minkowski sum of the weighted word intervals, uniformly over every letter weighting and scale.

def OAI.PolycyclicRecognition.weightedZonotope line 20
Source documentation
The sum of all weighted intervals from the fixed vector list.
```
def weightedZonotope (v : I → Fin n → ℝ) (w : I → ℝ) (r R : ℝ) : Set (Fin n → ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.exists_uniform_zonotope_box_bound line 26
Source documentation
The entire all-word interval sum is contained in a fixed enlargement of any maximizing scaled basis box.
```
theorem exists_uniform_zonotope_box_bound (v : I → Fin n → ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (w : I → ℝ) (b : Fin n → I),
      IsMaximizingColumnBasis v w b → ∀ (r R : ℝ), 0 ≤ r → 0 ≤ R →
        weightedZonotope v w r R ⊆ weightedCoordinateBox v w b r (C * R) := by
…
```
Mentions: OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.weightedZonotope, OAI.PolycyclicRecognition.weightedCoordinateBox
theorem OAI.PolycyclicRecognition.weightedCoordinateBox_subset_zonotope line 65
Source documentation
Conversely every selected box lies in a fixed enlargement of the all-word interval sum. This direction does not need maximality.
```
theorem weightedCoordinateBox_subset_zonotope (v : I → Fin n → ℝ) (w : I → ℝ)
    (b : Fin n → I) (r R : ℝ) (hR : 0 ≤ R) :
    weightedCoordinateBox v w b r R ⊆ weightedZonotope v w r ((n : ℝ) * R) := by
…
```
Mentions: OAI.PolycyclicRecognition.weightedCoordinateBox, OAI.PolycyclicRecognition.weightedZonotope