OAI/Probability/GammaPassage/Scaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.passageTime_scale line 12

   Source documentation

   Positive scaling commutes with the infimum over finite paths with nonnegative weights.

   theorem passageTime_scale (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
       (c : ℝ) (hc : 0 < c) (p q : Vertex) :
       passageTime (fun e => c * w e) p q = c * passageTime w p q := by
   …

2. theorem OAI.GammaFPP.timeConstantNorm_scale line 29

   Source documentation

   Positive scaling preserves the time-constant norm laws.

   theorem timeConstantNorm_scale {μ : Plane → ℝ} (hμ : TimeConstantNorm μ)
       (c : ℝ) (hc : 0 < c) : TimeConstantNorm (fun v => c * μ v) where
   …

3. theorem OAI.GammaFPP.isTimeConstant_scale line 40

   Source documentation

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

   theorem isTimeConstant_scale {Ω : Type*} [MeasurableSpace Ω]
       {P : Measure Ω} {τ : Edge → Ω → ℝ} {μ : Plane → ℝ}
       (hτ : ∀ᵐ ω ∂P, ∀ e, 0 ≤ τ e ω) (hμ : IsTimeConstant P τ μ)
       (c : ℝ) (hc : 0 < c) :
       IsTimeConstant P (fun e ω => c * τ e ω) (fun v => c * μ v) := by
   …

4. theorem OAI.GammaFPP.differentiableAwayFromOrigin_scale line 57

   Source documentation

   Scaling a differentiable time constant scales its continuous linear derivative.

   theorem differentiableAwayFromOrigin_scale {μ : Plane → ℝ}
       (hμ : DifferentiableAwayFromOrigin μ) (c : ℝ) :
       DifferentiableAwayFromOrigin (fun v => c * μ v) := by
   …