FrameWeightRigidity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

From minor weights to an invariant subspace

In a genuine Grassmannian coordinate chart, the pivot rows of a frame form the identity. A one-row replacement minor is then exactly the corresponding graph coordinate. The single-weight minor conclusion therefore forces the frame to intertwine the two diagonal operators.

def OAI.DukePrimeDegree.replaceFramePivot line 20
lemma OAI.DukePrimeDegree.replaceFramePivot_self line 23
lemma OAI.DukePrimeDegree.replaceFramePivot_other line 27
lemma OAI.DukePrimeDegree.frameMinor_replace_pivot line 35
lemma OAI.DukePrimeDegree.replaced_pivot_weight_ne line 56

theorem OAI.DukePrimeDegree.frame_entry_eq_zero_of_minor_weights line 74

Source documentation

In a normalized frame chart, a graph coefficient joining unequal diagonal weights must vanish.

theorem frame_entry_eq_zero_of_minor_weights {n k : ℕ}
    (B : Matrix (Fin n) (Fin k) ℝ) (p : Fin k ↪ Fin n)
    (hp : B.submatrix p id = 1)
    (a : Fin n → ℝ) (ha : ∀ i, a i ≠ 0)
    (hminor : ∀ q, (∏ u, a (q u)) ≠ ∏ u, a (p u) → frameMinor B q = 0)
    (i : Fin n) (j : Fin k) (hne : a i ≠ a (p j)) : B i j = 0 := by
…

Mentions: OAI.DukePrimeDegree.frameMinor

theorem OAI.DukePrimeDegree.diagonal_mul_frame_eq_frame_mul_diagonal line 94

Source documentation

The frame intertwines the ambient diagonal operator and its pivot restriction. Consequently its column subspace is invariant.

theorem diagonal_mul_frame_eq_frame_mul_diagonal {n k : ℕ}
    (B : Matrix (Fin n) (Fin k) ℝ) (p : Fin k ↪ Fin n)
    (hp : B.submatrix p id = 1)
    (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 * Matrix.diagonal (fun u => a (p u)) := by
…

Mentions: OAI.DukePrimeDegree.frameMinor

theorem OAI.DukePrimeDegree.ae_normalized_frame_diagonal_intertwining line 110

Source documentation

A finite invariant law of normalized frames is supported on frames whose column spaces are invariant under the actual diagonal operator. The frame covariance includes the genuine change of basis on its columns.

theorem ae_normalized_frame_diagonal_intertwining
    {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))
    (p : Fin k ↪ Fin n) (hp : ∀ᵐ x ∂μ, (B x).submatrix p id = 1)
    (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 ∂μ, Matrix.diagonal a * B x =
…