CavityGaussianTestLaw.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A bounded Gibbs replica test depends on a centered Gaussian field only through its covariance, including for the countable leaf prior.

theorem OAI.InvariantIsing.cavity_twoReplica_same_covariance line 14

theorem OAI.InvariantIsing.cavity_twoReplica_gaussian_transport line 44

Source documentation

Pull back both the energy and the test by a prior-preserving configuration map. This retains the common Gaussian disorder.

theorem cavity_twoReplica_gaussian_transport {X : Type*} [MeasurableSpace X]
    (ν : Measure X) [IsProbabilityMeasure ν] (e : X → X)
    (he : MeasurePreserving e ν ν) (H : X → ℝ) (hH : Measurable H)
    (C : X → ℕ →₀ ℝ) (hC : ∀ g, Measurable (fun x => cylinderField (C x) g))
    (F : (Fin 2 → X) → ℝ) (hF : Measurable F) :
    (∫ g, referenceReplicaMean ν
      (fun x => H (e x) + cylinderField (C (e x)) g)
      (fun σ => F (fun i => e (σ i))) ∂gaussianCoordinates) =
    ∫ g, referenceReplicaMean ν (fun x => H x + cylinderField (C x) g) F
      ∂gaussianCoordinates := by
…

theorem OAI.InvariantIsing.cavity_twoReplica_ensemble_symmetry line 60

Source documentation

A symmetry of the deterministic energy and Gaussian covariance, combined with invariance of the disorder and the prior, gives the full annealed replica-test symmetry.

theorem cavity_twoReplica_ensemble_symmetry {Ω X : Type*}
    [MeasurableSpace Ω] [MeasurableSpace X] [Countable X]
    [MeasurableSingletonClass X]
    (μ : Measure Ω) (R : Ω → Ω) (hR : MeasurePreserving R μ μ)
    (ν : Measure X) [IsProbabilityMeasure ν]
    (e : X → X) (he : MeasurePreserving e ν ν)
    (H : Ω → X → ℝ) (C : Ω → X → ℕ →₀ ℝ)
    (M V : Ω → ℝ) (hH : ∀ ω x, |H ω x| ≤ M ω)
    (hV : ∀ ω x, (C ω x).sum (fun _ z => z ^ 2) ≤ V ω)
    (henergy : ∀ ω x, H (R ω) (e x) = H ω x)
    (hcov : ∀ ω x y, cylinderCross (C (R ω) (e x)) (C (R ω) (e y)) =
      cylinderCross (C ω x) (C ω y))
…