ExponentialBoxCoordinates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exponential boxes and the concrete weighted coordinate boxes

The sup-norm definition of a box agrees with the previously measured linear image of a cube. This identifies group boxes with images of sets having the exact determinant volume, without treating the two coordinate systems as an extra hypothesis.

theorem OAI.PolycyclicRecognition.exponentialCoordinateBox_eq_cube_image line 25
Source documentation
A single basis identifies its exponential box with the exponential image of the standard coordinate cube.
```
theorem exponentialCoordinateBox_eq_cube_image {n : ℕ}
    (Exp : L → G) (b : Basis (Fin n) ℝ L) (R : ℝ) (hR : 0 ≤ R) :
    exponentialCoordinateBox Exp b R =
      (Exp ∘ b.equivFun.symm) '' Set.Icc (fun _ => -R) (fun _ => R) := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox
theorem OAI.PolycyclicRecognition.scaledColumnMatrix_eq_basis_toMatrix line 44
Source documentation
Matrix of the scaled word basis in the fixed ambient coordinates.
```
theorem scaledColumnMatrix_eq_basis_toMatrix
    (X : I → L) (S : Finset (FreeMagma I))
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (β : WordBasisSelections X S)
    (cost : S → ℝ) (r : ℝ) :
    scaledColumnMatrix (wordListCoordinates X S b₀) cost β.val r =
      b₀.toMatrix (exponentialRescaleBasis (WordBasisSelections.basis X S β)
        (fun i => cost (β.val i)) r) := by
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.scaledColumnMatrix, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.basis_image_cube line 60

Source documentation

A basis sends its coordinate cube to exactly the vectors with bounded coordinates, including dimension zero when R is nonnegative.

theorem basis_image_cube {n : ℕ} (b₀ b : Basis (Fin n) ℝ L)
    (R : ℝ) (hR : 0 ≤ R) :
    (Matrix.toLin' (b₀.toMatrix b)) '' Set.Icc (fun _ => -R) (fun _ => R) =
      b₀.equivFun '' {x : L | ‖b.equivFun x‖ ≤ R} := by
…

theorem OAI.PolycyclicRecognition.exponentialCoordinateBox_eq_weighted_image line 85
Source documentation
The group box is the exponential image of the exact weighted coordinate box used by the determinant-volume theorem.
```
theorem exponentialCoordinateBox_eq_weighted_image
    (X : I → L) (S : Finset (FreeMagma I))
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) (β : WordBasisSelections X S)
    (cost : S → ℝ) (r R : ℝ) (hR : 0 ≤ R) (Exp : L → G) :
    exponentialCoordinateBox Exp
      (exponentialRescaleBasis (WordBasisSelections.basis X S β)
        (fun i => cost (β.val i)) r) R =
    (Exp ∘ b₀.equivFun.symm) '' weightedCoordinateBox
      (wordListCoordinates X S b₀) cost β.val r R := by
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.weightedCoordinateBox, OAI.PolycyclicRecognition.wordListCoordinates