OAI/Probability/GammaPassage/LocalExponentialEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.FiniteLocal.finite_coordinates_nonnegative line 12
2. theorem OAI.GammaFPP.FiniteLocal.finite_exponential_forward_energy line 24

   Source documentation

   The forward resampling energy is bounded after weighting by the exponential of the passage time in the initial environment.

   theorem finite_exponential_forward_energy {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R)
       (a : ℝ) (ha : |a| ≤ rate/4) :
       (∑ e : ↥(localEdges p q R), ∫⁻ z : Coordinates p q R × Coordinates p q R,
         ENNReal.ofReal (exp (a*finitePassageTime p q R z.1) *
           (exp (a*max (finitePassageTime p q R (Function.update z.1 e (z.2 e))-
             finitePassageTime p q R z.1) 0/2)-1)^2)
         ∂(finiteGammaMeasure shape rate).prod (finiteGammaMeasure shape rate)) ≤
         (ENNReal.ofReal ((8*(2 : ℝ)^shape/rate^2)*a^2)*R) *
           ∫⁻ v, ENNReal.ofReal (exp (a*finitePassageTime p q R v))
             ∂finiteGammaMeasure shape rate := by
   …

   Mentions: OAI.GammaFPP.FiniteLocal.localEdges, OAI.GammaFPP.FiniteLocal.Coordinates, OAI.GammaFPP.FiniteLocal.finitePassageTime, OAI.GammaFPP.finiteGammaMeasure

3. theorem OAI.GammaFPP.FiniteLocal.finite_exponential_resampling_energy line 81

   Source documentation

   Exchanging the initial and resampled coordinates bounds the total exponential resampling energy by twice the forward energy, for either sign of a.

   theorem finite_exponential_resampling_energy {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate)
       (p q : Vertex) (R : ℕ) (hR : latticeDistance p q < R)
       (a : ℝ) (ha : |a| ≤ rate/4) :
       (∑ e : ↥(localEdges p q R), ∫⁻ z : Coordinates p q R × Coordinates p q R,
         ENNReal.ofReal ((exp (a*finitePassageTime p q R (Function.update z.1 e (z.2 e))/2) -
           exp (a*finitePassageTime p q R z.1/2))^2)
         ∂(finiteGammaMeasure shape rate).prod (finiteGammaMeasure shape rate)) ≤
         (ENNReal.ofReal ((16*(2 : ℝ)^shape/rate^2)*a^2)*R) *
           ∫⁻ v, ENNReal.ofReal (exp (a*finitePassageTime p q R v))
             ∂finiteGammaMeasure shape rate := by
   …

   Mentions: OAI.GammaFPP.FiniteLocal.localEdges, OAI.GammaFPP.FiniteLocal.Coordinates, OAI.GammaFPP.FiniteLocal.finitePassageTime, OAI.GammaFPP.finiteGammaMeasure