TiltDensity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.gammaScaleLikelihood line 16
Source documentation
Likelihood for changing a Gamma rate from rate to rate / alpha.
```
noncomputable def gammaScaleLikelihood (shape rate alpha x : ℝ) : ℝ :=
…
```
lemma OAI.GammaFPP.gammaScaleLikelihood_pos line 19

lemma OAI.GammaFPP.gamma_scale_likelihood_density line 24

Source documentation

The likelihood identity includes the real-power convention at x = 0.

lemma gamma_scale_likelihood_density {shape rate alpha : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (halpha : 0 < alpha) (x : ℝ) :
    gammaPDF shape rate x * ENNReal.ofReal (gammaScaleLikelihood shape rate alpha x) =
      gammaPDF shape (rate / alpha) x := by
…

Mentions: OAI.GammaFPP.gammaScaleLikelihood

theorem OAI.GammaFPP.gammaMeasure_withDensity_scaleLikelihood line 51

Source documentation

Weighting the Gamma measure by the scaling likelihood changes its rate.

theorem gammaMeasure_withDensity_scaleLikelihood {shape rate alpha : ℝ}
    (hshape : 0 < shape) (hrate : 0 < rate) (halpha : 0 < alpha) :
    (gammaMeasure shape rate).withDensity
        (fun x => ENNReal.ofReal (gammaScaleLikelihood shape rate alpha x)) =
      gammaMeasure shape (rate / alpha) := by
…

Mentions: OAI.GammaFPP.gammaScaleLikelihood

def OAI.GammaFPP.gammaShrinkLikelihood line 65
Source documentation
The likelihood with the parametrization alpha = 1 - delta.
```
noncomputable def gammaShrinkLikelihood (shape rate delta x : ℝ) : ℝ :=
…
```
theorem OAI.GammaFPP.gammaMeasure_withDensity_shrinkLikelihood line 68