FiniteMoments.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.edgeSum line 18
Source documentation
The cost of a deterministic finite set of distinct undirected edges.
```
def edgeSum (S : Finset PlanarFPP.Edge) (τ : PlanarFPP.Edge → Ω → ℝ) (ω : Ω) : ℝ :=
…
```
Mentions: OAI.PlanarFPP.Edge
lemma OAI.GammaFPP.edgeSum_empty line 22
lemma OAI.GammaFPP.IidEnvironment.measurable_edgeSum line 25

lemma OAI.GammaFPP.IidEnvironment.integral_finiteJoint line 30

Source documentation

Integral transport along the joint law of a finite edge set.

lemma IidEnvironment.integral_finiteJoint (h : IidEnvironment ν P τ)
    (S : Finset PlanarFPP.Edge) (f : (S → ℝ) → ℝ) (hf : Measurable f) :
    (∫ ω, f (fun e : S => τ e ω) ∂P) =
      ∫ x : S → ℝ, f x ∂Measure.pi (fun _ : S => ν) := by
…

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

theorem OAI.GammaFPP.GammaEnvironment.integral_exp_edgeSum line 42

Source documentation

The exponential moment of a finite edge sum, obtained by finite-product integration.

theorem GammaEnvironment.integral_exp_edgeSum
    (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
    (htheta : theta < rate) (S : Finset PlanarFPP.Edge) :
    (∫ ω, Real.exp (theta * edgeSum S τ ω) ∂P) =
      ((rate / (rate - theta)) ^ shape) ^ S.card := by
…

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

theorem OAI.GammaFPP.GammaEnvironment.lintegral_exp_edgeSum line 63

Source documentation

The nonnegative exponential moment of a finite iid Gamma edge sum.

theorem GammaEnvironment.lintegral_exp_edgeSum
    (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
    (htheta : theta < rate) (S : Finset PlanarFPP.Edge) :
    (∫⁻ ω, ENNReal.ofReal (Real.exp (theta * edgeSum S τ ω)) ∂P) =
      (ENNReal.ofReal ((rate / (rate - theta)) ^ shape)) ^ S.card := by
…

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

theorem OAI.GammaFPP.GammaEnvironment.integrable_exp_edgeSum line 92

Source documentation

Exponential functions of finite edge sums are integrable for theta < rate.

theorem GammaEnvironment.integrable_exp_edgeSum
    (h : GammaEnvironment shape rate P τ) (hshape : 0 < shape) (hrate : 0 < rate)
    (htheta : theta < rate) (S : Finset PlanarFPP.Edge) :
    Integrable (fun ω => Real.exp (theta * edgeSum S τ ω)) P := by
…

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