MeanLipschitz.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.coordinate_path_length_l1 line 15
Source documentation
The horizontal-then-vertical coordinate path has exactly the lattice L¹ length.
```
private theorem coordinate_path_length_l1 (p q : Vertex) :
    (coordinatePath p q).length = latticeDistance p q := by
…
```

theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_le_l1 line 26

Source documentation

The finite first-moment path bound controls the actual Fekete constant.

theorem GammaEnvironment.directionalMeanConstant_le_l1
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (z : Vertex) :
    directionalMeanConstant h hs hr z ≤
      (shape / rate) * ((z.1.natAbs + z.2.natAbs : ℕ) : ℝ) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant

theorem OAI.GammaFPP.GammaEnvironment.abs_directionalMeanConstant_sub_le line 37

Source documentation

Reverse triangle inequality for the actual lattice mean constants.

theorem GammaEnvironment.abs_directionalMeanConstant_sub_le
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (x y : Vertex) :
    |directionalMeanConstant h hs hr x - directionalMeanConstant h hs hr y| ≤
      directionalMeanConstant h hs hr (x - y) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant

theorem OAI.GammaFPP.GammaEnvironment.directionalMeanConstant_l1_lipschitz line 55

Source documentation

L1-Lipschitz estimate, with the true Gamma mean shape/rate, all lattice vertices, and no time-norm, positivity-of-limit or almost-sure premise.

theorem GammaEnvironment.directionalMeanConstant_l1_lipschitz
    (h : GammaEnvironment shape rate P τ) (hs : 0 < shape) (hr : 0 < rate)
    (x y : Vertex) :
    |directionalMeanConstant h hs hr x - directionalMeanConstant h hs hr y| ≤
      (shape / rate) * (((x.1-y.1).natAbs + (x.2-y.2).natAbs : ℕ) : ℝ) := by
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.directionalMeanConstant