FieldGaussianOrder.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The folded likelihood comparison for the actual Gaussian tilted transition, with its integrability discharged by linear growth.

lemma OAI.InvariantIsing.field_test_exp_integrable line 16

theorem OAI.InvariantIsing.field_gaussian_tilt_abs_parent_order line 28

Source documentation

Absolute child position is stochastically increasing in a nonnegative parent position under an arbitrary even linearly growing payoff.

theorem field_gaussian_tilt_abs_parent_order (v : ℝ≥0) (hv : v ≠ 0) (ζ : ℝ)
    (F f : ℝ → ℝ) (hF : Measurable F) (hFeven : Function.Even F)
    (hgrowth : HasLinearGrowth F) (hf : Measurable f)
    (hmono : MonotoneOn f (Ici 0)) {C : ℝ} (hbound : ∀ u, |f u| ≤ C)
    {z₀ z₁ : ℝ} (hz₀ : 0 ≤ z₀) (hzz : z₀ ≤ z₁) :
    (∫ u, f |u| ∂(gaussianReal z₀ v).tilted (fun u => ζ * F u)) ≤
      (∫ u, f |u| ∂(gaussianReal z₁ v).tilted (fun u => ζ * F u)) := by
…

theorem OAI.InvariantIsing.field_gaussian_tilt_abs_payoff_order line 51

Source documentation

Adding an even payoff which increases in absolute position raises the actual absolute-position transition.

theorem field_gaussian_tilt_abs_payoff_order (v : ℝ≥0) (hv : v ≠ 0) {ζ : ℝ} (hζ : 0 ≤ ζ)
    (F G f : ℝ → ℝ) (hF : Measurable F) (hG : Measurable G)
    (hFeven : Function.Even F) (hGeven : Function.Even G)
    (hFgrowth : HasLinearGrowth F) (hGgrowth : HasLinearGrowth G)
    (hFG : MonotoneOn (fun u => G u - F u) (Ici 0))
    (hf : Measurable f) (hmono : MonotoneOn f (Ici 0))
    {C : ℝ} (hbound : ∀ u, |f u| ≤ C) (z : ℝ) :
    (∫ u, f |u| ∂(gaussianReal z v).tilted (fun u => ζ * F u)) ≤
      (∫ u, f |u| ∂(gaussianReal z v).tilted (fun u => ζ * G u)) := by
…