CubeRepresentative

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

The continuous representative produced by the clipped-window family

A clipped-window oscillation family on the origin cube produces, through the Campanato characterisation of Hölder spaces on a cube, a representative that is continuous up to the boundary and carries an explicit C^{0,beta} seminorm bound. This file packages that passage in the form the localized estimates consume: a witness of IsCubeRepresentative on the translated cube y + □_m together with the seminorm bound.

Two adjustments are made along the way.

• The Campanato telescope is a statement about averages over balls of the ambient space, so it needs a globally locally integrable function; the family only controls the solution inside the cube. Both are reconciled by running the telescope on the extension by zero, which agrees with the solution on the cube and is globally square integrable. Every window of the family lies inside the cube, so the family itself is unchanged.
• The family lives at the origin and the estimate is read at the centre y, so the representative is recentred; the Hölder seminorm on a cube is invariant under that recentring.

Main results

• hasClipGridOscillationDecay_congr — the family depends only on the values inside the ambient ball.
• clipOffGridHolderConstant_le_uniform — the chaining constant of the cube is bounded uniformly on 1/2 ≤ beta ≤ 1.
• exists_cubeRepresentative_of_grid — the packaged representative.

1. Congruence of the oscillation family

theorem Algsuperdiff.Section4.Provider.Holder.hasClipGridOscillationDecay_congr {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {Grid : ℕ → Set (HCPolySupport.Vec d)} {Rtop alpha K : ℝ} {j0 : ℕ} {f g : HCPolySupport.Vec d → ℝ} (h : Set.EqOn f g (Metric.ball c Rm)) (hdec : StochasticProcess.Common.Regularity.Campanato.HasClipGridOscillationDecay c Rm Grid Rtop alpha K j0 f) : StochasticProcess.Common.Regularity.Campanato.HasClipGridOscillationDecay c Rm Grid Rtop alpha K j0 g

The clipped-window oscillation decay depends only on the values inside the ambient ball.

2. A constant uniform over the upper half of the exponent range

noncomputable def Algsuperdiff.Section4.Provider.Holder.uniformCubeHolderConstant (d : ℕ) : ℝ

The chaining constant of the cube, read uniformly on 1/2 ≤ alpha ≤ 1.

Equations

• Algsuperdiff.Section4.Provider.Holder.uniformCubeHolderConstant d = 5832 * Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballVolumePrice 6 d ^ 3

theorem Algsuperdiff.Section4.Provider.Holder.uniformCubeHolderConstant_nonneg (d : ℕ) : 0 ≤ uniformCubeHolderConstant d

theorem Algsuperdiff.Section4.Provider.Holder.clipOffGridHolderConstant_le_uniform (d : ℕ) {beta : ℝ} (h1 : 1 / 2 ≤ beta) (h2 : beta ≤ 1) : StochasticProcess.Common.Regularity.Campanato.clipOffGridHolderConstant d beta 18 ≤ uniformCubeHolderConstant d

3. The continuous representative on y + □_m

theorem Algsuperdiff.Section4.Provider.Holder.exists_cubeRepresentative_of_grid {d : ℕ} [NeZero d] {y : HCPolySupport.Vec d} {m : ℤ} {beta K : ℝ} (hbeta : 0 < beta) (hK : 0 ≤ K) (u : HCPolySupport.H1Function (Section5.Support.cubeSetAt y m)) (hdec : StochasticProcess.Common.Regularity.Campanato.HasClipGridOscillationDecay 0 (3 ^ m / 2) (StochasticProcess.Common.Regularity.Campanato.centredTriadicGrid 0 (3 ^ m / 2) (3 ^ m / 2)) (3 ^ m / 2) beta K 0 (Section5.Support.originPullback y m u).toFun) : ∃ (uRep : HCPolySupport.Vec d → ℝ), Section5.Support.IsCubeRepresentative y m u uRep ∧ Section5.Support.holderSeminormOn (Section5.Support.cubeSetAt y m) beta uRep ≤ ENNReal.ofReal (StochasticProcess.Common.Regularity.Campanato.clipOffGridHolderConstant d beta 18 * K)

From the clipped-window oscillation family at the origin to a continuous representative on y + □_m.