HomSpineCzGridDualTest #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The banded dual test G₀, and its pairing: EXACT ℓ^p–ℓ^{p'} duality #
The test #
HomSpineCzGridGaugeBanded.GridDualTestFamilyBanded asks, per cube Q (scale
m), order s, field F and truncation depth N, for ONE
W^{s,p'}(Q) ∩ L²(Q) field of full norm at most one whose normalized pairing
against F sees the truncated grid mass. The witness is the multi-depth
grid-piecewise-constant aggregate
G₀(x) = Σ_{j ≤ N} Σ_{R ∈ D_j} 3^{s·p·(m-j)} · ‖(F)_R‖^{p-1} · e_R · 1_R(x),
where (F)_R is the cell average of F on R and e_R is a Euclidean unit
vector dual to (F)_R for the SUP norm this development gauge is built on:
e_R = ±e_{i} at a coordinate i realizing ‖(F)_R‖ = |(F)_R i|
(vecSupDual). Such an e_R has Euclidean magnitude 1 and satisfies
⟨(F)_R, e_R⟩ = ‖(F)_R‖ exactly, which is what makes the duality below EXACT
rather than approximate.
What this file proves #
The single-depth pairing, EXACTLY:
⟨F, G₀⟩_{L²(Q)} = (truncated grid mass of F at depth ≤ N) (EXACT)
— the depth-≤ N truncated grid mass, on the nose. The mechanism is a pure
cell decomposition: at depth j the cells D_j partition Q exactly (the
half-open cubeSet realization), so the depth-j slice of G₀ is the
constant 3^{s·p·(m-j)}‖(F)_R‖^{p-1}e_R on each R, and
cubeAverage_eq_descendantsAverage_cubeAverage_of_integrableOn turns the cube
average of ⟨F, ·⟩ against it into the descendant average of
3^{s·p·(m-j)}‖(F)_R‖^{p-1}⟨(F)_R, e_R⟩ = 3^{s·p·(m-j)}‖(F)_R‖^{p}. Summing
over j ≤ N reproduces CoarseGraining's
cubeEuclideanNegativeBesovDepthEnergy term by term. No inequality is spent
anywhere; √d is NOT spent here (the sup-norm duality is exact, and
vecSupDual is a Euclidean unit vector).
What this file does NOT prove — the residual, stated exactly #
Two norm bounds on the SAME G₀ remain, both at s₀ ≤ s, s·p' ≤ 1/2, with
P the truncated grid mass above:
- the FLAT part
3^{-s·m}·‖G₀‖_{L^{p'}(Q)} ≤ (1-3^{-s·p})^{-1/p}·P^{1/p'}— Hölder in the depth index against the geometric weights, whose pure-algebra core is a geometric-series bound over the depth bands; the rate(1-3^{-s·p})^{-1/p}is the one the geometric sum forces and cannot be improved; - the GAGLIARDO part
[G₀]_{W^{s,p'}(Q)} ≤ C(d,p)·(1-3^{-s·p})^{-1/p}·P^{1/p'}— the band-first boundary-layer estimate: a depth-jpiecewise constant differs only across the depth-jskeleton; banding the double integral at|x-y| ~ 3^{-k}·3^m, the straddling-pair measure at bandk ≥ jis3^{j-k}-small, giving the factor3^{-(k-j)(1-s·p')} ≤ 3^{-(k-j)/2}ON THE BAND, and the depths inside each band are summed before the bands are (Minkowski in the band index).
Given both, G:= G₀/K with K = (1+C(d,p))·(1-3^{-s·p})^{-1/p}·P^{1/p'} has
full norm at most one and realizes GridDualTestFamilyBanded at
CA = (1+C(d,p))·(1-3^{-s₀·p})^{-1/p} (monotone in s₀ ≤ s). The L²(Q)
membership of G₀ is free: it is bounded and takes finitely many values.
1. Elementary bilinearity of vecDot #
2. The sup-norm dual unit vector #
This repository's gauge is built on ‖(F)_R‖, the SUP norm of the cell
average, while the admissible dual tests are measured in the EUCLIDEAN
magnitude. The two are compatible in the direction needed here at NO cost: a
signed coordinate unit vector has Euclidean magnitude 1 and realizes the sup
norm exactly.
Existence of the dual unit vector. Every a: Vec d admits u of
Euclidean magnitude at most one with ⟨a, u⟩ = ‖a‖ (the sup norm). For
d = 0 the statement is 0 = 0; otherwise u is a signed coordinate unit
vector at a coordinate realizing the maximum.
The sup-norm dual unit vector of a, chosen once and for all.
Instances For
The exactness of the sup-norm duality. No constant is spent passing from the sup-norm cell averages to a Euclidean unit dual test.
3. The grid-piecewise-constant test #
The depth-j slice of the dual test: the piecewise constant taking the
value v R on each cell R ∈ D_j and 0 off Q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Off Q the depth slice vanishes; on a cell it is that cell's value.
The pointwise pairing of a field with the depth slice, as an indicator sum.
The coefficient of the dual test at depth j and cell R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
4. Integrability of the components on the cube #
Each component of an L²(Q) field is integrable on Q for Lebesgue
measure. (normalizedCubeMeasure Q is a positive finite rescaling of
volume.restrict (cubeSet Q), and a probability measure carries L² ⊆ L¹.)
The pairing against a CONSTANT vector is integrable on the cube.
The cube average of the pairing against a constant vector is the pairing of the cell average against that vector.
descendantsAverage reads its argument only on the depth family.
5. The depth-slice pairing #
The depth-j cell decomposition of the pairing. The cube average of
⟨F, ·⟩ against the depth-j slice is the descendant average of the pairing
of the cell averages against the cell values.
6. THE EXACT DUALITY #
7. The ℝ≥0∞ form: the truncated grid mass, on the nose #
Each depth energy of CoarseGraining's running-scale negative Besov seminorm is the
ENNReal.ofReal of the corresponding real depth term of §6.
The Hilbert realization is additive on finite sums (it is the identity on the underlying pi type).
The normalized field pairing of CoarseGraining is the cube average of ⟨F, ·⟩: the
bridge from §6–§7 to GridDualTestFamilyBanded, once a W^{s,p'} ∩ L²
carrier for the test is available.