OscillationHolder

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Convex chaining and continuity from a Hölder bound

A local two-point Hölder estimate globalizes across a convex set by subdividing each segment. This file also records the elementary ball geometry and the continuity consequence of a positive Hölder exponent.

Main results

• holderSeminormBoundOn_of_local_of_convex — convex chaining, at the sharp price N ^ (1 - α) for N steps.
• norm_sub_le_two_mul_of_mem_ball — the diameter bound for a sup-ball.
• continuousOn_of_holderBound — a Hölder modulus is a modulus of continuity, for every positive exponent.

1. Convex chaining

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.holderSeminormBoundOn_of_local_of_convex {d : ℕ} {W : Set (HCPolySupport.Vec d)} {alpha L ell : ℝ} {N : ℕ} {G : HCPolySupport.Vec d → ℝ} (hW : Convex ℝ W) (hN : 0 < N) (hdiam : ∀ x ∈ W, ∀ y ∈ W, ‖x - y‖ ≤ ↑N * ell) (hloc : ∀ x ∈ W, ∀ y ∈ W, ‖x - y‖ ≤ ell → |G x - G y| ≤ L * ‖x - y‖ ^ alpha) : Section4.Support.HolderSeminormBoundOn W alpha (↑N ^ (1 - alpha) * L) G

Convex chaining. A Hölder bound valid for separations at most ell globalizes to a convex set of diameter at most N * ell, at the price N ^ (1 - α).

2. Ball geometry

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.norm_sub_le_two_mul_of_mem_ball {d : ℕ} {x0 : HCPolySupport.Vec d} {rho : ℝ} {x y : HCPolySupport.Vec d} (hx : x ∈ Metric.ball x0 rho) (hy : y ∈ Metric.ball x0 rho) : ‖x - y‖ ≤ 2 * rho

Two points of a sup-ball are separated by at most twice its radius.

3. Continuity

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.continuousOn_of_holderBound {d : ℕ} {W : Set (HCPolySupport.Vec d)} {alpha L : ℝ} {G : HCPolySupport.Vec d → ℝ} (halpha : 0 < alpha) (hL : 0 ≤ L) (hholder : ∀ x ∈ W, ∀ y ∈ W, |G x - G y| ≤ L * ‖x - y‖ ^ alpha) : ContinuousOn G W

A Hölder modulus is a modulus of continuity, for every positive exponent. The explicit modulus is (ε / (L + 1)) ^ (1 / α), so no restriction on α is needed.