OAI/Probability/InvariantIsing/Cavity/CavitySiteSymmetry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact site-symmetry identity used for cavity self-consistency. It is a statement about the full two-replica law, before any cutoff.

  1. def OAI.InvariantIsing.cavitySpinPairPermutation line 14
  2. def OAI.InvariantIsing.cavityTotalSpinOverlap line 23
  3. lemma OAI.InvariantIsing.cavityTotalSpinOverlap_permutation line 26
  4. theorem OAI.InvariantIsing.cavity_site_symmetry_identity line 35

    Source documentation

    Permutation symmetry makes every site insertion equal to the total-overlap insertion. No Ghirlanda--Guerra identity is required for the full system.

    theorem cavity_site_symmetry_identity {N : ℕ} (hN : 0 < N)
    (μ : Measure (Spin N × Spin N)) [IsFiniteMeasure μ]
    (hμ : ∀ e : Equiv.Perm (Fin N), Measure.map (cavitySpinPairPermutation e) μ = μ)
    (φ : ℝ → ℝ) (j : Fin N) :
    (∫ x, φ (cavityTotalSpinOverlap x) * spinValue (x.1 j) * spinValue (x.2 j) ∂μ) =
      ∫ x, φ (cavityTotalSpinOverlap x) * cavityTotalSpinOverlap x ∂μ := by
…

    Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.cavitySpinPairPermutation, OAI.InvariantIsing.cavityTotalSpinOverlap, OAI.InvariantIsing.spinValue