OAI/Probability/GammaPassage/EnvironmentScaling.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.GammaEnvironment.scale line 16

   Source documentation

   Scaling every edge weight by a > 0 divides the Gamma rate by a and preserves independence.

   theorem GammaEnvironment.scale
       (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate) (ha : 0 < a) :
       GammaEnvironment shape (rate / a) P (fun e ω => a * τ e ω) where
   …

   Mentions: OAI.GammaFPP.GammaEnvironment

2. theorem OAI.GammaFPP.GammaEnvironment.ae_positive_edges line 31
3. theorem OAI.GammaFPP.GammaEnvironment.scale_with_timeConstant line 42

   Source documentation

   Scaling the environment transports the almost-sure limit for each fixed real direction.

   theorem GammaEnvironment.scale_with_timeConstant
       (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate) (ha : 0 < a)
       {μ : PlanarFPP.Plane → ℝ} (hμ : PlanarFPP.IsTimeConstant P τ μ) :
       GammaEnvironment shape (rate / a) P (fun e ω => a * τ e ω) ∧
         PlanarFPP.IsTimeConstant P (fun e ω => a * τ e ω) (fun v => a * μ v) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Plane, OAI.PlanarFPP.IsTimeConstant