TensorArrayGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Geometry of weak limits of the actual perturbed tensor array laws.

lemma OAI.InvariantIsing.tensorPerturbedArrayLaw_gram line 15
lemma OAI.InvariantIsing.tensorPerturbedArrayLaw_reindex line 24

theorem OAI.InvariantIsing.tensorPerturbedArrayLaw_limit_geometry line 35

Source documentation

The geometry is derived from the actual finite Gibbs samples, independently of the subsequent concentration/minimization argument that enforces GG.

theorem tensorPerturbedArrayLaw_limit_geometry (N : ℕ → ℕ) (m n : ℕ)
    (μ : (k : ℕ) → Measure (SpecialOrthogonal (N k))) [∀ k, IsProbabilityMeasure (μ k)]
    (eig c : (k : ℕ) → Fin (N k) → ℝ)
    (I : (k : ℕ) → Fin m → Finset (Fin (N k)))
    (u : (k : ℕ) → Fin (N k) → ℝ) (v : ℕ → Fin m → ℝ) (t : ℕ → ℝ)
    (b : ℕ → ℝ) (h : ℕ → ℕ → ℝ) (Q : ProbabilityMeasure (SpectralArray (m + 1)))
    (hL : Tendsto (fun k => tensorPerturbedArrayLaw (μ k) (eig k) (c k) (I k)
      (u k) (v k) (t k) n b (h k)) atTop (𝓝 Q)) :
    (∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), SpectralGram x) ∧
      ∀ e : ℕ → ℕ, Function.Injective e →
        (Q : Measure (SpectralArray (m + 1))).map (permuteSpectralArray e) = Q := by
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.tensorPerturbedArrayLaw, OAI.InvariantIsing.SpectralGram, OAI.InvariantIsing.permuteSpectralArray