FirstMoment.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.gamma_ae_pos line 17
Source documentation
The Gamma law is concentrated on strictly positive real weights.
```
theorem gamma_ae_pos (shape rate : ℝ) :
    ∀ᵐ x : ℝ ∂gammaMeasure shape rate, 0 < x := by
…
```

lemma OAI.GammaFPP.gamma_first_weighted_density line 27

Source documentation

Multiplication by x shifts the Gamma shape by one. Both sides vanish at the origin.

lemma gamma_first_weighted_density {shape rate : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (x : ℝ) :
    gammaPDF shape rate x * ENNReal.ofReal x =
      ENNReal.ofReal (shape / rate) * gammaPDF (shape + 1) rate x := by
…

theorem OAI.GammaFPP.gamma_lintegral_id line 60

Source documentation

The nonnegative first moment from the normalized density with shifted shape.

theorem gamma_lintegral_id {shape rate : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) :
    (∫⁻ x : ℝ, ENNReal.ofReal x ∂gammaMeasure shape rate) =
      ENNReal.ofReal (shape / rate) := by
…

theorem OAI.GammaFPP.gamma_integrable_id line 73

Source documentation

The Gamma law has an integrable identity function for positive shape and rate.

theorem gamma_integrable_id {shape rate : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) :
    Integrable (fun x : ℝ => x) (gammaMeasure shape rate) := by
…

theorem OAI.GammaFPP.gamma_integral_id line 82

Source documentation

The mean of the Gamma law with shape and rate parameters.

theorem gamma_integral_id {shape rate : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) :
    (∫ x : ℝ, x ∂gammaMeasure shape rate) = shape / rate := by
…