OAI/Probability/InvariantIsing/Cavity/CavityHaarRank.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Almost-sure positive definiteness of finite Haar spectral compressions.

  1. theorem OAI.InvariantIsing.cavityHaarWindowGram_posDef line 16

    Source documentation

    A Haar-rotated orthonormal q-frame has positive-definite compression to every fixed coordinate window containing at least q rows.

    theorem cavityHaarWindowGram_posDef {N q : ℕ} (l u : ℕ)
    (hlq : l + q ≤ u) (huN : u ≤ N)
    (μ : Measure (Orthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulRightInvariant]
    (A₀ : Matrix (Fin N) (Fin q) ℝ) (hA₀ : A₀.transpose * A₀ = 1) :
    ∀ᵐ (U : Orthogonal N) ∂μ, (cavityWindowGram ((U : Matrix (Fin N) (Fin N) ℝ) * A₀) l u).PosDef := by
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.cavityWindowGram