CubeWindow #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Windows clipped to a cube, and their volume #
A regularity iteration run on a cube states its oscillation estimate on the
windows clipped to that cube: the window at a centre x and scale r is
(x + □) ∩ □_m, not x + □. Away from the boundary the two agree, but the
whole interest of a boundary-to-boundary Hölder estimate is at centres for which
they do not.
In the ambient space Vec d = Fin d → ℝ the metric is the supremum norm, so a
clipped window is the intersection of two boxes and is again a box. Its volume
is therefore easy to bracket, and the bracket is all the Campanato theory needs:
- every clipped window sits in the unclipped one, so its volume is at most
(2 r) ^ d; - a clipped window of a centre inside the cube contains a ball of radius
r / 2, so its volume is at leastr ^ d.
The lower bound is the only substantive point. Pushing the centre toward the
face of the cube shrinks one side of the window, but never below r: the side
lost on one face is gained on the other. The explicit inner ball is centred at
the projection of x onto the concentric cube of half-side Rm - r / 2.
The consequence is that all the volume ratios of the theory are bounded by
(2 R / r) ^ d instead of (R / r) ^ d: clipping costs a factor 2 ^ d in the
volume, i.e. 2 ^ (d/2) in the normalized L² price, once and for all.
Main definitions #
Main results #
exists_ball_subset_clipBall— the inner ball of radiusr / 2.pow_le_volume_clipBall_toReal,volume_clipBall_toReal_le— the volume bracketr ^ d ≤ |W| ≤ (2 r) ^ d.sqrt_volume_clipBall_ratio_le— the normalized-L²price of two clipped windows,ballVolumePrice κ dwhenever2 R ≤ κ r.oscillation_clipBall_le_of_subset— the mean-oscillation comparison between nested clipped windows.abs_volumeAverage_clipBall_sub_le— the mean comparison between nested clipped windows.eventually_clipBall_eq_ball— at an interior centre the clipping is eventually inactive, which is what identifies the clipped telescope's limit with the unclipped one.
1. The clipped window #
The window at x and scale r, clipped to the cube B(c, Rm). In the
supremum metric of Vec d this is the intersection of the open cube of side
2 r centred at x with the open cube of side 2 Rm centred at c.
Equations
Instances For
A clipped window at a nearby centre and a larger scale contains the given one.
The clipping is inactive when the unclipped window already sits in the cube.
2. The inner ball #
A clipped window of an interior centre contains a ball of half the
radius. The centre of that ball is the projection of x onto the cube
concentric with the ambient one of half-side Rm - r / 2: moving x toward the
centre by less than r / 2 buys the room the clipping took away.
3. The volume bracket #
The volume lower bound. Clipping a window at an interior centre costs at
most the factor 2 ^ d.
The normalized-L² price of two clipped windows. The numerator is at
most (2 R) ^ d and the denominator at least r ^ d, so the price is
ballVolumePrice κ d for any κ with 2 R ≤ κ r.
4. The two comparisons on nested clipped windows #
The mean-oscillation comparison between nested clipped windows.
The mean comparison between nested clipped windows.
5. The clipping is eventually inactive at an interior centre #
At a centre of the open cube the triadic windows are eventually untruncated: the clipped and unclipped telescopes have the same tail, hence the same limit.