FiniteSumIntegrability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.finiteGammaMeasure_ae_nonneg line 12

lemma OAI.GammaFPP.finite_probability_lintegral_prod line 23

Source documentation

Nonnegative integrals factor over a finite product of probability measures.

private lemma finite_probability_lintegral_prod (μ : ι → Measure ℝ)
    [∀ i, IsProbabilityMeasure (μ i)] (f : ι → ℝ → ℝ≥0∞)
    (hf : ∀ i, Measurable (f i)) :
    (∫⁻ v, ∏ i, f i (v i) ∂Measure.pi μ) = ∏ i, ∫⁻ u, f i u ∂μ i := by
…

theorem OAI.GammaFPP.finite_gamma_lintegral_exp_sum line 38

Source documentation

Exact nonnegative exponential moment for the sum of all finite coordinates.

theorem finite_gamma_lintegral_exp_sum {shape rate t : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (ht : t < rate) :
    (∫⁻ v : ι → ℝ, ENNReal.ofReal (Real.exp (t * ∑ i, v i))
      ∂finiteGammaMeasure shape rate) =
      (ENNReal.ofReal ((rate / (rate-t)) ^ shape)) ^ Fintype.card ι := by
…

Mentions: OAI.GammaFPP.finiteGammaMeasure

theorem OAI.GammaFPP.finite_gamma_integrable_exp_sum line 56

Source documentation

The exponential moment of the coordinate sum is finite for every t < rate.

theorem finite_gamma_integrable_exp_sum {shape rate t : ℝ}
    (hs : 0 < shape) (hr : 0 < rate) (ht : t < rate) :
    Integrable (fun v : ι → ℝ => Real.exp (t * ∑ i, v i))
      (finiteGammaMeasure shape rate) := by
…

Mentions: OAI.GammaFPP.finiteGammaMeasure