OAI/Probability/InvariantIsing/Fields/FieldFoldedKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.field_tanh_monotone line 15
2. lemma OAI.InvariantIsing.field_tanh_nonneg line 22
3. lemma OAI.InvariantIsing.field_scaled_tanh_mono line 25
4. lemma OAI.InvariantIsing.hasDerivAt_field_logcosh_mul line 30
5. lemma OAI.InvariantIsing.field_logcosh_scaled_difference_monotone line 40

   Source documentation

   Increasing the scale makes the log-cosh payoff difference even and nondecreasing on the positive half-line.

   lemma field_logcosh_scaled_difference_monotone {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :
       MonotoneOn (fun u => Real.log (Real.cosh (b * u)) - Real.log (Real.cosh (a * u))) (Ici 0) := by
   …

6. lemma OAI.InvariantIsing.field_logcosh_scaled_difference_even line 58
7. lemma OAI.InvariantIsing.field_cosh_ratio_monotone line 63
8. def OAI.InvariantIsing.fieldFoldedWeight line 70
9. lemma OAI.InvariantIsing.fieldFoldedWeight_pos line 73
10. lemma OAI.InvariantIsing.fieldFoldedWeight_parent_order line 78

    Source documentation

    The exact likelihood-ratio order in the absolute parent position.

    lemma fieldFoldedWeight_parent_order {v : ℝ} (hv : 0 < v) (ζ : ℝ) (F : ℝ → ℝ)
        {z₀ z₁ : ℝ} (hz₀ : 0 ≤ z₀) (hzz : z₀ ≤ z₁)
        {u₀ u₁ : ℝ} (hu₀ : 0 ≤ u₀) (huu : u₀ ≤ u₁) :
        fieldFoldedWeight v ζ F z₁ u₀ * fieldFoldedWeight v ζ F z₀ u₁ ≤
          fieldFoldedWeight v ζ F z₁ u₁ * fieldFoldedWeight v ζ F z₀ u₀ := by
    …

    Mentions: OAI.InvariantIsing.fieldFoldedWeight

11. lemma OAI.InvariantIsing.fieldFoldedWeight_payoff_order line 95

    Source documentation

    Increasing the even payoff by an increasing function raises the folded transition in likelihood-ratio order.

    lemma fieldFoldedWeight_payoff_order (v : ℝ) {ζ : ℝ} (hζ : 0 ≤ ζ)
        (F G : ℝ → ℝ) (hFG : MonotoneOn (fun u => G u - F u) (Ici 0))
        (z : ℝ) {u₀ u₁ : ℝ} (hu₀ : 0 ≤ u₀) (huu : u₀ ≤ u₁) :
        fieldFoldedWeight v ζ G z u₀ * fieldFoldedWeight v ζ F z u₁ ≤
          fieldFoldedWeight v ζ G z u₁ * fieldFoldedWeight v ζ F z u₀ := by
    …

    Mentions: OAI.InvariantIsing.fieldFoldedWeight

12. theorem OAI.InvariantIsing.fieldFolded_parent_expectation_le line 113

    Source documentation

    The parent comparison acts on every bounded increasing test under the actual folded density, after its Gaussian integrability is supplied.

    theorem fieldFolded_parent_expectation_le {v : ℝ} (hv : 0 < v)
        (ζ : ℝ) (F f : ℝ → ℝ) (hf : Measurable f)
        (hmono : MonotoneOn f (Ici 0)) {C : ℝ} (hbound : ∀ u, |f u| ≤ C)
        {z₀ z₁ : ℝ} (hz₀ : 0 ≤ z₀) (hzz : z₀ ≤ z₁)
        (h₀ : Integrable (fieldFoldedWeight v ζ F z₀) (volume.restrict (Ici 0)))
        (h₁ : Integrable (fieldFoldedWeight v ζ F z₁) (volume.restrict (Ici 0)))
        (hm₀ : 0 < ∫ u in Ici 0, fieldFoldedWeight v ζ F z₀ u)
        (hm₁ : 0 < ∫ u in Ici 0, fieldFoldedWeight v ζ F z₁ u) :
        (∫ u in Ici 0, f u * fieldFoldedWeight v ζ F z₀ u) /
            (∫ u in Ici 0, fieldFoldedWeight v ζ F z₀ u) ≤
          (∫ u in Ici 0, f u * fieldFoldedWeight v ζ F z₁ u) /
            (∫ u in Ici 0, fieldFoldedWeight v ζ F z₁ u) := by
    …

    Mentions: OAI.InvariantIsing.fieldFoldedWeight

13. theorem OAI.InvariantIsing.fieldFolded_payoff_expectation_le line 134

    Source documentation

    The payoff comparison acts on the same bounded increasing tests.

    theorem fieldFolded_payoff_expectation_le (v : ℝ) {ζ : ℝ} (hζ : 0 ≤ ζ)
        (F G f : ℝ → ℝ) (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 : ℝ)
        (h₀ : Integrable (fieldFoldedWeight v ζ F z) (volume.restrict (Ici 0)))
        (h₁ : Integrable (fieldFoldedWeight v ζ G z) (volume.restrict (Ici 0)))
        (hm₀ : 0 < ∫ u in Ici 0, fieldFoldedWeight v ζ F z u)
        (hm₁ : 0 < ∫ u in Ici 0, fieldFoldedWeight v ζ G z u) :
        (∫ u in Ici 0, f u * fieldFoldedWeight v ζ F z u) /
            (∫ u in Ici 0, fieldFoldedWeight v ζ F z u) ≤
          (∫ u in Ici 0, f u * fieldFoldedWeight v ζ G z u) /
            (∫ u in Ici 0, fieldFoldedWeight v ζ G z u) := by
    …

    Mentions: OAI.InvariantIsing.fieldFoldedWeight