OAI/Probability/InvariantIsing/Arrays/DiagonalCovariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.randomCoefficient_bounded_observable_covariance line 19
2. theorem OAI.InvariantIsing.randomCoefficient_diagonal_covariance_le line 84

   Source documentation

   No constant self-overlap is imposed at finite N. Its actual Gibbs L1 fluctuation controls precisely the extra covariance in the GG estimate.

   theorem randomCoefficient_diagonal_covariance_le (hν : Measurable ν)
       (A : Ω → X → ℕ →₀ ℝ)
       (hAm : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
       (hcross : Measurable (fun p : Ω × (X × X) => cylinderCross (A p.1 p.2.1) (A p.1 p.2.2)))
       {B : ℝ} (hA : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ B)
       (t d : ℝ) {r : ℕ} (D : Ω → (Fin (r + 1) → X) → ℝ)
       (hDm : Measurable (Function.uncurry D)) {c : ℝ} (hc : 0 ≤ c)
       (hD : ∀ ω σ, |D ω σ| ≤ c) :
       |randomCoefficientAverage P ν A t
           (fun ω σ => D ω σ * cylinderCross (A ω (σ 0)) (A ω (σ 0))) -
         randomCoefficientAverage P ν A t D * randomCoefficientAverage P ν A t
           (fun ω (σ : Fin 1 → X) => cylinderCross (A ω (σ 0)) (A ω (σ 0)))| ≤
   …

   Mentions: OAI.InvariantIsing.randomCoefficientAverage

3. theorem OAI.InvariantIsing.randomCoefficient_gaussian_gg_L1_bound line 137

   Source documentation

   Quantitative GG with both errors expressed as actual Gibbs L1 deviations. The energy fluctuation is divided by the perturbation scale when passing to the limiting GG identities; the diagonal fluctuation is not.

   theorem randomCoefficient_gaussian_gg_L1_bound (hν : Measurable ν)
       (A : Ω → X → ℕ →₀ ℝ)
       (hAm : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
       (hcross : Measurable (fun p : Ω × (X × X) => cylinderCross (A p.1 p.2.1) (A p.1 p.2.2)))
       {B : ℝ} (hA : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ B)
       (t b d : ℝ) {r : ℕ} (D : Ω → (Fin (r + 1) → X) → ℝ)
       (hDm : Measurable (Function.uncurry D)) {c : ℝ} (hc : 0 ≤ c)
       (hD : ∀ ω σ, |D ω σ| ≤ c)
       (hE : Integrable (fun z : Ω × (ℕ → ℝ) => ∫ x,
         |cylinderField (A z.1 x) z.2 - b|
           ∂(ν z.1).tilted (fun x => t * cylinderField (A z.1 x) z.2))
         (P.prod gaussianCoordinates)) :
   …