OffGridTransfer

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

Transferring clipped oscillation decay from lattice centres to every centre

A scale-by-scale regularity iteration run on a cube proves its oscillation estimate on the windows clipped to that cube, and only at the points of a triadic lattice: at each scale the centre must be a lattice point. A Hölder seminorm needs the estimate at every centre of the cube. This file performs the transfer and prices it exactly.

The mechanism is the only one available. Round the arbitrary centre x toward the centre of the cube at the spacing of the cube one triadic scale below the window; the displacement is then strictly below that spacing, so the window at x sits inside the lattice window one scale up, and

• the mean over the small window may be replaced by the mean over the large one at no cost, because the mean minimizes the deviation, and the two normalized L² norms then differ by at most 6 ^ (d/2) — the volume ratio of two clipped windows whose radii differ by a factor 3;
• the α-weight of the larger window is 3 ^ α times that of the smaller.

So the transfer costs the factor clipScaleStepConstant d α = 6 ^ (d/2) 3 ^ α and one triadic scale: a lattice family whose smallest available window index is j₀ yields an arbitrary-centre family whose smallest available window index is j₀ + 1. No smaller enclosing lattice window exists at the scale of the window itself: that would force the centre to be the lattice point.

Because the windows are clipped, there is no second scale loss. An enclosing lattice window is automatically inside the cube — it is clipped to it — so the lattice family may be used at every index it is available at, and the estimate reaches every centre of the cube, boundary included. Rounding toward the centre of the cube keeps the lattice centre inside the cube, which is what makes the lattice family applicable at it.

Main definitions

• HasClipGridOscillationDecay c Rm Grid Rtop α K j₀ f — the lattice-centred hypothesis: the estimate at window index j ≥ j₀ at every admissible centre z ∈ Grid j, on the window clipped to the cube.
• GridApproximatesOn Grid S Rtop j₀ — every centre of S has an admissible centre one scale up within twice the smaller radius.
• centredTriadicGrid c Rm Rtop — the concrete family of lattice centres of the cube B(c, Rm).

Main results

• hasClipTriadicOscillationDecayOn_of_grid — the transfer, with its constant and its loss of one triadic scale.
• gridApproximatesOn_centredTriadicGrid — the concrete family is fine enough, and rounding keeps the centre in the cube.

1. Iterating the triadic radius

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius_triadicRadius (R : ℝ) (k l : ℕ) : triadicRadius (triadicRadius R k) l = triadicRadius R (k + l)

Restarting the triadic radii at a radius of the same family shifts the index. This is the dictionary that turns a family available from index j₀ into a family available from index 0 at the smaller top radius.

2. The lattice-centred hypothesis

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

Oscillation decay on clipped windows at a scale-indexed family of admissible centres. Grid j is the set of centres at which the estimate is available for the window of index j, and the estimate is available only from the index j₀ on.

Equations

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

def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.GridApproximatesOn {d : ℕ} (Grid : ℕ → Set (HCPolySupport.Vec d)) (S : Set (HCPolySupport.Vec d)) (Rtop : ℝ) (j0 : ℕ) : Prop

The family is fine enough to carry every centre of S. Each centre of S admits, at every available index j, an admissible centre for the window of index j within twice the radius of the window of index j + 1. That is exactly the tolerance under which the window of index j + 1 at the arbitrary centre is contained in the window of index j at the admissible centre.

Equations

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

3. The transfer

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.hasClipTriadicOscillationDecayOn_of_grid {d : ℕ} {c : HCPolySupport.Vec d} {Rm : ℝ} {Grid : ℕ → Set (HCPolySupport.Vec d)} {S : Set (HCPolySupport.Vec d)} {Rtop alpha K : ℝ} {j0 : ℕ} {f : HCPolySupport.Vec d → ℝ} (hRtop : 0 < Rtop) (hRtopRm : Rtop ≤ Rm) (hS : S ⊆ Metric.ball c Rm) (hGrid : ∀ (j : ℕ), Grid j ⊆ Metric.ball c Rm) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Metric.ball c Rm))) (hdec : HasClipGridOscillationDecay c Rm Grid Rtop alpha K j0 f) (happ : GridApproximatesOn Grid S Rtop j0) : HasClipTriadicOscillationDecayOn c Rm S (triadicRadius Rtop (j0 + 1)) alpha (clipScaleStepConstant d alpha * K) f

The off-grid transfer on clipped windows. From oscillation decay at the admissible centres of a scale-indexed family, available from index j₀, one obtains oscillation decay at every centre of S, from index j₀ + 1 on — that is, with the top radius pushed down by exactly one triadic scale — at the cost of the factor clipScaleStepConstant d α in the constant.

4. The concrete triadic family on a cube

def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.centredTriadicGrid {d : ℕ} (c : HCPolySupport.Vec d) (Rm Rtop : ℝ) : ℕ → Set (HCPolySupport.Vec d)

The concrete family of admissible centres. At window index j the admissible centres are the points of the lattice through c of spacing 2 triadicRadius Rtop (j + 1) — the side of the cube one triadic scale below the window — that lie in the cube.

Equations

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

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.centredTriadicGrid_subset {d : ℕ} (c : HCPolySupport.Vec d) (Rm Rtop : ℝ) (j : ℕ) : centredTriadicGrid c Rm Rtop j ⊆ Metric.ball c Rm

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.gridApproximatesOn_centredTriadicGrid {d : ℕ} {Rtop : ℝ} (hRtop : 0 < Rtop) (c : HCPolySupport.Vec d) (Rm : ℝ) (j0 : ℕ) : GridApproximatesOn (centredTriadicGrid c Rm Rtop) (Metric.ball c Rm) Rtop j0

The concrete family is fine enough, and rounding keeps the centre in the cube. Rounding toward the centre of the cube is what supplies the second half: the rounded centre never leaves the cube, so the lattice family applies at it.