RandomCoefficientGG.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

GG estimates for Haar-dependent Gaussian perturbation tensors.

def OAI.InvariantIsing.randomCoefficientAverage line 20

Source documentation

Expectation over external disorder and independent Gaussian coordinates.

def randomCoefficientAverage (P : Measure Ω) (ν : Ω → Measure X)
    (A : Ω → X → ℕ →₀ ℝ) (t : ℝ) {r : ℕ} (D : Ω → (Fin r → X) → ℝ) : ℝ :=
…

def OAI.InvariantIsing.randomCoefficientEnergy line 25
lemma OAI.InvariantIsing.randomCoefficientAverage_abs_le line 35
lemma OAI.InvariantIsing.randomCoefficientAverage_one line 48
lemma OAI.InvariantIsing.randomCoefficientAverage_add_bounded line 61

theorem OAI.InvariantIsing.randomCoefficientEnergy_full_identity line 91

Source documentation

Conditional Gaussian integration by parts, with the diagonal retained.

theorem randomCoefficientEnergy_full_identity (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 : ℝ) {r : ℕ} (D : Ω → (Fin (r + 1) → X) → ℝ)
    (hDm : Measurable (Function.uncurry D)) {c : ℝ} (hc : 0 ≤ c)
    (hD : ∀ ω σ, |D ω σ| ≤ c) :
    randomCoefficientEnergy P ν A t D = t *
      (randomCoefficientAverage P ν A t (fun ω σ => D ω σ *
        (∑ i : Fin (r + 1), cylinderCross (A ω (σ 0)) (A ω (σ i)))) -
      (r + 1 : ℕ) * randomCoefficientAverage P ν A t
…

Mentions: OAI.InvariantIsing.randomCoefficientEnergy, OAI.InvariantIsing.randomCoefficientAverage

theorem OAI.InvariantIsing.randomCoefficient_energy_covariance_bound line 133

Source documentation

Energy fluctuation bounds remain valid for Haar-dependent tensors and Haar-dependent replica tests.

theorem randomCoefficient_energy_covariance_bound (hν : Measurable ν)
    (A : Ω → X → ℕ →₀ ℝ)
    (hAm : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
    {B : ℝ} (hA : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ B)
    (t b : ℝ) {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)) :
    |randomCoefficientEnergy P ν A t D - b * randomCoefficientAverage P ν A t D| ≤
…

Mentions: OAI.InvariantIsing.randomCoefficientEnergy, OAI.InvariantIsing.randomCoefficientAverage

theorem OAI.InvariantIsing.randomCoefficient_gaussian_gg_bound line 175

Source documentation

The finite GG comparison for the actual type of perturbations used here: both coefficients and tests may depend on the external Haar disorder, and the spectral self-overlap covariance remains an explicit error.

theorem randomCoefficient_gaussian_gg_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 : ℝ) {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)) :
…

lemma OAI.InvariantIsing.randomCoefficient_cgf_mean_bounds line 272

Source documentation

Gaussian mean logpartition bounds remain valid when the coefficient vectors depend on the external rotation disorder.

lemma randomCoefficient_cgf_mean_bounds (hν : Measurable ν)
    (A : Ω → X → ℕ →₀ ℝ)
    (hAm : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
    {B : ℝ} (hA : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ B) (t : ℝ) :
    0 ≤ (∫ z : Ω × (ℕ → ℝ), cgf (fun x => cylinderField (A z.1 x) z.2) (ν z.1) t
      ∂P.prod gaussianCoordinates) ∧
    (∫ z : Ω × (ℕ → ℝ), cgf (fun x => cylinderField (A z.1 x) z.2) (ν z.1) t
      ∂P.prod gaussianCoordinates) ≤ t ^ 2 * B / 2 := by
…

theorem OAI.InvariantIsing.randomCoefficient_energy_at_minimum line 290

Source documentation

The local-minimum fluctuation estimate applies to the actual Haar-dependent Gaussian fields, rather than requiring fixed coefficients.

theorem randomCoefficient_energy_at_minimum (hν : Measurable ν)
    (A : Ω → X → ℕ →₀ ℝ)
    (hAm : Measurable (fun p : (Ω × (ℕ → ℝ)) × X => cylinderField (A p.1.1 p.2) p.1.2))
    {B : ℝ} (hA : ∀ ω x, (A ω x).sum (fun _ c => c ^ 2) ≤ B)
    {v c a s δ K : ℝ} (hs : 0 < s) (hK : 0 < K)
    (hmin : ∀ t ∈ Set.Icc (v - s) (v + s),
      -(∫ z : Ω × (ℕ → ℝ), cgf (fun x => cylinderField (A z.1 x) z.2) (ν z.1) v
        ∂P.prod gaussianCoordinates) + c * (v - a) ^ 2 ≤
      -(∫ z : Ω × (ℕ → ℝ), cgf (fun x => cylinderField (A z.1 x) z.2) (ν z.1) t
        ∂P.prod gaussianCoordinates) + c * (t - a) ^ 2)
    (hconc : ∀ t ∈ ({v - s, v, v + s} : Set ℝ),
      (∫ z : Ω × (ℕ → ℝ), |cgf (fun x => cylinderField (A z.1 x) z.2) (ν z.1) t -
…