MeanLimit.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.GammaEnvironment.meanPassageSequence_isSubadditive line 13
Source documentation
Mean passage times along a lattice ray form a subadditive sequence.
```
theorem GammaEnvironment.meanPassageSequence_isSubadditive
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) : Subadditive (meanPassageSequence P τ z) := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.meanPassageSequence
theorem OAI.GammaFPP.GammaEnvironment.normalized_meanPassage_bddBelow line 21
Source documentation
Nonnegative passage times bound the normalized mean sequence below, including the totalized quotient at n = 0.
```
theorem GammaEnvironment.normalized_meanPassage_bddBelow
    (h : GammaEnvironment shape rate P τ) (z : Vertex) :
    BddBelow (Set.range (fun n : ℕ => meanPassageSequence P τ z n / (n : ℝ))) := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.meanPassageSequence
def OAI.GammaFPP.directionalMeanConstant line 30
Source documentation
The directional mean constant is the Fekete limit of mean passage times along a lattice ray, with the infimum taken over positive indices.
```
noncomputable def directionalMeanConstant
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) : ℝ :=
…
```
Mentions: OAI.GammaFPP.GammaEnvironment

theorem OAI.GammaFPP.GammaEnvironment.meanPassageSequence_tendsto line 36

Source documentation

Convergence in the native filter ℕ.atTop, including the zero direction.

theorem GammaEnvironment.meanPassageSequence_tendsto
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) :
    Tendsto (fun n : ℕ => meanPassageSequence P τ z n / (n : ℝ))
      atTop (𝓝 (directionalMeanConstant h hs hr z)) :=
…

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

theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_nonneg line 44
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_le_normalized_mean line 53
Source documentation
Every positive-index finite mean bounds the limit above. The restriction n≠0 is native to Fekete's infimum and is not discarded at total division zero.
```
theorem GammaEnvironment.directionalMeanConstant_le_normalized_mean
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) {n : ℕ} (hn : n ≠ 0) :
    directionalMeanConstant h hs hr z ≤ meanPassageSequence P τ z n / (n : ℝ) :=
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant, OAI.GammaFPP.meanPassageSequence
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_le_mean line 60
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_le_path_length line 71
Source documentation
Deterministic path bound; every repeated traversal is charged. This is finite but does not assert strict positivity in any nonzero direction.
```
theorem GammaEnvironment.directionalMeanConstant_le_path_length
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) (ds : List Step) (hend : (0 : Vertex) + displacement ds = z) :
    directionalMeanConstant h hs hr z ≤ (ds.length : ℝ) * (shape / rate) :=
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_zero line 80
Source documentation
The zero direction is handled by the actual empty path, not a positivity assumption or an exception to the convergence statement.
```
theorem GammaEnvironment.directionalMeanConstant_zero
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    directionalMeanConstant h hs hr (0 : Vertex) = 0 := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant

theorem OAI.GammaFPP.GammaEnvironment.meanPassageSequence_zero_direction_tendsto line 88

Source documentation

The same native convergence theorem specializes to literal zero at z=0.

theorem GammaEnvironment.meanPassageSequence_zero_direction_tendsto
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate) :
    Tendsto (fun n : ℕ => meanPassageSequence P τ (0 : Vertex) n / (n : ℝ))
      atTop (𝓝 0) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.meanPassageSequence