SpectralArrayDiagonalLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compact array/center subsequences and constant limiting diagonals.

lemma OAI.InvariantIsing.spectralArray_center_subsequence line 15

theorem OAI.InvariantIsing.spectralArray_constant_diagonal_of_weak_limit line 27

Source documentation

Vanishing actual L1 self-overlap fluctuations and converging compact centers give deterministic diagonals in the weak limiting array.

theorem spectralArray_constant_diagonal_of_weak_limit {m : ℕ}
    (L : ℕ → ProbabilityMeasure (SpectralArray m)) (Q : ProbabilityMeasure (SpectralArray m))
    (hL : Tendsto L atTop (nhds Q)) (center : ℕ → Fin m → ℝ) (q : Fin m → ℝ)
    (hc : Tendsto center atTop (nhds q))
    (hdiag : ∀ i a, Tendsto
      (fun k => ∫ x, |(x (i, i) a : ℝ) - center k a| ∂(L k : Measure (SpectralArray m)))
      atTop (nhds 0)) :
    ∀ᵐ x ∂(Q : Measure (SpectralArray m)), ∀ i a, (x (i, i) a : ℝ) = q a := by
…

Mentions: OAI.InvariantIsing.SpectralArray