FrameSubspaceRecurrence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Diagonal recurrence from transport of an actual subspace

The measurable frame theorem needs only transport of its column space. The change-of-basis matrix and its nonzero determinant are derived here from that transport and independence; they are not additional dynamical hypotheses.

theorem OAI.DukePrimeDegree.ae_frame_diagonal_invariant_of_span_transport line 19

theorem OAI.DukePrimeDegree.ae_frame_diagonal_invariant_on_event line 55

Source documentation

A fixed-rank frame may be extended by zero outside its invariant rank event. The projective recurrence then applies to the whole probability space; restriction to an invariant subspace of the measure is unnecessary.

theorem ae_frame_diagonal_invariant_on_event
    {Y : Type*} [MeasurableSpace Y] {n k : ℕ}
    (μ : Measure Y) [IsFiniteMeasure μ]
    (T : Y → Y) (hT : MeasurePreserving T μ μ)
    (E : Set Y) (hE : ∀ᵐ x ∂μ, T x ∈ E ↔ x ∈ E)
    (B : Y → Matrix (Fin n) (Fin k) ℝ)
    (hB : ∀ i j, Measurable (fun x => B x i j))
    (hfull : ∀ᵐ x ∂μ, x ∈ E → LinearIndependent ℝ (B x).col)
    (hzero : ∀ᵐ x ∂μ, x ∉ E → B x = 0)
    (a : Fin n → ℝ) (ha : ∀ i, 0 < a i)
    (htransport : ∀ᵐ x ∂μ, x ∈ E →
      Submodule.span ℝ (Set.range (B (T x)).col) =
…