RootAssemblyChain #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
t.regularity root assembly, part two: the carrier bridge and the bracket #
The gap this module closes #
The frozen root, by contrast, states e.energy.density.estimate in ℝ≥0∞:
ENNReal.ofReal (√ν) * eLpNorm (fun y => √(vecNormSq (u.grad y))) 2
(normalizedVolumeMeasureOn ((x+□_n) ∩ □_m))
≤ ENNReal.ofReal (C·3^{(1-α)(m-n)}) *
(ENNReal.ofReal (√ν) * eLpNorm … (normalizedVolumeMeasureOn □_m)
+ ENNReal.ofReal (√σ_m⁻¹·3^{m/2}·K_g)
+ ENNReal.ofReal (√σ_m·3^{m/2}·K_h)) .
Two things separate the two ends, and N is an estimate:
The carrier.
Support.normalizedL2On W fis thetoRealofeLpNorm f 2 (normalizedVolumeMeasureOn W)(the proved dictionarySupport.normalizedL2On_eq_toReal_eLpNorm_normalizedVolumeMeasureOn), so a real inequality lifts to theℝ≥0∞one exactly when theeLpNormis finite. §1 proves the finiteness from theH¹datum the root's own binders carry and §2 performs the lift into the root's three-leg and two-leg bracket shapes.The bracket. The chain's output carries two powers of three (
3^{(1-α)(m-n)}on the oscillation half and3^{(3/4)(1-α)(m-n)}on the data half) and its own data scalarsdataG,dataM; the root prints ONE power and the two seminorm legs√σ_m⁻¹·3^{m/2}K_g,√σ_m·3^{m/2}K_h. §3 collapses the former into the latter. The collapse is pure arithmetic:3^{3E/4} ≤ 3^EatE ≥ 0and two DOMINATION hypotheses (dataGanddataMareK_g-legs), each of which is a proved conversion, not a new estimate.
§4 composes §2 and §3 with energyDensityEstimate_offGrid_pair and produces
the frozen root's two-clause conclusion at an arbitrary centre x ∈ □_m.
References #
- ABK26,
t.regularity, (e.energy.density.estimate), 12203. Algsuperdiff/Section4/Support/NormalizedL2.lean(the dictionary).
1. Finiteness of the normalized L² norm #
The normalized-measure eLpNorm in terms of the restricted one.
The normalized L² norm is finite on a window of nonzero volume carrying
an L² datum.
The bridge. On a window of nonzero finite volume carrying an L² datum,
the frozen root's ℝ≥0∞ quantity is the ENNReal.ofReal of the proved chain's real
quantity.
2. The lift of a real display into the root's bracket #
The three-leg lift. A real e.energy.density.estimate display becomes the
frozen root's ℝ≥0∞ display, with the bracket in the root's own shape (the
√ν-weighted □_m leg plus two ENNReal.ofReal data legs).
The two-leg lift — the frozen root's boundary-leg-free clause.
3. The bracket collapse #
4. Volume data of the two windows #
The volume of □_m is nonzero.
The volume of □_m is finite.
The lattice window of the off-grid transfer has nonzero volume.
The lattice window of the off-grid transfer has finite volume.
The L² datum on □_m restricts to any truncated window.
4b. The L² datum of the displayed function #
The displayed function is L². The frozen root's left-hand side is the
L² norm of |∇u|, and its L² membership is a of the root's own u: H1Function □_m — not an extra hypothesis.
5. The frozen root's two-clause conclusion at an arbitrary centre #
The root assembly's ℝ-to-root step.
From the §4.4 chain's real display at the lattice centre z = offGridCentre n x
and scale n+1 — in both the general and the boundary-leg-free form — this
produces the frozen root's two-clause conclusion at an arbitrary centre
x ∈ □_m and scale n, at the constant 3^d·C (the off-grid transfer factor
and nothing else).
The only data beyond the root's own binders is hfM, the L² membership of
the displayed function on □_m — a field of the root's u : H1Function □_m,
not a new hypothesis.