HomCGDischargeAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
the general coarse-graining proposition at finite p: PROVED, at the smooth-dual reading #
What is proved here #
The printed finite-p coarse-graining proposition,
3^{-ms} σ₀ ‖∇u - ∇v‖_{W_hat^{-s,p}(□_m)} + 3^{-ms} ‖𝐚∇u - σ₀∇v‖_{W_hat^{-s,p}(□_m)}
≤ C s^{-1} σ₀^{1/2} 𝓔_{s₁,∞,1}(□_m,n;𝐚,σ₀)
( Σ_{k ≤ n} 3^{-(s-s₁)p(n-k)} avsum_z ‖σ^{1/2}∇u‖_{L²(z+□_k)}^p )^{1/p}
+ C s^{-9/2} (s₂-s)^{-1} (1 + 𝓔²_{s₁/2,∞,2}(□_m,n;𝐚,σ₀))
3^{s₂ n} [𝐠]_{W^{s₂,p}(□_m)}
is a theorem (exists_printedCoarseGrainingFiniteP_smoothDual) when the
undefined left-hand symbol ‖·‖_{W_hat^{-s,p}(□_m)} is read as CoarseGraining's
smooth fractional dual cubeEuclideanNegativeWspSmoothDualENorm, under exactly
the printed hypotheses:
𝐚uniformly elliptic on□_m(CoarseGraining'sBook.Ch02.CoeffOn),σ₀ > 0;p ∈ [2,∞),s₁ < s < s₂fractional orders,n < m;𝐠 ∈ W^{s₂,p}(□_m)(MemCubeEuclideanFullWsp);-∇·𝐚∇u = ∇·𝐠and-∇·σ₀∇v = ∇·𝐠in□_m(IsForcedEquation,IsScalarForcedEquation) andu - v ∈ H¹₀(□_m)(HasH10Difference).
The right-hand side is CoarseGraining's localCoarseGrainingLpRHS, which is
the printed right-hand side symbol for symbol. The constant is C(p,d) < ∞,
fixed before the cube, the orders, the coefficient field, the forcing and the
solutions.
The three links, and where each comes from #
LHS ≤ C_cz · 3^{s(m-n)} · (smooth-dual descendant average) -- link 1
≤ C_cz · C_d · 3^{s(m-n)} · 3^{sn} · (neg-Besov average) -- link 2
≤ C_cz · C_d · C_lcg-RHS at 3^{sm} -- link 3
- link 1 is
CoarseGraining'sexists_centeredCubeFluxComparison_cz(the fractional Calderón--Zygmund duality argument), used as a black box; - link 2 is
localFluxDefect_smoothDualAverage_leofHomCGDischargeBridge, i.e. the smooth-dual/negative-Besov comparison aggregated over the descendant grid; - link 3 is
CoarseGraining'sexists_localCoarseGrainingLp, used as a black box.
Nothing else enters. The three 3-powers multiply to 1
(ofReal_three_rpow_scale_triple), which is the exact statement that the
printed 3^{-ms} prefactor is the correct normalization of this composition.
The hypothesis bridge (§1) #
CoarseGraining's flux-comparison statement takes the consequence of the
printed pair — the flux difference is weakly solenoidal against H¹₀ tests, in
the normalized cube measure — rather than the pair itself.
isCenteredCubeFluxBalanced_of_forced derives it from the printed pair, so no
hypothesis is smuggled: the two forced equations are subtracted, the common
forcing cancels, and the volume normalization is a nonzero scalar. Similarly
HasCenteredCubeH10Difference is HasH10Difference on the origin cube,
definitionally.
What this does NOT give (the honest scope) #
The transcribed finite-p coarse-graining hypothesis of HomFinitePSource
carries three clauses. This file's display is the duality content;
converting it to this repository's WeakNegDualBoundOn (clauses 2 and 3) needs a
test-class change, and the multiscale clause 1 is a different object
altogether. See HomCGDischargeTestClass for both measurements.
1. The printed hypothesis pair produces CoarseGraining's flux balance #
The L² membership of 𝐚∇u on a cube, for a bundled elliptic coefficient.
Adapted from the private memVectorL2_matVecMul_pointwiseCoeffOn of
Homogenization/Book/Ch03/ABK26/LocalCoarseGrainingDefinitions.lean, which is
not exported.
Left additivity of the Euclidean dot product under subtraction.
The centered-cube normalized volume is a positive multiple of the raw volume restricted to the open cube.
Adapted from the private
centeredCube_normalizedVolume_eq_smul_openCubeVolume of
Homogenization/Book/Ch03/ABK26/FluxComparisonBridges.lean.
The printed hypothesis pair gives CoarseGraining's flux balance.
-∇·𝐚∇u = ∇·𝐠 and -∇·σ₀∇v = ∇·𝐠 in □_m imply that 𝐚∇u - σ₀∇v is weakly
divergence free against H¹₀(□_m), which is the hypothesis CoarseGraining's
flux-comparison theorem actually consumes. No hypothesis is smuggled: the
common forcing cancels and the volume normalization is a nonzero scalar.
The printed zero-trace hypothesis on the origin cube IS CoarseGraining's
HasCenteredCubeH10Difference.
2. Scaling bookkeeping #
The printed right-hand side is homogeneous of degree one in its constant.
The three scale powers of the composition multiply to one.
3^{-sm} · 3^{s(m-n)} · 3^{sn} = 1: the printed 3^{-ms} prefactor is exactly
the normalization that the flux-comparison factor and the negative-Besov
normalization leave over.
3. The printed display, PROVED at the smooth-dual reading #
the general coarse-graining proposition at finite p, at the smooth-dual reading.
For every p ∈ [2,∞) and every dimension d ≥ 2 there is C(p,d) < ∞ such
that, for every n < m, every s₁ < s < s₂, every uniformly elliptic 𝐚 on
□_m, every σ₀ > 0, every 𝐠 ∈ W^{s₂,p}(□_m) and every pair u, v solving
the printed pair of equations with u - v ∈ H¹₀(□_m),
3^{-ms} ( σ₀ ‖∇u - ∇v‖_{W_hat^{-s,p}} + ‖𝐚∇u - σ₀∇v‖_{W_hat^{-s,p}} )
≤ (the printed right-hand side, at C).
This is the printed display, at the printed hypotheses, with the printed
right-hand side, and with ‖·‖_{W_hat^{-s,p}(□_m)} read as the smooth fractional
dual. Nothing in the proof is assumed: links 1 and 3 are CoarseGraining
theorems, link 2 is HomCGDischargeBridge.