MeanPositive.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.lower_le_limit_integral_of_ae_eventually line 15

Source documentation

Fatou needs only eventual lower bounds, not samplewise convergence.

lemma lower_le_limit_integral_of_ae_eventually [IsProbabilityMeasure P]
    (X : ℕ → Ω → ℝ) (a m : ℝ)
    (hX : ∀ n, Measurable (X n)) (hI : ∀ n, Integrable (X n) P)
    (hpos : ∀ n, ∀ᵐ ω ∂P, 0 ≤ X n ω)
    (hlower : ∀ᵐ ω ∂P, ∀ᶠ n in atTop, a ≤ X n ω)
    (hlimit : Tendsto (fun n => ∫ ω, X n ω ∂P) atTop (𝓝 m)) (hm : 0 ≤ m) :
    a ≤ m := by
…

lemma OAI.GammaFPP.latticeDistance_zero_nsmul line 39
Source documentation
Literal lattice L1 distance scales under natural multiplication.
```
lemma latticeDistance_zero_nsmul (z : Vertex) (n : ℕ) :
    latticeDistance 0 (n • z) = n * latticeDistance 0 z := by
…
```
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_linear_lower line 47
Source documentation
The actual Fekete mean limit has the same positive linear lower bound as the eventual path metric. The zero direction is treated before division.
```
theorem GammaEnvironment.directionalMeanConstant_linear_lower
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) :
    cheapSlope shape rate * (latticeDistance 0 z : ℝ) ≤ directionalMeanConstant h hs hr z := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.cheapSlope, OAI.GammaFPP.directionalMeanConstant