ForceTransport #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The A4 transport of the fractional (Gagliardo) force seminorm #
The frozen §4.3 anchor writes its force leg as
[g]_{H^s(W)} = normalizedGagliardoESeminormOn W s g ,
W = ((z + □_{n+2}) ∩ □_m) ,
while every proved §4.3 estimate lives in the translated frame at the
origin cube □_{n+2}. The anchor's z is an arbitrary real point of
□_m, so that lemma does not apply.
This module proves the real-translation statement directly. The route is the
one the lattice proof uses, carried out on an arbitrary set: the map x ↦ x + z is measure preserving for the restricted Lebesgue measure between A and
z + A (CoarseGraining's measurePreserving_addRight_restrict_translateSet),
and volume (z + A) = volume A, so it is measure preserving for both slots
of normalizedGagliardoMeasureOn — the volume-normalized first slot and the
plain restricted second slot. The Gagliardo kernel is translation covariant
because dist (x + z) (y + z) = dist x y, so the two eLpNorms agree. No
constant and no side condition appear: the identity is exact, and holds for an
arbitrary (possibly non-measurable) f, because it is proved through the
lintegral form of eLpNorm and a measurable equivalence.
Main results #
normalizedGagliardoMeasureOn_translateSet,measurePreserving_prodMap_addRight_normalizedGagliardoMeasureOn— the two-slot change of variables.normalizedGagliardo /normalizedGagliardo — the real-translation covariance[f]_{H^s(z+A)} = [f(· + z)]_{H^s(A)}.- `normalizedGagliardo — evenness.
eLpNorm_normalizedVolumeMeasureOn_translateSet— the same change of variables in the one-slot (L^p) measure, used by theL²carrier bridge.normalizedGagliardo — on the *open* realization of a triadic cube the anchor's object is CoarseGraining'scubeGagliardoESeminorm`.
References #
- ABK26,
l.harmonic.approximation.good.scales, (the force leg[g]_{H^s}on the window(z+□_{n+2}) ∩ □_m); (the definition of[·]_{W^{s,p}}).
1. eLpNorm under a measure-preserving measurable equivalence #
2. The one-slot change of variables #
The volume-normalized measure of a translate is the pushforward of the volume-normalized measure.
The L^p norm over a translate. Exact, with no measurability side
condition.
The same in the frozen statement's (fun y => z + y) '' A spelling.
3. The two-slot change of variables #
The Gagliardo product measure of a translate is the pushforward under the pair translation. Both slots move: the normalized first slot because the normalizing volume is translation invariant, the plain second slot because restricted Lebesgue measure is.
The pair translation is measure preserving for the Gagliardo product measure.
4. The real-translation covariance of the fractional seminorm #
[f]_{H^s(z+A)} = [f(· + z)]_{H^s(A)} for an arbitrary real
translation vector z and an arbitrary set A.
This is the statement CoarseGraining does not have: its cubeGagliardoESeminorm lattice
translation only moves a cube by an integer multiple of its scale factor. The identity is
exact — no constant, no s-restriction, no regularity of f.
The same in the frozen statement's (fun y => z + y) '' A spelling: the
anchor's force leg, read at the origin cube.
5. Evenness #
The fractional seminorm is even: the kernel only sees f x - f y.
6. The force datum transports #
The L² half of the force datum transports. g ∈ L^p(z+A) in the
anchor's normalized measure is g(· + z) ∈ L^p(A).
The fractional half of the force datum transports. The Gagliardo kernel
of g is L² for the anchor's window measure exactly when the kernel of the
transported force is L² at the origin frame.
7. The open cube #
On the open realization of a triadic cube the volume-normalized measure is
CoarseGraining's normalizedCubeMeasure (the boundary is Lebesgue null).
The Gagliardo product measure on the open cube is CoarseGraining's.
The anchor's fractional seminorm on an open cube is CoarseGraining's cube
seminorm. The bridge into the whole cubeGagliardo* A.
The anchor's force leg, transported. The [g]_{H^s} slot of the frozen
statement, on the bare translated parent window, equals CoarseGraining's cube
seminorm of the transported force at the origin cube.