InteriorGlueWindow #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Clause (iv) restricted to a sub-window #
The anchor states its clause-(iv) force data on the whole cube □_m:
g ∈ L²(⨍_{□_m}) and [g]_{H^s(□_m)} < ∞, in the volume-normalized and
Gagliardo-normalized carriers. Every proved coarse-graining estimate is read
on a sub-window (the child x + □_n, or the parent z + □_{n+2}). This
module supplies the restriction, unconditionally:
B ⊆ A , 0 < |A| < ∞ , 0 < |B| ⟹ L²(⨍_A) ⊆ L²(⨍_B) ,
H^s(A) ⊆ H^s(B) .
Both are the same two-line measure argument: the normalized measures differ from
the restricted Lebesgue measures by finite nonzero scalars, and restricted
Lebesgue measure is monotone in the set. The Gagliardo case is the product
restriction (⨍_B ⊗ vol|_B) = |B|^{-1} · (vol ⊗ vol)|_{B×B}, whose set
monotonicity is again Measure.restrict_mono.
No estimate is claimed and no constant appears: these are membership transports.
References #
- ABK26,
l.harmonic.approximation.good.scales, (clause (iv)).
1. Volume facts for the anchor's windows #
The open realization of a triadic cube has finite volume.
The open realization of a triadic cube has positive volume.
Translates of an open cube keep its volume.
2. The volume-normalized restriction #
L²(⨍_A) ⊆ L²(⨍_B) for B ⊆ A. Exact: no constant, no measurability
side condition.
3. The Gagliardo restriction #
The Gagliardo measure of a window, as a scalar multiple of a restricted product measure.
H^s(A) ⊆ H^s(B) for B ⊆ A, at the level of the Gagliardo kernel's
L² membership.
4. Clause (iv) at the anchor's child window #
The anchor's clause-(iv) L² datum, read at a translated sub-cube.
The anchor's clause-(iv) Gagliardo datum, read at a translated sub-cube.