OAI/Probability/InvariantIsing/Fields/FieldFoldedDensity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact Gaussian folding and conditional sign factors. These identities supply the folded transition and spin-mean kernel used in fld:radial.

  1. lemma OAI.InvariantIsing.field_gaussian_pair_sum line 15
  2. lemma OAI.InvariantIsing.field_gaussian_pair_sign line 31
  3. lemma OAI.InvariantIsing.field_even_tilt_conditional_sign line 61

    Source documentation

    An even terminal tilt cancels from the conditional sign law.

    lemma field_even_tilt_conditional_sign (v : ℝ≥0) (hv : v ≠ 0)
    (ζ : ℝ) (F : ℝ → ℝ) (hF : Function.Even F) (z u : ℝ) :
    Real.exp (ζ * F u) * gaussianPDFReal z v u -
      Real.exp (ζ * F (-u)) * gaussianPDFReal z v (-u) =
      Real.tanh ((z / v) * u) *
        (Real.exp (ζ * F u) * gaussianPDFReal z v u +
          Real.exp (ζ * F (-u)) * gaussianPDFReal z v (-u)) := by
…