OAI/Probability/GammaPassage/EndpointCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GammaFPP.GammaEnvironment.two_attachment_cost_probability line 13

   Source documentation

   Combined attachment cost for a real distance budget, without an independence assumption between the attachments.

   theorem GammaEnvironment.two_attachment_cost_probability
       (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
       (p p' q' q : Vertex) (L t : ℝ)
       (hdist : (latticeDistance p p' : ℝ) + (latticeDistance q' q : ℝ) ≤ L) :
       P.real {ω | coordinateAllowance shape rate * L + t ≤
         pathCost (fun e => τ e ω) p (coordinatePath p p') +
         pathCost (fun e => τ e ω) q' (coordinatePath q' q)} ≤
         4 * Real.exp (-(rate / 8) * t) := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.coordinateAllowance

2. theorem OAI.GammaFPP.endpoint_net_budget line 49

   Source documentation

   A finite-net attachment allowance exists for every positive Gamma law and every norm Lipschitz constant.

   theorem endpoint_net_budget (hs : 0 < shape) (hr : 0 < rate)
       (β η δ : ℝ) (hβ : 0 ≤ β) (hη : 0 < η) (hδ : 0 < δ) :
       ∃ γ : ℝ, 0 < γ ∧
         (4 * coordinateAllowance shape rate + 2*β)*γ ≤ η/2 ∧ γ ≤ δ/12 := by
   …

   Mentions: OAI.GammaFPP.coordinateAllowance