RecutAtoms #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The window move: the three atoms of the re-cut #
In the frozen statement's general clause five window carriers — the
mean-subtracted L² leg's average window and its measure carrier, both
Gagliardo carriers, and the ∇h L² carrier — are read on the enlarged
window:
W = (z + □_{n+2}) ∩ □_m is enlarged to W' = (z + □_{n+3}) ∩ □_m;
the in-bracket 3^n |(∇h)_W| companion deliberately keeps W.
Since W ⊆ W', every one of those legs grows the window and therefore has to
be paid for at the volume ratio. This module proves the three atoms:
eLpNorm_le_of_volume_le— theL²carrier move on nested windows;eLpNorm_sub_volumeAverage_le_two_mul— the mean move: on a normalized window the mean-subtractedL²norm is within a factor2of the norm with any other constant subtracted (the triangle form of mean optimality; the sharp constant1is not needed, and the factor is absorbed into the existentially quantifiedC);normalizedGagliardoESeminormOn_anchorWindow_leandeLpNorm_sub_volumeAverage_anchorWindow_le— the two atoms at the anchor's own windows, at the volume ratio81^d.
The volume ratio actually used #
The ratio can be priced at 6^d (from z ∈ □_m and n+2 ≤ m alone). The
cheaper route taken here uses the anchor's own geometry binder: the child
cube x + □_n sits inside W, so
|W'| ≤ |z + □_{n+3}| = 27^d |□_n| ≤ 81^d |x + □_n| ≤ 81^d |W| ,
whose square root 9^d is a perfect power and keeps the arithmetic trivial. The
frozen statement quantifies C existentially, so the constant is immaterial; the
sharper 6^d is available and unused.
References #
- ABK26,
l.harmonic.approximation.good.scales; the frozen block ofAlgsuperdiff/Frozen/Section4/HarmonicApproximation.lean.
1. The measure comparison on nested windows #
If B ⊆ A and |A| ≤ K |B| then the normalized measure of B is dominated
by K times that of A.
The L² carrier move. If B ⊆ A and |A| ≤ K |B| then the normalized
L² norm over B costs K^{1/2} against the one over A.
2. The normalized window as a probability space #
A window of positive finite volume carries a probability measure.
The Bochner integral against the normalized window measure is CoarseGraining's
volumeAverage.
MemLp transported from the restricted to the normalized window measure.
3. The mean move #
The mean move. On a normalized window, subtracting the window mean costs
at most a factor 2 against subtracting any other constant.
This is the triangle form of mean optimality: the sharp statement has the
factor 1, but the frozen theorem's constant is existentially quantified, so
the cheap form suffices.
The two moves composed. On nested windows of comparable volume, the
mean-subtracted normalized L² norm over the smaller window is controlled by the
one over the larger, at 2 K^{1/2}.
4. The atoms at the anchor's own windows #
The window move's constant: 9^d, the square root of the volume ratio
81^d.
Equations
Instances For
The inner window W sits inside the enlarged window W'.
The anchor's child cube sits inside the inner window W.
The volume of W' is at most 81^d times the volume of W.
The inner window W has positive volume.
Both windows have finite volume.
The Gagliardo window move. The Gagliardo seminorm on W is at
most 9^d times the one on W'.
The L² window move. The mean-subtracted normalized L² norm on W
is at most 2 · 9^d times the one on W'.