Stationarity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.IidEnvironment.translate line 14
Source documentation
Deterministic lattice translation preserves an iid environment.
```
theorem IidEnvironment.translate (h : IidEnvironment ν P τ) (a : Vertex) :
    IidEnvironment ν P (fun e => τ (shiftEdge a e)) where
…
```
Mentions: OAI.GammaFPP.IidEnvironment
theorem OAI.GammaFPP.IidEnvironment.jointLaw line 22
Source documentation
The complete configuration has the product law.
```
theorem IidEnvironment.jointLaw (h : IidEnvironment ν P τ) :
    Measure.map (fun ω e => τ e ω) P = iidProductLaw ν := by
…
```
Mentions: OAI.GammaFPP.IidEnvironment, OAI.GammaFPP.iidProductLaw

theorem OAI.GammaFPP.IidEnvironment.translated_event_probability line 28

Source documentation

Every measurable configuration observable has translation-invariant law.

theorem IidEnvironment.translated_event_probability
    (h : IidEnvironment ν P τ) (a : Vertex)
    (A : Set (Edge → ℝ)) (hA : MeasurableSet A) :
    P {ω | (fun e => τ (shiftEdge a e) ω) ∈ A} =
      P {ω | (fun e => τ e ω) ∈ A} := by
…

Mentions: OAI.GammaFPP.IidEnvironment

theorem OAI.GammaFPP.IidEnvironment.integral_configuration line 40

Source documentation

Integral transport to the common product law.

theorem IidEnvironment.integral_configuration (h : IidEnvironment ν P τ)
    (f : (Edge → ℝ) → ℝ) (hf : Measurable f) :
    (∫ ω, f (fun e => τ e ω) ∂P) = ∫ w, f w ∂iidProductLaw ν := by
…

Mentions: OAI.GammaFPP.IidEnvironment, OAI.GammaFPP.iidProductLaw

theorem OAI.GammaFPP.IidEnvironment.integral_passageTime_translate line 48

Source documentation

Translated passage times have equal expectations.

theorem IidEnvironment.integral_passageTime_translate
    (h : IidEnvironment ν P τ) (a p q : Vertex) :
    (∫ ω, passageTime (fun e => τ e ω) (a + p) (a + q) ∂P) =
      ∫ ω, passageTime (fun e => τ e ω) p q ∂P := by
…

Mentions: OAI.GammaFPP.IidEnvironment

theorem OAI.GammaFPP.GammaEnvironment.integral_passageTime_nonneg line 66

Source documentation

The expected passage time is nonnegative.

theorem GammaEnvironment.integral_passageTime_nonneg
    (h : GammaEnvironment shape rate P τ) (p q : Vertex) :
    0 ≤ ∫ ω, passageTime (fun e => τ e ω) p q ∂P := by
…

Mentions: OAI.GammaFPP.GammaEnvironment

theorem OAI.GammaFPP.GammaEnvironment.integral_passageTime_le_path_length line 74

Source documentation

A deterministic path bounds the expected passage time, counting every traversal.

theorem GammaEnvironment.integral_passageTime_le_path_length
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (p q : Vertex) (ds : List Step) (hend : p + displacement ds = q) :
    (∫ ω, passageTime (fun e => τ e ω) p q ∂P) ≤
      (ds.length : ℝ) * (shape / rate) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment

theorem OAI.GammaFPP.GammaEnvironment.finite_expected_passage line 87

Source documentation

There is a finite upper bound for the expected passage time.

theorem GammaEnvironment.finite_expected_passage
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (p q : Vertex) :
    Integrable (fun ω => passageTime (fun e => τ e ω) p q) P ∧
      ∃ L : ℕ, 0 ≤ (∫ ω, passageTime (fun e => τ e ω) p q ∂P) ∧
        (∫ ω, passageTime (fun e => τ e ω) p q ∂P) ≤ (L : ℝ) * (shape / rate) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment

theorem OAI.GammaFPP.GammaEnvironment.mean_passageTime_subadditive line 99

Source documentation

Stationarity and the passage-time triangle inequality give subadditivity in expectation.

theorem GammaEnvironment.mean_passageTime_subadditive
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (x y : Vertex) :
    (∫ ω, passageTime (fun e => τ e ω) 0 (x + y) ∂P) ≤
      (∫ ω, passageTime (fun e => τ e ω) 0 x ∂P) +
      (∫ ω, passageTime (fun e => τ e ω) 0 y ∂P) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment

def OAI.GammaFPP.meanPassageSequence line 119
Source documentation
Mean passage time along an integer lattice direction, indexed by natural steps.
```
noncomputable def meanPassageSequence (P : Measure Ω) (τ : Edge → Ω → ℝ)
    (z : Vertex) (n : ℕ) : ℝ :=
…
```
theorem OAI.GammaFPP.GammaEnvironment.meanPassageSequence_nonneg line 123

theorem OAI.GammaFPP.GammaEnvironment.meanPassageSequence_subadditive line 129

Source documentation

Subadditivity includes the zero direction and zero indices.

theorem GammaEnvironment.meanPassageSequence_subadditive
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) (m n : ℕ) :
    meanPassageSequence P τ z (m + n) ≤
      meanPassageSequence P τ z m + meanPassageSequence P τ z n := by
…

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