OscillationCubeFamily #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The concentric triadic cube family of e.nablaw.oscillations #
e.nablaw.oscillations is stated for a mesh point z in 3^n Zd ∩ cu_K with `z
- cu_{m-h} ⊆ cu_K
, and compares the oscillation ofgrad wonz + cu_nwith its size onz + cu_{m-h}`. Its proof passes through every intermediate scale. The carrier is therefore the family of concentric open cubes
U_j := z + cu_{n+j} = openCubeAtScale z (n + j) , 0 ≤ j ≤ m - h - n ,
all centred at the same z. Only U_0 is a triadic cube in the lattice sense
(z ∈ 3^n Zd); the coarser members U_j, j ≥ 1, are cubes of side 3^{n+j}
centred at a point of the finer lattice, so they are not members of
Homogenization.TriadicCube at their own scale. This is why the whole argument
must be run on Homogenization.openCubeAtScale, and why this module exists.
CoarseGraining supplies openCubeAtScale together with openness,
measurability, the product description, the translation identity and the
dilation identity, but no nesting, no volume and no convexity. Those three
facts are what the nested-recentring route consumes from the cube family
itself, and they are proved here.
Contents #
openCubeAtScale_subset_of_forall_abs_add_le-- the general concentric / off-centre containment criterion, from which bothz + cu_n ⊆ z + cu_{n+j}andz + cu_{m-h} ⊆ cu_Kfollow.openCubeAtScale_subset_of_le-- nesting in the scale.volume_openCubeAtScale,volume_openCubeAtScale_toReal-- the exact volume(3^m)^d, with positivity and finiteness.convex_openCubeAtScale-- convexity, the hypothesis of the mean-value inequality used to convertsup |grad h|into an oscillation bound.
References #
- ABK26,
e.nablaw.oscillations.
Membership in the concentric cube z + cu_m, with the half-width written as
an integer power of three.
The containment criterion.
If every coordinate of the offset z - w is small enough to fit the cube of
scale m inside the cube of scale n, then it does. Taking z = w gives the
concentric nesting z + cu_m ⊆ z + cu_n for m ≤ n; taking w = 0, n = K
gives the interior-mesh hypothesis z + cu_{m-h} ⊆ cu_K of
e.nablaw.oscillations.
Concentric nesting: the cube family U_j = z + cu_{n+j} is increasing.
The exact Lebesgue volume of a concentric triadic cube.
Convexity of the concentric cube, the hypothesis under which the mean-value
inequality turns a bound on sup |grad h| into the birth-scale forcing size.