CubeTelescope

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

The Campanato telescope on windows clipped to a cube

This file runs the triadic Campanato telescope with the windows clipped to a cube, so that the resulting estimate reaches the boundary of the cube rather than an interior sub-cube.

The construction is the unclipped one, with two changes. Every volume ratio is paid at ballVolumePrice 6 d = 6 ^ (d/2) rather than 3 ^ (d/2), because a clipped window can be half as wide as the unclipped one in every direction; and the enclosing window of the geometric step is taken at the same centre, so the step needs no room above the top radius.

The limit of the clipped telescope is the same function as the limit of the unclipped one: at a centre of the open cube the clipping is eventually inactive, so the two sequences of means have the same tail. Everything is therefore stated for campanatoRepresentative, and the clipped theory only supplies bounds for it that are valid up to the boundary.

Main definitions

• HasClipCampanatoDecayOn c Rm S Rtop α K f — oscillation decay on the clipped windows, at every radius.
• HasClipTriadicOscillationDecayOn c Rm S Rtop α K f — the same at the discrete triadic radii only.
• clipScaleStepConstant d α — the price 6 ^ (d/2) 3 ^ α of one triadic step on clipped windows.
• clipCampanatoAverage c Rm f R x k — the mean over the clipped window.

Main results

• hasClipCampanatoDecayOn_of_triadic — the discrete family controls every radius.
• dist_clipCampanatoAverage_succ_le — the geometric bound on consecutive means.
• tendsto_clipCampanatoAverage — the clipped means converge to campanatoRepresentative.
• dist_clipCampanatoAverage_representative_le — the uniform tail.
• campanatoRepresentative_ae_eq_of_clip — the limit is a representative of f.

1. The hypotheses

def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.HasClipCampanatoDecayOn {d : ℕ} (c : HCPolySupport.Vec d) (Rm : ℝ) (S : Set (HCPolySupport.Vec d)) (Rtop alpha K : ℝ) (f : HCPolySupport.Vec d → ℝ) : Prop

Campanato oscillation decay on the clipped windows: the volume-normalized L² oscillation on B(x, r) ∩ B(c, Rm) is at most K r ^ α for every centre x ∈ S and every radius 0 < r ≤ Rtop.

Equations

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

def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.HasClipTriadicOscillationDecayOn {d : ℕ} (c : HCPolySupport.Vec d) (Rm : ℝ) (S : Set (HCPolySupport.Vec d)) (Rtop alpha K : ℝ) (f : HCPolySupport.Vec d → ℝ) : Prop

Oscillation decay on the clipped windows at the discrete triadic radii only. This is the shape a scale-by-scale iteration produces.

Equations

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

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

The price of one triadic step between clipped windows: the volume ratio 6 ^ (d/2) and the α-weight 3 ^ α.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.clipScaleStepConstant d alpha = Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballVolumePrice 6 d * 3 ^ alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.clipScaleStepConstant_nonneg (d : ℕ) (alpha : ℝ) : 0 ≤ clipScaleStepConstant d alpha

2. From the discrete scales to all radii

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.hasClipCampanatoDecayOn_of_triadic {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {S : Set (HCPolySupport.Vec d)} {Rtop alpha K : ℝ} {f : HCPolySupport.Vec d → ℝ} (hRtop : 0 < 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))) (hdisc : HasClipTriadicOscillationDecayOn c Rm S Rtop alpha K f) : HasClipCampanatoDecayOn c Rm S Rtop alpha (clipScaleStepConstant d alpha * K) f

The discrete clipped family controls every radius.

3. The clipped telescope

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

The mean of f over the clipped window of radius R 3 ^ (-k) at x.

Equations

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

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.dist_clipCampanatoAverage_succ_le {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {S : Set (HCPolySupport.Vec d)} {R Rtop alpha K : ℝ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRRtop : R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (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 : HCPolySupport.Vec d} (hx : x ∈ S) (k : ℕ) : dist (clipCampanatoAverage c Rm f R x k) (clipCampanatoAverage c Rm f R x (k + 1)) ≤ Ported.ballVolumePrice 6 d * K * R ^ alpha * campanatoRatio alpha ^ k

Consecutive means of the clipped telescope differ geometrically.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.cauchySeq_clipCampanatoAverage {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {S : Set (HCPolySupport.Vec d)} {R Rtop alpha K : ℝ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRRtop : R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (halpha : 0 < alpha) (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 : HCPolySupport.Vec d} (hx : x ∈ S) : CauchySeq (clipCampanatoAverage c Rm f R x)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.tendsto_clipCampanatoAverage {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {S : Set (HCPolySupport.Vec d)} {R Rtop alpha K : ℝ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRRtop : R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (halpha : 0 < alpha) (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 : HCPolySupport.Vec d} (hx : x ∈ S) : Filter.Tendsto (clipCampanatoAverage c Rm f R x) Filter.atTop (nhds (campanatoRepresentative f R x))

The clipped telescope has the same limit as the unclipped one. At a centre of the open cube the clipping is eventually inactive, so the two sequences of means agree from some index on.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.dist_clipCampanatoAverage_representative_le {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {S : Set (HCPolySupport.Vec d)} {R Rtop alpha K : ℝ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRRtop : R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (halpha : 0 < alpha) (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 : HCPolySupport.Vec d} (hx : x ∈ S) (k : ℕ) : dist (clipCampanatoAverage c Rm f R x k) (campanatoRepresentative f R x) ≤ campanatoTailConstant alpha * Ported.ballVolumePrice 6 d * K * triadicRadius R k ^ alpha

The uniform tail of the clipped telescope.

4. The limit is a representative

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoRepresentative_ae_eq_of_clip {d : ℕ} [NeZero d] {c : HCPolySupport.Vec d} {Rm : ℝ} {S : Set (HCPolySupport.Vec d)} {R Rtop alpha K : ℝ} {f : HCPolySupport.Vec d → ℝ} (hR : 0 < R) (hRRtop : R ≤ Rtop) (hRtopRm : Rtop ≤ Rm) (halpha : 0 < alpha) (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) (hint : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) : ∀ᵐ (x : HCPolySupport.Vec d), x ∈ S → campanatoRepresentative f R x = f x

Lebesgue differentiation identifies the limit with f.