LocalResamplingExponential.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.FiniteLocal.sum_upward_transform line 13

Source documentation

A single minimizing trail bounds the summed upward resampling increments for every replacement law supported on nonnegative weights.

theorem sum_upward_transform (μ : Measure ℝ) (hμ : ∀ᵐ u ∂μ, 0 ≤ u)
    (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e) (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) (φ : ℝ → ℝ≥0∞)
    (hφ : MonotoneOn φ (Set.Ici 0)) (hzero : φ 0 = 0) :
    (∑ e ∈ localEdges p q R, ∫⁻ u, φ (upward w p q R e u) ∂μ) ≤
      (∫⁻ u, φ u ∂μ) * R := by
…

Mentions: OAI.GammaFPP.FiniteLocal.localEdges, OAI.GammaFPP.FiniteLocal.upward

lemma OAI.GammaFPP.FiniteLocal.exponential_increment_monotone line 56
Source documentation
Scalar monotonicity holds for negative as well as positive a.
```
lemma exponential_increment_monotone (a : ℝ) :
    MonotoneOn (fun u => ENNReal.ofReal ((exp (a*u/2)-1)^2)) (Set.Ici 0) := by
…
```
lemma OAI.GammaFPP.FiniteLocal.gamma_lintegral_half_exp_increment_square_le line 70

theorem OAI.GammaFPP.FiniteLocal.sum_upward_exponential line 80

Source documentation

Quadratic Gamma proxy, uniform in ambient edge-set cardinality.

theorem sum_upward_exponential {shape rate : ℝ} (hs : 0 < shape) (hr : 0 < rate)
    (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e) (p q : Vertex) (R : ℕ)
    (hR : latticeDistance p q < R) (a : ℝ) (ha : |a| ≤ rate/4) :
    (∑ e ∈ localEdges p q R, ∫⁻ u, ENNReal.ofReal
      ((exp (a * upward w p q R e u / 2)-1)^2) ∂gammaMeasure shape rate) ≤
      ENNReal.ofReal ((8*(2 : ℝ)^shape/rate^2)*a^2) * R := by
…

Mentions: OAI.GammaFPP.FiniteLocal.localEdges, OAI.GammaFPP.FiniteLocal.upward

theorem OAI.GammaFPP.FiniteLocal.finite_upward_exponential_sum line 93

Source documentation

The summed exponential upward increments are bounded uniformly over every nonnegative finite coordinate assignment.

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

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