OAI/Probability/InvariantIsing/Spectral/SpectralArrayGG.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantIsing.SpectralEntry line 14
2. abbrev OAI.InvariantIsing.SpectralArray line 15
3. abbrev OAI.InvariantIsing.SpectralBlock line 16
4. def OAI.InvariantIsing.spectralEntryMonomial line 18
5. lemma OAI.InvariantIsing.continuous_spectralEntryMonomial line 21
6. def OAI.InvariantIsing.spectralBlockView line 25
7. def OAI.InvariantIsing.spectralBlockLink line 28
8. lemma OAI.InvariantIsing.continuous_spectralBlockView line 31
9. lemma OAI.InvariantIsing.continuous_spectralBlockLink line 35
10. def OAI.InvariantIsing.spectralBlockPairCoordinate line 38
11. lemma OAI.InvariantIsing.continuous_spectralBlockPairCoordinate line 45
12. lemma OAI.InvariantIsing.spectralBlockPairCoordinate_ext line 50
13. theorem OAI.InvariantIsing.spectralBlock_pair_monomials_unique line 61

    Source documentation

    Polynomial moments in the new link, with arbitrary continuous tests of the old block, determine its full joint law.

    theorem spectralBlock_pair_monomials_unique (m n : ℕ)
        (P Q : Measure (SpectralBlock m n × SpectralEntry m)) [IsFiniteMeasure P] [IsFiniteMeasure Q]
        (h : ∀ D : SpectralBlock m n → ℝ, Continuous D → ∀ d : Fin m → ℕ,
          (∫ x, D x.1 * spectralEntryMonomial d x.2 ∂P) =
            ∫ x, D x.1 * spectralEntryMonomial d x.2 ∂Q) : P = Q := by
    …

    Mentions: OAI.InvariantIsing.SpectralBlock, OAI.InvariantIsing.SpectralEntry, OAI.InvariantIsing.spectralEntryMonomial

14. theorem OAI.InvariantIsing.spectral_monomial_measure_identity line 124
15. theorem OAI.InvariantIsing.spectral_monomialGG_measurable line 168
16. def OAI.InvariantIsing.spectralMonomialResidual line 199
17. lemma OAI.InvariantIsing.spectralMonomialResidual_zero line 206
18. lemma OAI.InvariantIsing.spectralMonomialResidual_weak_limit line 217
19. theorem OAI.InvariantIsing.spectralGG_of_weak_monomial_residuals line 237

    Source documentation

    Vanishing monomial residuals imply the Ghirlanda–Guerra identities for the weak limit of the spectral overlap arrays.

    theorem spectralGG_of_weak_monomial_residuals {m : ℕ} {L : ℕ → ProbabilityMeasure (SpectralArray m)}
        {μ : ProbabilityMeasure (SpectralArray m)} (hL : Tendsto L atTop (𝓝 μ))
        (hg : ∀ n, 2 ≤ n → ∀ i : Fin n, ∀ D : SpectralBlock m n → ℝ, Continuous D → ∀ d : Fin m → ℕ,
          Tendsto (fun N => spectralMonomialResidual (L N) n i D d) atTop (𝓝 0)) :
        HasEntryGhirlandaGuerra (fun x i j => x (i, j)) (μ : Measure (SpectralArray m)) := by
    …

    Mentions: OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.SpectralBlock, OAI.InvariantIsing.spectralMonomialResidual

20. theorem OAI.InvariantIsing.spectralGG_of_weak_nonconstant_monomial_residuals line 249