OAI/Probability/InvariantIsing/Gaussian/GaussianGGBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.randomReplicaAverage_const_mul line 21
2. lemma OAI.InvariantIsing.randomReplicaAverage_add_bounded line 29
3. theorem OAI.InvariantIsing.randomReplicaEnergy_full_identity line 50

   Source documentation

   Gaussian integration by parts without imposing a constant diagonal.

   theorem randomReplicaEnergy_full_identity (hν : Measurable ν)
       (A : X → ℕ →₀ ℝ) {B : ℝ} (hA : ∀ x, (A x).sum (fun _ c => c ^ 2) ≤ B)
       (t : ℝ) {r : ℕ} (D : (Fin (r + 1) → X) → ℝ)
       {c : ℝ} (hc : 0 ≤ c) (hD : ∀ σ, |D σ| ≤ c) :
       randomReplicaEnergy P ν A t D = t *
         (randomReplicaAverage P ν A t (fun σ => D σ *
           (∑ i : Fin (r + 1), cylinderCross (A (σ 0)) (A (σ i)))) -
         (r + 1 : ℕ) * randomReplicaAverage P ν A t
           (fun τ : Fin (r + 1 + 1) → X => D (Fin.tail τ) *
             cylinderCross (A ((Fin.tail τ) 0)) (A (τ 0)))) := by
   …

4. theorem OAI.InvariantIsing.countable_gaussian_gg_bound_variable_diagonal line 88

   Source documentation

   The finite GG error splits into an energy fluctuation and an explicit covariance of the self-overlap. Spectral self-overlaps are not constant before adding their separate deterministic perturbations.

   theorem countable_gaussian_gg_bound_variable_diagonal (hν : Measurable ν)
       (A : X → ℕ →₀ ℝ) {B : ℝ} (hA : ∀ x, (A x).sum (fun _ c => c ^ 2) ≤ B)
       (t b : ℝ) {r : ℕ} (D : (Fin (r + 1) → X) → ℝ)
       {c : ℝ} (hc : 0 ≤ c) (hD : ∀ σ, |D σ| ≤ c)
       (hE : Integrable (fun z : Ω × (ℕ → ℝ) => ∫ x,
         |cylinderField (A x) z.2 - b|
           ∂(ν z.1).tilted (fun x => t * cylinderField (A x) z.2))
         (P.prod gaussianCoordinates)) :
       |t| * |(r + 1 : ℕ) * randomReplicaAverage P ν A t
           (fun τ : Fin (r + 1 + 1) → X => D (Fin.tail τ) *
             cylinderCross (A ((Fin.tail τ) 0)) (A (τ 0))) -
         randomReplicaAverage P ν A t D * randomReplicaAverage P ν A t
   …