FieldSpinKernelOrder.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of the physical conditional-spin transition. This keeps the spin observable, rather than the derivative in rescaled coordinates.

lemma OAI.InvariantIsing.field_spin_test_measurable line 14
lemma OAI.InvariantIsing.field_spin_test_bound line 19
lemma OAI.InvariantIsing.field_spin_test_monotone line 25
lemma OAI.InvariantIsing.field_spin_exp_integrable line 33
lemma OAI.InvariantIsing.field_gaussian_tilt_odd_eq_abs line 42

theorem OAI.InvariantIsing.field_gaussian_spin_transition_order line 63

Source documentation

Parent, payoff and physical spin-observable comparisons in one actual Gaussian transition. This is the backward induction step in fld:radial.

theorem field_gaussian_spin_transition_order (v : ℝ≥0) (hv : v ≠ 0) {ζ : ℝ} (hζ : 0 ≤ ζ)
    (F G a b : ℝ → ℝ) (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))
    (ha : Measurable a) (hb : Measurable b) (haodd : Function.Odd a) (hbodd : Function.Odd b)
    (hamono : MonotoneOn a (Ici 0)) (hapos : ∀ u ∈ Ici (0 : ℝ), 0 ≤ a u)
    (hab : ∀ u ∈ Ici (0 : ℝ), a u ≤ b u)
    {B : ℝ} (haB : ∀ u, |a u| ≤ B) (hbB : ∀ u, |b u| ≤ B)
    {z₀ z₁ : ℝ} (hz₀ : 0 ≤ z₀) (hzz : z₀ ≤ z₁) :
    (∫ u, a u ∂(gaussianReal z₀ v).tilted (fun u => ζ * F u)) ≤
      ∫ u, b u ∂(gaussianReal z₁ v).tilted (fun u => ζ * G u) := by
…