OAI/Probability/GammaPassage/PathSecondMoment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.pathSecondMomentConstant line 16
2. lemma OAI.GammaFPP.square_le_gamma_exp line 19
3. lemma OAI.GammaFPP.gamma_integrable_square_bound line 29
4. lemma OAI.GammaFPP.gamma_integral_square_le line 37
5. lemma OAI.GammaFPP.GammaEnvironment.integrable_edge_square line 59
6. lemma OAI.GammaFPP.GammaEnvironment.integral_edge_square_le line 67
7. lemma OAI.GammaFPP.GammaEnvironment.pathCost_memLp_two line 76
8. lemma OAI.GammaFPP.pathCost_eq_indexed_trace line 90

   Source documentation

   The path cost is a sum over ordered traversal positions, including repeated edges.

   lemma pathCost_eq_indexed_trace (w : Edge → ℝ) (p : Vertex) (ds : List Step) :
       pathCost w p ds =
         ∑ i : Fin ((trace p ds).map traversalEdge).length,
           w (((trace p ds).map traversalEdge).get i) := by
   …

9. lemma OAI.GammaFPP.pathCost_square_le_indexed line 100

   Source documentation

   Finite Cauchy–Schwarz bounds the square of a sum for every real assignment.

   lemma pathCost_square_le_indexed (w : Edge → ℝ) (p : Vertex) (ds : List Step) :
       (pathCost w p ds)^2 ≤ (ds.length : ℝ) *
         ∑ i : Fin ((trace p ds).map traversalEdge).length,
           (w (((trace p ds).map traversalEdge).get i))^2 := by
   …

10. theorem OAI.GammaFPP.GammaEnvironment.pathCost_second_moment_le line 112

    Source documentation

    A polynomial second-moment bound for every deterministic finite step list.

    theorem GammaEnvironment.pathCost_second_moment_le
        (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
        (p : Vertex) (ds : List Step) :
        (∫ ω, (pathCost (fun e => τ e ω) p ds)^2 ∂P) ≤
          pathSecondMomentConstant shape rate * (ds.length : ℝ)^2 := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.pathSecondMomentConstant

11. theorem OAI.GammaFPP.GammaEnvironment.coordinatePath_second_moment_le line 141

    Source documentation

    A polynomial second-moment bound for the deterministic coordinate path.

    theorem GammaEnvironment.coordinatePath_second_moment_le
        (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
        (p q : Vertex) :
        (∫ ω, (pathCost (fun e => τ e ω) p (coordinatePath p q))^2 ∂P) ≤
          pathSecondMomentConstant shape rate * ((coordinatePath p q).length : ℝ)^2 :=
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.pathSecondMomentConstant