Coordinates on positive-diagonal lower-triangular matrices

A lower-triangular matrix is determined by its on-or-below-diagonal entries. Reading off these entries identifies the positive-diagonal lower-triangular matrices with the functions on the lower-triangular positions whose diagonal values are positive. This file packages that identification as a homeomorphism for the subtype topologies on both sides, and as a measurable equivalence for the corresponding Borel structures. These are the product coordinates in which the Jacobian of Cholesky reconstruction is computed. The file also reads the determinant of a lower-triangular matrix and the trace of its Gram matrix L * Lᵀ off these coordinates, records how a product over the lower-triangular positions splits into a product over the rows, and combines these into the factorization, one factor per coordinate, of a determinant power times an exponential trace factor that underlies Cholesky-coordinate density computations.

Main declarations

• TauCeti.lowerTriangle — the index type of on-or-below-diagonal positions.
• TauCeti.lowerTriangleMatrix — the lower-triangular matrix with prescribed entries there.
• TauCeti.PosDiagLowerCoordinates — the coordinate functions with positive diagonal values.
• TauCeti.lowerTriangleCoordinatesHomeomorph — the coordinate homeomorphism.
• TauCeti.lowerTriangleCoordinates — its measurable-equivalence form.
• TauCeti.prod_lowerTriangle_diag_rpow_mul_exp_neg_sq — the coordinatewise factorization of a determinant power times an exponential trace factor.

@[reducible, inline]

abbrev TauCeti.lowerTriangle (p : ℕ) : Type

The on-or-below-diagonal positions (i, j), j ≤ i, of a p × p matrix.

Equations

• TauCeti.lowerTriangle p = { ij : Fin p × Fin p // ij.2 ≤ ij.1 }

theorem TauCeti.prod_lowerTriangle_ite {M : Type u_1} [CommMonoid M] {p : ℕ} (F G : Fin p → M) : (∏ ij : lowerTriangle p, if (↑ij).1 = (↑ij).2 then F (↑ij).1 else G (↑ij).1) = ∏ i : Fin p, F i * G i ^ ↑i

A product over the lower-triangular positions of a quantity that depends only on the row index, and only through whether the position is diagonal, collapses to a product over the rows: row i has one diagonal position and i strictly lower ones.

@[reducible, inline]

abbrev TauCeti.PosDiagLowerCoordinates (p : ℕ) : Type

Real functions on the lower-triangular positions whose diagonal values are positive: the coordinate space of TauCeti.PosDiagLowerTriangular p.

Equations

• TauCeti.PosDiagLowerCoordinates p = { x : TauCeti.lowerTriangle p → ℝ // ∀ (i : Fin p), 0 < x ⟨(i, i), ⋯⟩ }

def TauCeti.lowerTriangleMatrix (p : ℕ) : (lowerTriangle p → ℝ) →ₗ[ℝ] Matrix (Fin p) (Fin p) ℝ

The lower-triangular matrix whose on-or-below-diagonal entries are prescribed by x and whose entries above the diagonal vanish.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.lowerTriangleMatrix_apply_of_le {p : ℕ} (x : lowerTriangle p → ℝ) {i j : Fin p} (h : j ≤ i) : (lowerTriangleMatrix p) x i j = x ⟨(i, j), h⟩

@[simp]

theorem TauCeti.lowerTriangleMatrix_apply_of_lt {p : ℕ} (x : lowerTriangle p → ℝ) {i j : Fin p} (h : i < j) : (lowerTriangleMatrix p) x i j = 0

theorem TauCeti.isLowerTriangular_lowerTriangleMatrix {p : ℕ} (x : lowerTriangle p → ℝ) : ((lowerTriangleMatrix p) x).IsLowerTriangular

@[simp]

theorem TauCeti.lowerTriangleMatrix_entries {p : ℕ} {A : Matrix (Fin p) (Fin p) ℝ} (hA : A.IsLowerTriangular) : ((lowerTriangleMatrix p) fun (ij : lowerTriangle p) => A (↑ij).1 (↑ij).2) = A

A lower-triangular matrix is rebuilt from its on-or-below-diagonal entries.

@[simp]

theorem TauCeti.det_lowerTriangleMatrix {p : ℕ} (x : lowerTriangle p → ℝ) : ((lowerTriangleMatrix p) x).det = ∏ i : Fin p, x ⟨(i, i), ⋯⟩

A lower-triangular matrix has determinant the product of its diagonal entries, which in coordinates are the values at the diagonal positions.

theorem TauCeti.trace_lowerTriangleMatrix_mul_transpose {p : ℕ} (x : lowerTriangle p → ℝ) : ((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose).trace = ∑ ij : lowerTriangle p, x ij ^ 2

The trace of the Gram matrix L * Lᵀ of a lower-triangular L is the sum of the squares of the on-or-below-diagonal coordinates of L: the entries above the diagonal contribute nothing.

theorem TauCeti.prod_lowerTriangle_diag_rpow_mul_exp_neg_sq {p : ℕ} (x : lowerTriangle p → ℝ) (hpos : ∀ (i : Fin p), 0 < x ⟨(i, i), ⋯⟩) (d q : ℝ) (c : Fin p → ℝ) (b : ℝ) : ∏ ij : lowerTriangle p, (if (↑ij).1 = (↑ij).2 then c (↑ij).1 * x ⟨((↑ij).1, (↑ij).1), ⋯⟩ ^ (2 * d + ↑p - ↑↑(↑ij).1) else b) * Real.exp (-q * x ij ^ 2) = (∏ i : Fin p, c i * b ^ ↑i) * ((((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose).det ^ d * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i)) * Real.exp (-q * ((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose).trace))

The common algebraic core of Cholesky-coordinate density factorizations. A determinant power, the Cholesky diagonal powers, and an exponential trace factor split into one factor per lower triangular coordinate; c and b supply the diagonal and off-diagonal constants.

theorem TauCeti.continuous_lowerTriangleMatrix {p : ℕ} : Continuous fun (x : lowerTriangle p → ℝ) => (lowerTriangleMatrix p) x

def TauCeti.lowerTriangleCoordinatesHomeomorph (p : ℕ) : PosDiagLowerTriangular p ≃ₜ PosDiagLowerCoordinates p

Reading off the on-or-below-diagonal entries is a homeomorphism from the positive-diagonal lower-triangular matrices to their coordinate space. Its inverse fills the positions above the diagonal with zeros.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.lowerTriangleCoordinatesHomeomorph_apply_coe (p : ℕ) (L : PosDiagLowerTriangular p) (ij : lowerTriangle p) : ↑((lowerTriangleCoordinatesHomeomorph p) L) ij = ↑L (↑ij).1 (↑ij).2

@[simp]

theorem TauCeti.lowerTriangleCoordinatesHomeomorph_symm_apply_coe (p : ℕ) (x : PosDiagLowerCoordinates p) : ↑((lowerTriangleCoordinatesHomeomorph p).symm x) = (lowerTriangleMatrix p) ↑x

@[simp]

theorem TauCeti.lowerTriangleMatrix_lowerTriangleCoordinatesHomeomorph (p : ℕ) (L : PosDiagLowerTriangular p) : (lowerTriangleMatrix p) ↑((lowerTriangleCoordinatesHomeomorph p) L) = ↑L

def TauCeti.lowerTriangleCoordinates (p : ℕ) : PosDiagLowerTriangular p ≃ᵐ PosDiagLowerCoordinates p

The measurable equivalence induced by TauCeti.lowerTriangleCoordinatesHomeomorph.

Equations

• TauCeti.lowerTriangleCoordinates p = (TauCeti.lowerTriangleCoordinatesHomeomorph p).toMeasurableEquiv

@[simp]

theorem TauCeti.lowerTriangleCoordinates_coe (p : ℕ) : ⇑(lowerTriangleCoordinates p) = ⇑(lowerTriangleCoordinatesHomeomorph p)

@[simp]

theorem TauCeti.lowerTriangleCoordinates_symm_coe (p : ℕ) : ⇑(lowerTriangleCoordinates p).symm = ⇑(lowerTriangleCoordinatesHomeomorph p).symm