HomSpineCzGridDepthTest #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The SINGLE-DEPTH dual test: the exact pairing and the FREE flat part #
What this file is for #
HomSpineCzGridDualTest builds the MULTI-depth aggregate G₀ = Σ_{j≤N} g_j
and proves its pairing exact. The multi-depth flat part then costs a
Hölder-in-depth factor (1-3^{-s·p})^{-1/p}, which the necessity record of
HomSpineCzGridGaugeRefuted shows SHARP. This file does the SINGLE depth,
where that factor is not merely avoidable but absent by an exact computation:
⟨F, g_j⟩ = cubeEuclideanNegativeBesovDepthEnergy Q s p F j (EXACT)
3^{-s·m}‖g_j‖_{L^{p'}} = 3^{-s·j} · (depth energy)^{1/p'} (EXACT)
so the flat half of the single-depth full norm is bounded by (depth energy)^{1/p'}
at CONSTANT ONE, with room 3^{-s·j} to spare — no geometric factor, no band, no
s₀. Both displays are proved below (§1, §3).
The residue, measured exactly — and a WARNING #
What is NOT free at a single depth is the Gagliardo half. §4 records the exact
band arithmetic. Writing ℓ = 3^{m-j} for the depth-j cell side and banding the
double integral at |x-y| ~ 3^{m-k}:
- the NEAR bands
k ≥ j(distances below the cell side) are geometric at ratio3^{-(1-s·p')} ≤ 3^{-1/2}on the bands·p' ≤ 1/2, and sum to the uniformnearBandGeometricConstant— this half ISγ-uniform, as this file expected; - the FAR bands
k < j(distances above the cell side, up todiam Q) are NOT. A depth-jpiecewise constant straddles at EVERY coarser scale, so the far bands contribute the truncated geometric sumΣ_{i<j} 3^{-i·s·p'}, which is≥ j/3as soon asj·s·p' ≤ 1, and≈ min(j·log 3, (s·p')^{-1})in general.
So the single-depth Gagliardo bound carries a factor
(1 + min(j·log 3 + c_d, (s·p')^{-1}))^{1/p'}, NOT C(d,p). The factor is real,
not an artefact of the estimate: the alternating field ((F)_R = ±e_1 on the
depth-j cells) makes |g_j(x) - g_j(y)| of full size for a fixed fraction of the
far pairs. At the Step-3 pin s ≈ |log γ|⁻¹ this is |log γ|^{1/p'} — WORSE than
the banded lane's |log γ|^{1/p} (p' ≈ 1, p = 4d).
What this file proves #
ofReal_cubeAverage_vecDot_gridDualDepthTest_eq— the single-depth pairing, EXACT;weight_mul_flat_rpow_le_depthEnergy— the flat half at constant one,γ-uniform;sum_near_band_le— the near-band arithmetic of the Gagliardo half, uniform ins,jandd;fullENorm_gridDualDepthTest_le_of_gagliardo— the full norm of the slice from ANY Gagliardo input[g_j]^{p'} ≤ Cg^{p'}·(depth energy);depthEnergy_rpow_le_smoothDual_of_gagliardo— THE ENDPOINT: the depth-jgauge inequality atCA = (1+Cg^{p'})^{1/p'}, with NO normalization step (the common factor is cancelled, so the positive homogeneity ofcubeEuclideanWspFullENorm— proved upstream but PRIVATE — is never needed).
1. The pairing at ONE depth #
The depth-j slice of HomSpineCzGridDualTest's grid dual test pairs with F
against exactly the depth-j term of CoarseGraining's running-scale negative
Besov seminorm. No sum over depths is taken, so no Hölder in the depth index
is spent and no geometric factor appears.
The real-valued single-depth pairing: the cube average of ⟨F, g_j⟩ is
3^{s·p·(m-j)} times the depth-j descendant average of ‖(F)_R‖^p.
The single-depth pairing is nonnegative: it is a geometric weight times a
descendant average of p-th powers.
THE SINGLE-DEPTH EXACT PAIRING.
⟨F, g_j⟩ = cubeEuclideanNegativeBesovDepthEnergy Q s p F j
on the nose — the depth-j gauge term, with no constant spent, no √d, and no
inequality. This is the whole of HomSpineCzGridDualTest's exact-duality
mechanism read at ONE depth: the depth-j cells partition Q, the slice is
constant on each, and vecSupDual realizes the sup-norm duality exactly.
2. The flat part at ONE depth: the cell-measure bookkeeping #
One depth, one geometric weight, no Hölder in the depth index. The depth-j
cells carry normalized measure |D_j|⁻¹ each, so the normalized L^{p'} norm of
the slice is the ℓ^{p'} average of the cell values, and the identity
(p-1)·p' = p turns it into the depth energy to the power 1/p'.
Each depth-j cell carries normalized measure |D_j|⁻¹.
The r-th power of the pointwise Euclidean size of a depth slice, as a sum of
indicators of the depth-j cells.
The normalized L^r mass of a depth slice is the ℓ^r average of its cell
values: one depth, |D_j| cells of equal normalized measure.
The flat (normalized L^{p'}) norm of a depth slice, computed.
The Euclidean size of a dual-test coefficient: the vecSupDual factor is a
Euclidean unit vector, so no constant is spent.
3. The flat half of the single-depth full norm, at CONSTANT ONE #
The identity behind the display is (p-1)·p' = p together with p·p' = p + p':
the depth-j slice has normalized L^{p'} mass 3^{s·p·(m-j)}·A_j^{1/p'} with
A_j the descendant average of ‖(F)_R‖^p, and the scale weight 3^{-s·m·p'}
turns the product into 3^{-s·j·p'} times the depth energy 3^{s·p·(m-j)}·A_j.
The spare factor 3^{-s·j·p'} ≤ 1 is thrown away below.
The Hölder conjugacy of a finite exponent, read in the reals.
The scale weight of the full norm, in ENNReal.ofReal form.
The normalized finite-cell mass shared by the flat and cell-weighted grid estimates.
THE SINGLE-DEPTH FLAT HALF IS FREE.
3^{-s·m·p'} · ‖g_j‖_{L^{p'}(Q)}^{p'} ≤ cubeEuclideanNegativeBesovDepthEnergy Q s p F j
at constant ONE, uniformly in s, j, Q, F — no band, no s₀, no
(1-3^{-s·p})^{-1/p}. (The true value of the left side is 3^{-s·j·p'} times the
right side; the spare factor is discarded.) This is the display the multi-depth
aggregate cannot have: there the same computation is followed by a Minkowski sum
and a discrete Hölder over the depths, and THAT is what buys the geometric
factor the necessity record of HomSpineCzGridGaugeRefuted shows sharp.
4. The band arithmetic of the Gagliardo half: near bands uniform, far bands NOT #
A depth-j piecewise constant differs only across the depth-j skeleton, so the
Gagliardo double integral splits at the cell side ℓ = 3^{m-j}.
- NEAR bands (
|x-y| ~ 3^{m-k},k ≥ j): the straddling-pair measure is3^{j-k}-small and the kernel contributes3^{(k-j)·s·p'}, so bandkis3^{-(k-j)(1-s·p')}relative to the flat mass — geometric at ratio≤ 3^{-1/2}on the bands·p' ≤ 1/2.sum_near_band_lebounds the whole near half bynearBandGeometricConstant, uniformly ins,jandd. - FAR bands (
k < j, up todiam Q): every pair straddles, and bandkis3^{-(j-k)·s·p'}relative to the flat mass. The sum over the far bands is the truncated geometric seriesΣ_{i<j} 3^{-i·s·p'}, which is≥ j/3wheneverj·s·p' ≤ 1and is UNBOUNDED over the admissible parameter range. This is this file's central negative finding: the single-depth Gagliardo half is NOTγ-uniform.
The near-band geometric constant (1-3^{-1/2})^{-1}: the whole k ≥ j half of
the banded boundary-layer estimate, at any admissible s·p' ≤ 1/2.
Equations
Instances For
The near half is uniform. On the band s·p' ≤ 1/2 the near bands sum at
ratio at most 3^{-1/2}, so the whole near half costs nearBandGeometricConstant
— no s, no j, no γ.
The single-depth full norm from a Gagliardo input. The flat half is free
(§3); so any Gagliardo bound [g_j]^{p'} ≤ Cg^{p'}·(depth energy) gives the full
norm at (1+Cg^{p'})^{1/p'}·(depth energy)^{1/p'}.
THE SINGLE-DEPTH GAUGE INEQUALITY.
(depth energy)^{1/p} ≤ (1+Cg^{p'})^{1/p'} · ‖F‖_{W^{-s,p}(Q), smooth dual}
from the Gagliardo input alone: the exact pairing of §1, the free flat half of
§3, CoarseGraining's pairing bound, and a cancellation of the common factor
(depth energy)^{1/p'} — legitimate because the depth energy is an
ENNReal.ofReal, hence never ⊤. The hypothesis hGfield says only that G is a
W^{s,p'} ∩ L² carrier FOR THE SLICE ITSELF; no normalization is performed.