ForcingCorrection #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The forcing correction: the two inequalities #
Nothing here imports that file, and nothing here claims the anchor or any source node.
The printed display #
σ_{n+2} ‖∇v − ∇v_g‖_{L²(x+□_n)}
≤ ‖g − (g)_{x+□_n}‖_{L²(x+□_n)}
≤ C 3^{sn} [g]_{H^s(x+□_n)} .
This module proves both.
First inequality: the energy comparison #
Stated here in the general form it actually has, for any zero-trace weak
solution of −∇·a∇w = ∇·G on the cube:
λ ‖∇w‖_{L²(Q)} ≤ ‖G − (G)_Q‖_{L²(Q)} .
The proof is the printed one: test the equation with w itself, subtract the
mean of G for free because ∫_Q ∇w = 0 for w ∈ H¹₀(Q), and use ellipticity
on the left — all three steps packaged in CoarseGraining's
IsZeroTraceDirichletRhsWeakSolution.energy_le_sub_const_rhs_pairing_of_isEllipticFieldOn
— and then absorb the right-hand pairing by the sharp pointwise Young
inequality |vecDot x y| ≤ λ⁻¹|x|²/2 + λ|y|²/2 (CoarseGraining's
abs_mul_mul_vecDot_le_add_halves_mul_sq_vecNormSq at the weights (λ^{-1/2}, λ^{1/2})), which returns the constant 1 exactly.
Applied to w = v_g − v and G = −g — the difference of the two replacements
of HarmonicReplacement.lean — and to the scalar background a₀ = σ Id, where
λ = σ, this is the printed first inequality with the printed constant 1.
Second inequality: the fractional Poincaré, at constant 1 #
cubeBesovPositiveVectorDepthSeminorm Q s g 0
= 3^{s·0} · sqrt(descendantsAverage Q 0 (R ↦ ‖g − (g)_R‖²_{L²(R)}))
= ‖g − (g)_Q‖_{L²(Q)} ,
and every depth term is bounded by the partial seminorm, which is bounded by
cubeBesovPositiveVectorSeminormTwo Q s g = 3^{s·scale} [g]_{B^s_{2,2}(Q)}.
No fractional-Poincaré constant is needed: C = 1.
Carriers, and the one dimensional constant (disclosed) #
The manuscript's ‖·‖_{L²} for a vector field is the normalized
Euclidean L² norm, normalizedEuclideanL2 below. CoarseGraining's
cubeLpNorm measures the ambient Vec d = Fin d → ℝ sup norm instead, so
passing from the Euclidean carrier (in which the energy comparison lives) to
the Besov carrier (in which the seminorm lives) costs the factor sqrt d, and
nothing else — Ch03.cubeAverage_vecNormSq_le_card_mul_cubeLpNorm_two_sq.
Consequently the composed statement forcingCorrection_le carries sqrt d
where the manuscript writes C(d); this is the only constant in the display,
and it is d-only, as printed.
References #
- ABK26,
l.harmonic.approximation.good.scales.
1. The normalized Euclidean L² carrier #
The manuscript's ‖F‖_{L²(Q)} for a vector field: the normalized L²
norm taken with the Euclidean norm on ℝ^d.
Equations
Instances For
Transport of vector L² membership between the two cube realizations.
Transport of vector L² membership between the two cube realizations.
The manuscript's clause (iv) already gives g ∈ L² on the window.
Hilbertified L² membership against the normalized cube measure.
The square of the normalized Euclidean L² norm is the Euclidean square
average.
Euclidean against sup: the only dimensional constant of this module.
2. The sharp weighted Young inequality #
The sharp weighted Young inequality on ℝ^d, at the elliptic weight.
3. The energy comparison #
The first inequality of the forcing correction, in its general form.
For a zero-trace weak solution of −∇·a∇w = ∇·G on the open cube Q,
λ ‖∇w‖_{L²(Q)} ≤ ‖G − (G)_Q‖_{L²(Q)} ,
with constant 1. The mean subtraction is free (∫_Q ∇w = 0).
4. The fractional Poincaré at constant 1 #
The depth-0 Besov term is the normalized oscillation.
The second inequality of the forcing correction, at constant 1.
‖g − (g)_Q‖_{L²(Q)} ≤ 3^{s·scale(Q)} [g]_{B^s_{2,2}(Q)} .
In the manuscript's normalization the right-hand side is written C 3^{sn} [g]_{H^s}; CoarseGraining's seminorm already carries the factor 3^{sn}, and
the constant is 1.
5. The composed display #
The fluctuation of −g is the negative of the fluctuation of g.
The forcing correction, composed.
For a zero-trace weak solution of −∇·a∇w = ∇·(−g) (the difference of the
forced and the harmonic replacement, w = v_g − v):
λ ‖∇w‖_{L²(Q)} ≤ ‖g − (g)_Q‖_{L²(Q)}
≤ sqrt d · 3^{s·scale(Q)} [g]_{B^s_{2,2}(Q)} .
The sqrt d is the Euclidean-vs-sup carrier conversion documented in the module
docstring; the manuscript writes C(d).