TriadicTelescope #

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

Canonical averages on shrinking triadic balls #

This file records the means of a function on the balls with radii R 3 ^ (-k) and the corresponding limit-based representative.

Main definitions #

campanatoAverage f R x k, campanatoRepresentative f R x.

Averages and representative #

source

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoAverage {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (R : ℝ) (x : HCPolySupport.Vec d) (k : ℕ) :

ℝ

The mean of f over the sup-ball of radius R 3 ^ (-k) centred at x.

Equations

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

Instances For

source

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoRepresentative {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (R : ℝ) (x : HCPolySupport.Vec d) :

ℝ

The canonical Campanato representative: the limit of the means over the shrinking triadic balls at x.