Ehrhart volume inequality: Convexity

Physical-measure, convexity, and probability-transfer arguments.

theorem Ehrhart.BergmanJetGlobalLogKernelEquiLipschitz.tendsto_of_dense_eventually_equiLipschitz {X : Type u_1} [PseudoMetricSpace X] (f : ℕ → X → ℝ) (g : X → ℝ) (C : NNReal) (hf : ∀ᶠ (k : ℕ) in Filter.atTop, LipschitzWith C (f k)) (hg : LipschitzWith C g) {S : Set X} (hS : Dense S) (hconv : ∀ y ∈ S, Filter.Tendsto (fun (k : ℕ) => f k y) Filter.atTop (nhds (g y))) (x : X) : Filter.Tendsto (fun (k : ℕ) => f k x) Filter.atTop (nhds (g x))

Equi-Lipschitz functions converging on a dense set converge everywhere.