FieldLikelihoodRatio.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The ordered likelihood-ratio comparison used by the folded Gaussian transitions of the one-site Ising field recursion.

theorem OAI.InvariantIsing.field_likelihood_ratio_expectation_le line 15

Source documentation

Ordered likelihood ratios increase every integrable increasing test. The reference measure is supported on nonnegative absolute positions.

theorem field_likelihood_ratio_expectation_le
    (μ : Measure ℝ) [SFinite μ] (w₀ w₁ f : ℝ → ℝ)
    (hμ : ∀ᵐ x ∂μ, 0 ≤ x)
    (hf : MonotoneOn f (Ici 0))
    (hcross : ∀ x ∈ Ici (0 : ℝ), ∀ y ∈ Ici (0 : ℝ), x ≤ y →
      w₁ x * w₀ y ≤ w₁ y * w₀ x)
    (hw₀ : Integrable w₀ μ) (hw₁ : Integrable w₁ μ)
    (hfw₀ : Integrable (fun x => f x * w₀ x) μ)
    (hfw₁ : Integrable (fun x => f x * w₁ x) μ)
    (hm₀ : 0 < ∫ x, w₀ x ∂μ) (hm₁ : 0 < ∫ x, w₁ x ∂μ) :
    (∫ x, f x * w₀ x ∂μ) / (∫ x, w₀ x ∂μ) ≤
      (∫ x, f x * w₁ x ∂μ) / (∫ x, w₁ x ∂μ) := by
…