OAI/Probability/InvariantIsing/Pressure/RandomCoefficientIBP.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.measurable_randomCoefficient_mean line 23
2. lemma OAI.InvariantIsing.integrable_randomCoefficient_mean line 34
3. lemma OAI.InvariantIsing.measurable_randomCoefficient_insertion line 45
4. lemma OAI.InvariantIsing.integrable_randomCoefficient_insertion line 60
5. theorem OAI.InvariantIsing.joint_randomCoefficient_cylinder_insertion line 83

   Source documentation

   The countable Gaussian insertion identity with external-disorder-dependent coefficients and replica tests. The uniform second-moment estimate justifies Fubini for the countable cylinder law.

   theorem joint_randomCoefficient_cylinder_insertion (hν : Measurable ν)
       (A B : Ω → X → ℕ →₀ ℝ)
       (hA : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
       (hB : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (B p.1.1 p.2) p.1.2))
       (hcross : Measurable (fun p : Ω × (X × X) => cylinderCross (B p.1 p.2.1) (A p.1 p.2.2)))
       {K L : ℝ} (ha : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ K)
       (hb : ∀ ω x, (B ω x).sum (fun _ c => c ^ 2) ≤ L)
       {r : ℕ} (D : Ω → (Fin (r + 1) → X) → ℝ)
       (hDm : Measurable (Function.uncurry D)) {c : ℝ} (hc : 0 ≤ c)
       (hD : ∀ ω σ, |D ω σ| ≤ c) :
       (∫ z : Ω × (ℕ → ℝ), referenceReplicaMean (ν z.1)
         (fun x => cylinderField (A z.1 x) z.2)
   …

6. lemma OAI.InvariantIsing.randomCoefficient_all_exp_ae line 170

   Source documentation

   All exponential tilts are integrable for almost every joint disorder. Only integer tilts are intersected before extending to every real parameter.

   lemma randomCoefficient_all_exp_ae (hν : Measurable ν)
       (A : Ω → X → ℕ →₀ ℝ)
       (hA : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
       {K : ℝ} (ha : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ K) :
       ∀ᵐ z : Ω × (ℕ → ℝ) ∂P.prod gaussianCoordinates, ∀ t : ℝ,
         Integrable (fun x => Real.exp (t * cylinderField (A z.1 x) z.2)) (ν z.1) := by
   …

7. lemma OAI.InvariantIsing.measurable_randomCoefficient_cgf line 202
8. lemma OAI.InvariantIsing.integrable_randomCoefficient_cgf line 214

   Source documentation

   The external-disorder-dependent log partition is integrable, by the uniform pointwise Gaussian second-moment estimate.

   lemma integrable_randomCoefficient_cgf (hν : Measurable ν)
       (A : Ω → X → ℕ →₀ ℝ)
       (hA : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
       {K : ℝ} (ha : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ K) (t : ℝ) :
       Integrable (fun z : Ω × (ℕ → ℝ) =>
         cgf (fun x => cylinderField (A z.1 x) z.2) (ν z.1) t) (P.prod gaussianCoordinates) := by
   …