Quartic Core Bounds

This module contains the quartic-core Gaussian bounds used by the active local-gap bridge. The content formerly lived in a scratch file; it is now part of the RequestProject library proper.

theorem quartic_core_integral_dim_bound (β t : ℝ) (hβ : 0 ≤ β) (ht : 0 < t) (n : ℕ) (hsmall : β * (↑(dim n) / t) ≤ 1 / 2) : ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n t, Real.exp (β * t * quarticCorr n (matrixOfEdge n mu)) * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu) ≤ Real.exp (β ^ 2 / 2 * ↑n * (↑(dim n) / t) ^ 2) * gaussianF (dim n) t

Quartic-core integral bound specialized to the natural radius dim n / t.