TriangularMatrixHeight.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Actual logarithmic height on positive triangular matrices

The logarithms of positive diagonal entries form a group homomorphism. Bounded logarithmic height bounds both diagonal frames and their inverses, which are the hypotheses in the polynomial product estimate.

theorem OAI.PolycyclicRecognition.triangular_mul_diag line 20
def OAI.PolycyclicRecognition.positiveTriangular line 32
Source documentation
Positive invertible upper triangular real matrices, as an actual subgroup.
```
def positiveTriangular (n : ℕ) : Subgroup (Matrix (Fin n) (Fin n) ℝ)ˣ where
…
```
abbrev OAI.PolycyclicRecognition.PositiveTriangular.matrix line 62
theorem OAI.PolycyclicRecognition.PositiveTriangular.upper line 64
theorem OAI.PolycyclicRecognition.PositiveTriangular.diagonal_pos line 66
def OAI.PolycyclicRecognition.PositiveTriangular.diagonal line 69
Source documentation
The diagonal characters with their actual unit values.
```
noncomputable def diagonal : positiveTriangular n →* (Fin n → ℝˣ) where
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular
theorem OAI.PolycyclicRecognition.PositiveTriangular.diagonal_val line 78
def OAI.PolycyclicRecognition.PositiveTriangular.height line 82
Source documentation
The logarithmic diagonal is a homomorphism to an additive real vector space.
```
noncomputable def height : positiveTriangular n →* Multiplicative (Fin n → ℝ) where
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular
theorem OAI.PolycyclicRecognition.PositiveTriangular.height_apply line 96
def OAI.PolycyclicRecognition.PositiveTriangular.frame line 100
Source documentation
The exact diagonal frame used to normalize triangular products.
```
noncomputable def frame (g : positiveTriangular n) : (Matrix (Fin n) (Fin n) ℝ)ˣ :=
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular
theorem OAI.PolycyclicRecognition.PositiveTriangular.frame_norm_le_exp line 104
Source documentation
A bounded height bounds the frame and its inverse by the same exponential.
```
theorem frame_norm_le_exp (g : positiveTriangular n) {M : ℝ}
    (hg : ‖(height g).toAdd‖ ≤ M) :
    ‖(frame g : Matrix (Fin n) (Fin n) ℝ)‖ ≤ Real.exp M ∧
    ‖(↑(frame g)⁻¹ : Matrix (Fin n) (Fin n) ℝ)‖ ≤ Real.exp M := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.PositiveTriangular.height, OAI.PolycyclicRecognition.PositiveTriangular.frame