Integral identities and domination lemmas for signed resolvent moments.

Reference: O. Kallenberg, Foundations of Modern Probability, 2nd ed., Springer, 2002.

theorem BGW.Probability.integral_sq_eq_two_mul_tail {ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ν] [MeasureTheory.NullSingletonClass ν] {f : ℝ → ℝ} (hf : MeasureTheory.Integrable f ν) : (∫ (s : ℝ), f s ∂ν) ^ 2 = 2 * ∫ (s : ℝ), f s * ∫ (t : ℝ) in Set.Ioi s, f t ∂ν ∂ν

The square of an integral is twice its integral over strictly ordered pairs.

theorem BGW.Probability.measurable_integral_tail {Ω : Type u_1} [MeasurableSpace Ω] {f : ℝ × Ω → ℝ} (hf : Measurable f) : Measurable fun (p : ℝ × Ω) => ∫ (t : ℝ) in Set.Ioi p.1, f (t, p.2)

A jointly measurable integrand has a jointly measurable tail integral.

theorem BGW.Probability.integrable_exp_mul_bounded_prod {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {F : ℝ × Ω → ℝ} (hF : Measurable F) {C a b : ℝ} (ha : a < 0) (hC : ∀ (p : ℝ × Ω), |F p| ≤ C) : MeasureTheory.Integrable (fun (p : ℝ × Ω) => Real.exp (a * p.1) * F p) ((MeasureTheory.volume.restrict (Set.Ioi b)).prod μ)

An exponentially weighted bounded jointly measurable function is integrable.