NormalizedFrame.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Diagonal invariance of an actual frame

A nonzero pivot minor gives a concrete normalized frame, by multiplying on the right by that minor's inverse. The one-weight conclusion for the original minors then makes its column space diagonal-invariant. The pivot may be chosen separately at each point; no invariant chart or measurable choice of the pivot is assumed.

lemma OAI.DukePrimeDegree.frame_submatrix_mul_right line 22
lemma OAI.DukePrimeDegree.frameMinor_mul_right line 29
def OAI.DukePrimeDegree.normalizeFrame line 36
lemma OAI.DukePrimeDegree.normalizeFrame_pivot line 40
lemma OAI.DukePrimeDegree.normalizeFrame_mul_pivot line 46

theorem OAI.DukePrimeDegree.diagonal_mul_frame_of_minor_weights line 53

Source documentation

The change of basis exhibiting invariance is the explicit conjugate of the diagonal on the pivot rows.

theorem diagonal_mul_frame_of_minor_weights {n k : ℕ}
    (B : Matrix (Fin n) (Fin k) ℝ) (p : Fin k ↪ Fin n)
    (hp : frameMinor B p ≠ 0)
    (a : Fin n → ℝ) (ha : ∀ i, a i ≠ 0)
    (hminor : ∀ q, (∏ u, a (q u)) ≠ ∏ u, a (p u) → frameMinor B q = 0) :
    Matrix.diagonal a * B = B *
      ((B.submatrix p id)⁻¹ * Matrix.diagonal (fun u => a (p u)) * B.submatrix p id) := by
…

Mentions: OAI.DukePrimeDegree.frameMinor

theorem OAI.DukePrimeDegree.ae_frame_diagonal_invariant line 76

Source documentation

A finite invariant law of actual full-rank frames is supported on diagonal-invariant column spaces. This derives the invariant-space conclusion from frame covariance, without assuming a fixed pivot chart.

theorem ae_frame_diagonal_invariant
    {Y : Type*} [MeasurableSpace Y] {n k : ℕ}
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (B : Y → Matrix (Fin n) (Fin k) ℝ)
    (hB : ∀ i j, Measurable (fun x => B x i j))
    (hfull : ∀ᵐ x ∂μ, ∃ p : Fin k ↪ Fin n, frameMinor (B x) p ≠ 0)
    (a : Fin n → ℝ) (ha : ∀ i, 0 < a i)
    (R : Y → Matrix (Fin k) (Fin k) ℝ)
    (hR : ∀ᵐ x ∂μ, (R x).det ≠ 0)
    (hcov : ∀ᵐ x ∂μ, B (T x) = Matrix.diagonal a * B x * R x) :
    ∀ᵐ x ∂μ, ∃ C : Matrix (Fin k) (Fin k) ℝ,
…

Mentions: OAI.DukePrimeDegree.frameMinor