StepNineOffGridTransfer #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
t.regularity off-grid transfer: the quantity #
What is transferred #
StepNineOffGridGeometry supplies the inclusion of windows
(x + □_n) ∩ □_m ⊆ (z + □_{n+1}) ∩ □_m , z = offGridCentre n x .
A volume-normalized norm is NOT monotone under inclusion: passing to the smaller window costs the volume ratio. This module prices that ratio and proves the transfer in BOTH carriers the development uses:
- the
ℝ≥0∞-valuedeLpNorm · 2 (normalizedVolumeMeasureOn ·)of the frozen root's left-hand side (e.energy.density.estimate), where the transfer needs NO integrability hypothesis at all — theℝ≥0∞monotonicityeLpNorm_mono_measureis unconditional; - the
ℝ-valuedSupport.normalizedL2Onof the proved Step-7 chain, where theIntegrableOndatum of theH¹solution is the carried hypothesis ofSupport.normalizedL2On_le_of_subset.
The volume accounting #
Upper bound: (z+□_{n+1}) ∩ □_m ⊆ z + □_{n+1}, of volume 3^{d(n+1)}.
Lower bound: (x+□_n) ∩ □_m contains a translate of □_{n−1}
(exists_inner_cube_subset_truncatedWindow; the truncated interval is at least
3^n/2 long in each coordinate and 3^{n−1} = 3^n/3 ≤ 3^n/2), of volume
3^{d(n−1)}.
Hence the ratio is at most 3^{2d} = 9^d and the NO factor is 3^d:
‖f‖_{L²((x+□_n) ∩ □_m)} ≤ 3^d · ‖f‖_{L²((z+□_{n+1}) ∩ □_m)} .
records the price of the off-grid step as 3^{d+1} (there: 3^d for the
untruncated volume ratio of the squared average, times 3 for the Campanato
weight 3^{-j} → 3^{-(j+1)}). The present display carries no scale weight,
and 3^d ≤ 3^{d+1}: the transfer is spent strictly inside that
price. The sharp interior value is 3^{d/2} (no truncation, no
inscribed-cube slack); the extra 3^{d/2} is the honest cost of the
boundary-truncated windows, and is a C(d) spent once.
References #
- ABK26,
t.regularity.
1. Volumes of the two windows #
Translation invariance of Lebesgue measure, in the translation-image carrier the windows are written in.
|□_k| = (3^k)^d, as an ℝ≥0∞.
The truncated window is inside the untruncated cube, so its volume is at most
(3^k)^d.
The truncated window at a centre of □_m contains a translate of □_{k−1}, so
its volume is at least (3^{k−1})^d.
The volume ratio of the off-grid transfer. The scale-(n+1) lattice
window has at most 9^d times the volume of the arbitrary-centre scale-n
window it contains.
2. The ℝ≥0∞ transfer: no integrability hypothesis #
The normalized L² transfer, ℝ≥0∞-valued. For W' ⊆ W of positive
finite volume with |W| ≤ K²·|W'|,
‖f‖_{L²(⨍_{W'})} ≤ K · ‖f‖_{L²(⨍_W)} .
No MemLp, no IntegrableOn: the underlying monotonicity
eLpNorm_mono_measure holds in ℝ≥0∞ unconditionally.
The off-grid transfer of the energy-density left-hand side, in the
frozen root's own carrier and at the honest constant 3^d:
‖f‖_{L²(⨍_{(x+□_n) ∩ □_m})} ≤ 3^d · ‖f‖_{L²(⨍_{(z+□_{n+1}) ∩ □_m})} ,
z = offGridCentre n x the toward-origin lattice point of
StepNineOffGridGeometry.
The frozen root's left-hand side, transferred. The √ν-weighted
energy-density norm of e.energy.density.estimate at an A centre x ∈ □_m and
scale n, bounded by 3^d times the same object at the lattice centre z and
scale n+1 — the exact display the §4.4 chain produces.