OAI/Probability/InvariantIsing/Arrays/ReplicaCovariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantIsing.random_replica_energy_covariance_bound line 16

   Source documentation

   Integrate the replica covariance estimate while allowing both the inserted observable and the replica test to depend on the disorder.

   theorem random_replica_energy_covariance_bound {Ω X : Type*}
       [MeasurableSpace Ω] [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X]
       {μ : Measure Ω} [IsProbabilityMeasure μ] {ν : Ω → Measure X}
       [∀ ω, IsProbabilityMeasure (ν ω)] {H Y : Ω × X → ℝ} {r : ℕ}
       (D : Ω × (Fin (r + 1) → X) → ℝ) (hD : Measurable D)
       {c : ℝ} (hc : 0 ≤ c) (hDb : ∀ ω σ, |D (ω, σ)| ≤ c) (b : ℝ)
       (he : ∀ᵐ ω ∂μ, Integrable (fun x => Real.exp (H (ω, x))) (ν ω))
       (hY : ∀ᵐ ω ∂μ, Integrable (fun x => Y (ω, x))
         ((ν ω).tilted (fun x => H (ω, x))))
       (hU : Integrable (fun ω => referenceReplicaMean (ν ω) (fun x => H (ω, x))
         (fun σ => Y (ω, σ 0) * D (ω, σ))) μ)
       (hV : Integrable (fun ω => referenceReplicaMean (ν ω) (fun x => H (ω, x))
   …