MeanSwap.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.SwapGeometry.swapStep line 10
lemma OAI.GammaFPP.SwapGeometry.swapStep_swap line 16
lemma OAI.GammaFPP.SwapGeometry.swapStep_delta line 17
def OAI.GammaFPP.SwapGeometry.swapEdge line 19
lemma OAI.GammaFPP.SwapGeometry.swapEdge_swap line 20
lemma OAI.GammaFPP.SwapGeometry.swapEdge_injective line 21
lemma OAI.GammaFPP.SwapGeometry.swapStep_edge line 23
lemma OAI.GammaFPP.SwapGeometry.displacement_swap line 26
lemma OAI.GammaFPP.SwapGeometry.pathCost_swap line 31
lemma OAI.GammaFPP.SwapGeometry.passageTime_swap line 37
def OAI.GammaFPP.swapEdgeEquiv line 59
Source documentation
The actual undirected edge swap is a bijection, not just a sign reversal.
```
def swapEdgeEquiv : Edge ≃ Edge where
…
```
theorem OAI.GammaFPP.IidEnvironment.coordinateSwap line 65
theorem OAI.GammaFPP.IidEnvironment.coordinateSwap_jointLaw line 73
Source documentation
Equality of full configuration measures, not merely finite marginals.
```
theorem IidEnvironment.coordinateSwap_jointLaw (h : IidEnvironment ν P τ) :
    Measure.map (fun ω e => τ (SwapGeometry.swapEdge e) ω) P =
      Measure.map (fun ω e => τ e ω) P :=
…
```
Mentions: OAI.GammaFPP.IidEnvironment, OAI.GammaFPP.SwapGeometry.swapEdge
theorem OAI.GammaFPP.IidEnvironment.integral_passageTime_coordinateSwap line 80
Source documentation
Coordinate swap preserves the integral of each passage time; the integral identity also holds for the totalized integral without an integrability assumption.
```
theorem IidEnvironment.integral_passageTime_coordinateSwap
    (h : IidEnvironment ν P τ) (p q : Vertex) :
    (∫ ω, passageTime (fun e => τ e ω) p.swap q.swap ∂P) =
      ∫ ω, passageTime (fun e => τ e ω) p q ∂P := by
…
```
Mentions: OAI.GammaFPP.IidEnvironment
theorem OAI.GammaFPP.GammaEnvironment.meanPassageSequence_coordinateSwap line 100
Source documentation
The equality holds for every index including zero, and swaps the two coordinates rather than applying central symmetry.
```
theorem GammaEnvironment.meanPassageSequence_coordinateSwap
    (h : GammaEnvironment shape rate P τ) (z : Vertex) (n : ℕ) :
    meanPassageSequence P τ z.swap n = meanPassageSequence P τ z n := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.meanPassageSequence
theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_coordinateSwap line 110
Source documentation
Actual deterministic mean-limit invariance, with no norm or time-constant existence premise. It also includes the zero direction.
```
theorem GammaEnvironment.directionalMeanConstant_coordinateSwap
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) :
    directionalMeanConstant h hs hr z.swap = directionalMeanConstant h hs hr z := by
…
```
Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant