OAI/Probability/InvariantIsing/Cavity/CavityGaussianIntegral.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Scalar square completion for the quadratic cavity tilt. The variance may vanish; only positivity of the resulting precision is required.

  1. lemma OAI.InvariantIsing.cavity_complete_square line 14
  2. lemma OAI.InvariantIsing.cavity_integrable_exp_quadratic line 20
  3. lemma OAI.InvariantIsing.cavity_integral_exp_quadratic line 28
  4. lemma OAI.InvariantIsing.cavity_gaussian_weighted_integrand line 35
  5. lemma OAI.InvariantIsing.cavity_gaussian_normalizer line 48
  6. lemma OAI.InvariantIsing.cavity_gaussian_constant line 63
  7. theorem OAI.InvariantIsing.cavity_gaussian_quadratic_integrable line 72

    Source documentation

    Exponential integrability includes the degenerate Gaussian.

    theorem cavity_gaussian_quadratic_integrable (v : ℝ≥0) (a u : ℝ)
    (hq : 0 < 1 - v * a) :
    Integrable (fun z : ℝ => Real.exp (a / 2 * (u + z) ^ 2)) (gaussianReal 0 v) := by
…
  8. theorem OAI.InvariantIsing.cavity_gaussian_quadratic_integral line 89

    Source documentation

    The one-dimensional form of cav:q-gaussian-integral, including singular covariance v = 0.

    theorem cavity_gaussian_quadratic_integral (v : ℝ≥0) (a u : ℝ)
    (hq : 0 < 1 - v * a) :
    (∫ z : ℝ, Real.exp (a / 2 * (u + z) ^ 2) ∂gaussianReal 0 v) =
      (Real.sqrt (1 - v * a))⁻¹ * Real.exp (a * u ^ 2 / (2 * (1 - v * a))) := by
…
  9. theorem OAI.InvariantIsing.cavity_gaussian_quadratic_logIntegral line 105