FieldSpinFolding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact odd-observable law for an even Gaussian tilt. This is the conditional-spin kernel in the radial field comparison.

lemma OAI.InvariantIsing.field_abs_tanh_le_one line 14
lemma OAI.InvariantIsing.field_gaussian_odd_folded_integral line 19

theorem OAI.InvariantIsing.field_gaussian_tilt_odd_integral_eq_folded line 44

Source documentation

The physical odd conditional spin observable equals the folded observable multiplied by the exact conditional sign.

theorem field_gaussian_tilt_odd_integral_eq_folded (v : ℝ≥0) (hv : v ≠ 0) (z ζ : ℝ)
    (F a : ℝ → ℝ) (hF : Function.Even F) (ha : Function.Odd a)
    (hi : Integrable (fun u => Real.exp (ζ * F u) * a u) (gaussianReal z v))
    (hweight : Integrable (fun u => Real.exp (ζ * F u)) (gaussianReal z v)) :
    (∫ u, a u ∂(gaussianReal z v).tilted (fun u => ζ * F u)) =
      (∫ u in Ici (0 : ℝ), (a u * Real.tanh ((z / v) * u)) * fieldFoldedWeight v ζ F z u) /
        (∫ u in Ici (0 : ℝ), fieldFoldedWeight v ζ F z u) := by
…

Mentions: OAI.InvariantIsing.fieldFoldedWeight