MeanAlgebra.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.GammaEnvironment.integral_passageTime_neg line 13

Source documentation

Undirected reversal followed by translation, on the actual passage times.

theorem GammaEnvironment.integral_passageTime_neg
    (h : GammaEnvironment shape rate P τ) (z : Vertex) :
    (∫ ω, passageTime (fun e => τ e ω) 0 (-z) ∂P) =
      ∫ ω, passageTime (fun e => τ e ω) 0 z ∂P := by
…

Mentions: OAI.GammaFPP.GammaEnvironment

theorem OAI.GammaFPP.GammaEnvironment.meanPassageSequence_neg line 26
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_neg line 32

theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_add_le line 41

Source documentation

Limit order applied to finite, integrable mean subadditivity.

theorem GammaEnvironment.directionalMeanConstant_add_le
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (x y : Vertex) :
    directionalMeanConstant h hs hr (x + y) ≤
      directionalMeanConstant h hs hr x + directionalMeanConstant h hs hr y := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant

theorem OAI.GammaFPP.tendsto_nat_right_multiple line 56
Source documentation
Cofinality of positive natural multiples, proved without a real-index limit.
```
private theorem tendsto_nat_right_multiple (k : ℕ) (hk : 0 < k) :
    Tendsto (fun n : ℕ => n * k) atTop atTop := by
…
```
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_nsmul line 67
Source documentation
Natural homogeneity follows from the cofinal subsequence n*k, not an assumed homogeneous extension. The zero multiplier is a separate case.
```
theorem GammaEnvironment.directionalMeanConstant_nsmul
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) (k : ℕ) :
    directionalMeanConstant h hs hr (k • z) =
      (k : ℝ) * directionalMeanConstant h hs hr z := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_zsmul line 97
Source documentation
Integer homogeneity, with |k| represented by its exact natural absolute value. This includes k=0, negative multipliers, and the zero direction.
```
theorem GammaEnvironment.directionalMeanConstant_zsmul
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) (k : ℤ) :
    directionalMeanConstant h hs hr (k • z) =
      (k.natAbs : ℝ) * directionalMeanConstant h hs hr z := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant