FieldGaussianRecursionOrder.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The radial payoff comparison propagates through each actual nonzero Gaussian backward operator. The zero-exponent case is handled separately.

lemma OAI.InvariantIsing.fieldFolded_exp_difference_mul line 14
lemma OAI.InvariantIsing.fieldFolded_mass_ratio_monotone line 23
lemma OAI.InvariantIsing.field_gaussian_exp_ratio_folded line 44

theorem OAI.InvariantIsing.gaussianOperator_difference_monotone_pos line 62

Source documentation

Increasing an even payoff by a radially increasing difference has a radially increasing effect on the nonzero-exponent backward value.

theorem gaussianOperator_difference_monotone_pos (v : ℝ≥0) (hv : v ≠ 0)
    {ζ : ℝ} (hζ : 0 < ζ) (F G : ℝ → ℝ)
    (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)) :
    MonotoneOn (fun z => gaussianOperator ζ v G z - gaussianOperator ζ v F z) (Ici 0) := by
…

Mentions: OAI.InvariantIsing.gaussianOperator

theorem OAI.InvariantIsing.gaussianOperator_difference_monotone line 93

Source documentation

Full one-step radial difference preservation, including zero Gaussian variance and the ordinary root exponent.

theorem gaussianOperator_difference_monotone (v : ℝ≥0) {ζ : ℝ} (hζ : 0 ≤ ζ)
    (F G : ℝ → ℝ) (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)) :
    MonotoneOn (fun z => gaussianOperator ζ v G z - gaussianOperator ζ v F z) (Ici 0) := by
…

Mentions: OAI.InvariantIsing.gaussianOperator