CubeOscillationHolder

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

From clipped oscillation decay to a Hölder seminorm on the whole cube

The Campanato/Morrey embedding, run on the windows clipped to a cube. Because the windows are clipped, the estimate is available at every centre of the cube, including centres arbitrarily close to its boundary, and the resulting Hölder seminorm bound is therefore a bound on the whole open cube rather than on an interior sub-cube.

The two-point argument is the unclipped one: two centres at distance at most the bracketing radius have their windows inside a common window of three times that radius, taken at the first of the two centres and clipped to the same cube. The only change is the price of each comparison, which is ballVolumePrice 6 d instead of ballVolumePrice 3 d because a clipped window may be half as wide as the unclipped one in every direction.

The chaining step is unchanged and is reused verbatim: it is a statement about a two-point bound on a convex set and knows nothing about windows.

Main definitions

• clipLocalHolderConstant d α — the explicit constant of the two-point bound.

Main results

• abs_campanatoRepresentative_sub_le_clip — the two-point bound for separations at most R, valid up to the boundary of the cube.
• holderSeminormBoundOn_clip_campanatoRepresentative — the embedding on a convex subset of the cube.
• holderSeminormBoundOn_cube_campanatoRepresentative — the embedding on the whole open cube.

1. The local two-point bound

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.clipLocalHolderConstant (d : ℕ) (alpha : ℝ) : ℝ

The constant of the two-point Hölder bound on clipped windows. The two summands are the geometric tail of the telescope and the enclosing-window comparison at the two centres; the outer factor 3 ^ α converts the bracketing radius into the separation.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.clipLocalHolderConstant_nonneg (d : ℕ) {alpha : ℝ} (halpha : 0 < alpha) : 0 ≤ clipLocalHolderConstant d alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.abs_campanatoRepresentative_sub_le_clip {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {S : Set (HCPolySupport.Vec d)} {R Rtop alpha K : ℝ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRtop : 3 * R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (halpha : 0 < alpha) (hK : 0 ≤ K) (hS : S ⊆ Metric.ball c Rm) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Metric.ball c Rm))) (hcamp : HasClipCampanatoDecayOn c Rm S Rtop alpha K f) {x y : HCPolySupport.Vec d} (hx : x ∈ S) (hy : y ∈ S) (hxy : ‖x - y‖ ≤ R) : |campanatoRepresentative f R x - campanatoRepresentative f R y| ≤ clipLocalHolderConstant d alpha * K * ‖x - y‖ ^ alpha

The two-point Hölder bound on the clipped windows. Both centres are arbitrary points of S, so the bound holds up to the boundary of the cube.

2. The embedding

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.holderSeminormBoundOn_clip_campanatoRepresentative {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {S W : Set (HCPolySupport.Vec d)} {R Rtop alpha K : ℝ} {N : ℕ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRtop : 3 * R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (halpha : 0 < alpha) (hK : 0 ≤ K) (hS : S ⊆ Metric.ball c Rm) (hW : Convex ℝ W) (hWS : W ⊆ S) (hN : 0 < N) (hdiam : ∀ x ∈ W, ∀ y ∈ W, ‖x - y‖ ≤ ↑N * R) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Metric.ball c Rm))) (hcamp : HasClipCampanatoDecayOn c Rm S Rtop alpha K f) : Section4.Support.HolderSeminormBoundOn W alpha (↑N ^ (1 - alpha) * (clipLocalHolderConstant d alpha * K)) (campanatoRepresentative f R)

The Campanato/Morrey embedding on a convex subset of the cube.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.holderSeminormBoundOn_cube_campanatoRepresentative {d : ℕ} {c : HCPolySupport.Vec d} {Rm R Rtop alpha K : ℝ} {N : ℕ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRtop : 3 * R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (halpha : 0 < alpha) (hK : 0 ≤ K) (hN : 0 < N) (hchain : 2 * Rm ≤ ↑N * R) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Metric.ball c Rm))) (hcamp : HasClipCampanatoDecayOn c Rm (Metric.ball c Rm) Rtop alpha K f) : Section4.Support.HolderSeminormBoundOn (Metric.ball c Rm) alpha (↑N ^ (1 - alpha) * (clipLocalHolderConstant d alpha * K)) (campanatoRepresentative f R)

The embedding on the whole open cube. The chain length N absorbs the ratio between the diameter 2 Rm of the cube and the top radius R of the telescope.