Environment.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.GammaFPP.IidEnvironment line 10
Source documentation
An independent, identically distributed edge environment with marginal law ν.
Also declared: ComparatorChallenges/GammaPassage.lean:71 (same declaration text).
```
structure IidEnvironment {Ω : Type*} [MeasurableSpace Ω]
    (ν : Measure ℝ) (P : Measure Ω) (τ : PlanarFPP.Edge → Ω → ℝ) : Prop where
…
```
Mentions: OAI.PlanarFPP.Edge
abbrev OAI.GammaFPP.GammaEnvironment line 18
Source documentation
An iid edge environment with Gamma marginal law.
Also declared: ComparatorChallenges/GammaPassage.lean:79 (same declaration text).
```
abbrev GammaEnvironment {Ω : Type*} [MeasurableSpace Ω]
    (shape rate : ℝ) (P : Measure Ω) (τ : PlanarFPP.Edge → Ω → ℝ) :=
…
```
Mentions: OAI.PlanarFPP.Edge
def OAI.GammaFPP.iidProductLaw line 23
Source documentation
The product law of the edge weights.
```
noncomputable def iidProductLaw (ν : Measure ℝ) : Measure (PlanarFPP.Edge → ℝ) :=
…
```
Mentions: OAI.PlanarFPP.Edge
def OAI.GammaFPP.HasTimeConstantFor line 27
Source documentation
The passage-time limit predicate on the product probability space with marginal ν.
```
def HasTimeConstantFor (ν : Measure ℝ) (μ : PlanarFPP.Plane → ℝ) : Prop :=
…
```
Mentions: OAI.PlanarFPP.Plane
theorem OAI.GammaFPP.iidProductLaw_environment line 31
Source documentation
The coordinate evaluations form an iid environment under the product law.
```
theorem iidProductLaw_environment (ν : Measure ℝ) [IsProbabilityMeasure ν] :
    IidEnvironment ν (iidProductLaw ν) (fun e ω => ω e) where
…
```
Mentions: OAI.GammaFPP.IidEnvironment, OAI.GammaFPP.iidProductLaw

theorem OAI.GammaFPP.gammaProductLaw_environment line 41

Source documentation

Gamma product environments exist for every positive shape and rate.

theorem gammaProductLaw_environment (shape rate : ℝ)
    (hshape : 0 < shape) (hrate : 0 < rate) :
    GammaEnvironment shape rate (iidProductLaw (gammaMeasure shape rate))
      (fun e ω => ω e) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.iidProductLaw

theorem OAI.GammaFPP.IidEnvironment.finiteJointLaw line 53
Source documentation
The joint law on a finite set of edges, including the empty set.
```
theorem IidEnvironment.finiteJointLaw (h : IidEnvironment ν P τ)
    (S : Finset PlanarFPP.Edge) :
    P.map (fun ω (e : S) => τ e ω) = Measure.pi (fun _ : S => ν) := by
…
```
Mentions: OAI.GammaFPP.IidEnvironment, OAI.PlanarFPP.Edge
theorem OAI.GammaFPP.IidEnvironment.measurable_passageTime line 62
Source documentation
Passage time is measurable in an iid edge environment.
```
theorem IidEnvironment.measurable_passageTime (h : IidEnvironment ν P τ)
    (p q : PlanarFPP.Vertex) :
    Measurable (fun ω => PlanarFPP.passageTime (fun e => τ e ω) p q) :=
…
```
Mentions: OAI.GammaFPP.IidEnvironment, OAI.PlanarFPP.Vertex, OAI.PlanarFPP.passageTime
theorem OAI.GammaFPP.iid_expOne_iff line 68
Source documentation
The exponential environment with rate one is the corresponding iid environment.
```
theorem iid_expOne_iff :
    IidEnvironment (expMeasure 1) P τ ↔ PlanarFPP.ExponentialEnvironment P τ := by
…
```
Mentions: OAI.GammaFPP.IidEnvironment, OAI.PlanarFPP.ExponentialEnvironment