OAI/Probability/InvariantIsing/Fields/FieldGaussianFolding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.field_integral_fold line 14
2. lemma OAI.InvariantIsing.field_gaussian_density_integrable line 28
3. theorem OAI.InvariantIsing.field_gaussian_folded_integral line 38

   Source documentation

   Folding a Gaussian with an even terminal tilt gives precisely the positive-half-line density used in the likelihood-ratio comparison.

   theorem field_gaussian_folded_integral (v : ℝ≥0) (hv : v ≠ 0) (z ζ : ℝ)
       (F f : ℝ → ℝ) (hF : Function.Even F)
       (hf : Integrable (fun u => Real.exp (ζ * F u) * f |u|) (gaussianReal z v)) :
       (∫ u, Real.exp (ζ * F u) * f |u| ∂gaussianReal z v) =
         (2 * (Real.sqrt (2 * Real.pi * v))⁻¹ * Real.exp (-z ^ 2 / (2 * v))) *
           ∫ u in Ici (0 : ℝ), f u * fieldFoldedWeight v ζ F z u := by
   …

   Mentions: OAI.InvariantIsing.fieldFoldedWeight

4. lemma OAI.InvariantIsing.field_folded_constant_pos line 61
5. lemma OAI.InvariantIsing.fieldFoldedWeight_integrable line 68

   Source documentation

   Gaussian exponential integrability supplies the folded density's integrability; no separate density-tail assumption is needed.

   lemma fieldFoldedWeight_integrable (v : ℝ≥0) (hv : v ≠ 0) (z ζ : ℝ)
       (F : ℝ → ℝ) (hF : Function.Even F)
       (hweight : Integrable (fun u => Real.exp (ζ * F u)) (gaussianReal z v)) :
       Integrable (fieldFoldedWeight v ζ F z) (volume.restrict (Ici 0)) := by
   …

   Mentions: OAI.InvariantIsing.fieldFoldedWeight

6. lemma OAI.InvariantIsing.fieldFoldedWeight_mass_pos line 90
7. lemma OAI.InvariantIsing.field_gaussian_folded_ratio line 103