PathIntegrability.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.GammaEnvironment.ae_positive line 16
Source documentation
All edge weights are almost surely positive, by positivity of the marginal and countability.
```
theorem GammaEnvironment.ae_positive (h : GammaEnvironment shape rate P τ) :
    ∀ᵐ ω ∂P, ∀ e, 0 < τ e ω := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment

theorem OAI.GammaFPP.GammaEnvironment.integrable_edge line 26

Source documentation

Each Gamma edge weight is integrable.

theorem GammaEnvironment.integrable_edge (h : GammaEnvironment shape rate P τ)
    (hs : 0 < shape) (hr : 0 < rate) (e : PlanarFPP.Edge) :
    Integrable (τ e) P := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge

theorem OAI.GammaFPP.GammaEnvironment.integral_edge line 35

Source documentation

The mean edge weight is shape / rate.

theorem GammaEnvironment.integral_edge (h : GammaEnvironment shape rate P τ)
    (hs : 0 < shape) (hr : 0 < rate) (e : PlanarFPP.Edge) :
    (∫ ω, τ e ω ∂P) = shape / rate := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge

theorem OAI.GammaFPP.GammaEnvironment.integrable_pathCost line 44
Source documentation
The cost of a fixed finite step list is integrable, including repeated edges.
```
theorem GammaEnvironment.integrable_pathCost (h : GammaEnvironment shape rate P τ)
    (hs : 0 < shape) (hr : 0 < rate)
    (p : PlanarFPP.Vertex) (ds : List PlanarFPP.Step) :
    Integrable (fun ω => PlanarFPP.pathCost (fun e => τ e ω) p ds) P := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Vertex, OAI.PlanarFPP.Step, OAI.PlanarFPP.pathCost

theorem OAI.GammaFPP.GammaEnvironment.integral_pathCost line 57

Source documentation

Expected path cost counts edge traversals. The empty path has expectation zero.

theorem GammaEnvironment.integral_pathCost (h : GammaEnvironment shape rate P τ)
    (hs : 0 < shape) (hr : 0 < rate)
    (p : PlanarFPP.Vertex) (ds : List PlanarFPP.Step) :
    (∫ ω, PlanarFPP.pathCost (fun e => τ e ω) p ds ∂P) =
      (ds.length : ℝ) * (shape / rate) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Vertex, OAI.PlanarFPP.Step, OAI.PlanarFPP.pathCost

theorem OAI.GammaFPP.GammaEnvironment.integrable_passageTime line 74
Source documentation
Passage time is integrable by domination by the cost of one deterministic path.
```
theorem GammaEnvironment.integrable_passageTime (h : GammaEnvironment shape rate P τ)
    (hs : 0 < shape) (hr : 0 < rate) (p q : PlanarFPP.Vertex) :
    Integrable (fun ω => PlanarFPP.passageTime (fun e => τ e ω) p q) P := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Vertex, OAI.PlanarFPP.passageTime