HomSpineEnergyDensity #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The per-cube energy density at EVERY depth, from Theorem C #
What this file supplies #
The §4.5 supplier's energy slot (hS0, hS, hSbound) needs the printed
per-cube energy ‖σ^{1/2}∇u‖_{L²(R)} — this repository's printedLocalEnergy
at the cutoff coefficient field — bounded at EVERY depth j ≤ m below □_m.
Theorem C (anomalous_regularity) gives the display only on the deep range
X_m(α) ≤ m - n's "Hence, for every j ≤ m" silently extends it. This file
supplies both halves of that extension at the printed carriers:
ofReal_printedLocalEnergy_coefficientCutoff— the carrier identity. The printed per-cell energy of the cutoff field IS Theorem C's own left-hand side on the cube's own window:symmPart(a_L) = ν Id(Cutoff.symmPart_coefficientCutoff) turnsCoarseGraining'slocalSymmetricEnergyENorminto√ν · ‖∇u‖_{L²(R)}with no ellipticity ratio and no conversion. This is an identity, not an estimate.printedLocalEnergy_le_of_deep— the deep range, by ONE application of the display at the descendant's own lattice centre (latticeTranslate_of_mem_descendantsAtDepth).printedLocalEnergy_le_of_shallow— the sub-cube average step, i.e. the shallow half at the energy carrier: a shallow cube's normalized energy is the volume-weighted average of its depth-Xdescendants' energies (cubeAverage_le_of_descendants,CoarseGraining's exact partition identity), hence at most their maximum. This is where the printed3^{(1-α)X_m(α)}factor is created.printedLocalEnergy_le_of_display— the two halves joined: ONE bound at every depth, at the majorantC · 3^{(1-α)X} · 3^{(1-α)j}.
The display, sliced #
RegularityEnergyDisplay is the root's FIRST conjunct with its three-term
bracket abstracted as one [0,∞] value T. Nothing is added: the binder
shape, the window ((x+□_n) ∩ □_m), the measure, the integrand and the factor
C·3^{(1-α)(m-n)} are byte-for-byte the statement's. The deep gate is written
(X: ℤ) ≤ m - n — at n ≤ m this is the X ω ≤ (m-n).toNat with a finite cut
of the ℕ∞-valued minimal scale.
1. The carrier identity #
The normalized volume measure of the OPEN cube is CoarseGraining's normalized cube
measure: the two realizations of a triadic cube differ by a null set.
The ν-drop, pointwise. The symmetric part of the cutoff coefficient
field is ν Id (Cutoff.symmPart_coefficientCutoff), so the printed energy
density is literally ν |∇u|². An identity: no ellipticity ratio is spent.
The p = 2 eLpNorm of |∇u| against a measure, as a lower integral.
The Euclidean magnitude of an H¹ gradient is a.e. strongly measurable for the
normalized volume measure of any subwindow of the domain.
THE CARRIER IDENTITY.
The printed per-cell energy of the cutoff field on a subcube R of □_m is
exactly Theorem C's left-hand side read on R's own window:
‖σ^{1/2}∇u‖_{L²(R)} = √ν · ‖∇u‖_{L²(R)}.
Both sides are ENNReal.ofReal-cut of the same finite quantity; the only step
is the pointwise ν-drop, which is an identity.
2. The display, sliced at one sample #
Theorem C's energy-density display, sliced.
The FIRST conjunct of anomalous_regularity at one ω, one L and one
solution, with the printed three-term bracket abstracted as a single [0,∞]
value T. The window, the measure, the integrand, the factor and the deep
gate are the statement's own; nothing is added.
Creg is the constant C, alpha the α, and X a finite cut of the
minimal scale X_m(α)(ω).
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The deep range #
The deep range, by one application of the display at the descendant's
own lattice centre. latticeTranslate_of_mem_descendantsAtDepth identifies the
descendant with the printed translate z + □_{m-j}, and the intersection with
□_m is the descendant itself.
4. The shallow range: the sub-cube average step #
THE SUB-CUBE AVERAGE STEP (at the energy carrier).
A shallow cube's normalized energy is the volume-weighted average of its
depth-X descendants' energies — CoarseGraining's exact triadic partition
identity, routed through cubeAverage_le_of_descendants — hence at most their
maximum, each of which the deep display bounds. No volume factor
3^{(d/2)(m-j)} is paid; the printed 3^{(1-α)X_m(α)} is created exactly
here.
5. The two halves joined #
THE DISPLAY AT EVERY DEPTH ("Hence, for every
j ≤ m").
At every depth j below □_m — deep or shallow — the printed per-cube energy
obeys the same bound with the single extra factor 3^{(1-α)X}, which is ≥ 1
and is the manuscript's own minimal-scale factor.