PluckerCovariance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual frame minors under diagonal transport

The projective coordinates here are determinants of minors of an actual real matrix frame. Changing its basis multiplies every coordinate by the same determinant. Thus diagonal recurrence applies to these coordinates without an assumed projective-action interface.

def OAI.DukePrimeDegree.frameMinor line 23
lemma OAI.DukePrimeDegree.minor_diagonal_frame_mul line 26
lemma OAI.DukePrimeDegree.measurable_frameMinor line 41

theorem OAI.DukePrimeDegree.ae_frame_minors_have_one_diagonal_weight line 56

Source documentation

For a measurably transported real frame, two nonzero minors can have only the same diagonal weight almost everywhere. This is the projective recurrence conclusion in actual matrix coordinates.

theorem ae_frame_minors_have_one_diagonal_weight
    {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))
    (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 ∂μ, ∀ p q : Fin k ↪ Fin n,
      (∏ i, a (p i)) ≠ (∏ i, a (q i)) →
…