OAI/Probability/GammaPassage/ScalingLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.map_mul_withDensity_real line 12

   Source documentation

   Scalar change of variables for a measurable nonnegative density.

   lemma map_mul_withDensity_real {a : ℝ} (ha : 0 < a)
       {f : ℝ → ℝ≥0∞} (hf : Measurable f) :
       Measure.map (fun x : ℝ => a * x) (volume.withDensity f) =
         volume.withDensity (fun y => ENNReal.ofReal a⁻¹ * f (y / a)) := by
   …

2. lemma OAI.GammaFPP.gammaPDF_scaling line 39

   Source documentation

   The Gamma density satisfies the scaling Jacobian identity, including at the origin.

   lemma gammaPDF_scaling {shape rate a : ℝ} (hshape : 0 < shape) (hrate : 0 < rate)
       (ha : 0 < a) (y : ℝ) :
       ENNReal.ofReal a⁻¹ * gammaPDF shape rate (y / a) =
         gammaPDF shape (rate / a) y := by
   …

3. theorem OAI.GammaFPP.map_mul_gammaMeasure line 57

   Source documentation

   Scaling a Gamma random variable by a positive constant divides its rate.

   theorem map_mul_gammaMeasure {shape rate a : ℝ} (hshape : 0 < shape)
       (hrate : 0 < rate) (ha : 0 < a) :
       Measure.map (fun x : ℝ => a * x) (gammaMeasure shape rate) =
         gammaMeasure shape (rate / a) := by
   …

4. theorem OAI.GammaFPP.map_mul_gammaMeasure_eq_tilt line 69

   Source documentation

   The scaling pushforward equals the measure weighted by the Gamma likelihood.

   theorem map_mul_gammaMeasure_eq_tilt {shape rate a : ℝ} (hshape : 0 < shape)
       (hrate : 0 < rate) (ha : 0 < a) :
       Measure.map (fun x : ℝ => a * x) (gammaMeasure shape rate) =
         (gammaMeasure shape rate).withDensity
           (fun x => ENNReal.ofReal (gammaScaleLikelihood shape rate a x)) := by
   …

   Mentions: OAI.GammaFPP.gammaScaleLikelihood