WeightedBoxVolume.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

+# Exact Euclidean volume of the weighted boxes

The determinant separates into the unscaled basis determinant and the exponential of its total weight. This gives the exact exponential volume rate of the coordinate box, before passage to nilpotent exponential charts.

def OAI.PolycyclicRecognition.scaledColumnMatrix line 22
theorem OAI.PolycyclicRecognition.det_scaledColumnMatrix line 26
def OAI.PolycyclicRecognition.weightedCoordinateBox line 36
Source documentation
The coordinate weighted box is an actual linear image of a cube.
```
def weightedCoordinateBox (v : I → Fin n → ℝ) (w : I → ℝ)
    (b : Fin n → I) (r L : ℝ) : Set (Fin n → ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.isCompact_weightedCoordinateBox line 41
theorem OAI.PolycyclicRecognition.volume_weightedCoordinateBox line 47
Source documentation
The exact coordinate-volume formula; in particular, the exponent is the total weight of the selected basis.
```
theorem volume_weightedCoordinateBox (v : I → Fin n → ℝ) (w : I → ℝ)
    (b : Fin n → I) (r L : ℝ) :
    volume (weightedCoordinateBox v w b r L) =
      ENNReal.ofReal |(columnBasisMatrix v b).det| *
        ENNReal.ofReal (Real.exp (r * columnBasisWeight w b)) *
          ENNReal.ofReal (2 * L) ^ n := by
…
```
Mentions: OAI.PolycyclicRecognition.weightedCoordinateBox, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.columnBasisWeight