OAI/Probability/InvariantIsing/Fields/FieldGaussianTransformLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact one-step Gaussian operator laws used to propagate the radial comparison through the finite Ising field recursion.

  1. lemma OAI.InvariantIsing.field_even_abs line 15
  2. lemma OAI.InvariantIsing.field_gaussian_integral_shift line 20
  3. lemma OAI.InvariantIsing.gaussianOperator_eq_gaussian_integral line 29
  4. lemma OAI.InvariantIsing.gaussianOperator_eq_gaussian_exp_integral line 38
  5. lemma OAI.InvariantIsing.field_gaussian_integral_reflect line 48
  6. lemma OAI.InvariantIsing.gaussianOperator_even line 57
  7. lemma OAI.InvariantIsing.field_gaussian_linear_integrable line 71
  8. lemma OAI.InvariantIsing.field_linearGrowth_sub line 84
  9. lemma OAI.InvariantIsing.field_folded_test_integrable line 97

    Source documentation

    Gaussian integrability of an even-test tilt supplies integrability of its folded numerator, also for unbounded linearly growing tests.

    lemma field_folded_test_integrable (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)) :
    Integrable (fun u => f u * fieldFoldedWeight v ζ F z u) (volume.restrict (Ici 0)) := by
…

    Mentions: OAI.InvariantIsing.fieldFoldedWeight