ReplacementDatumHarmonic #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The passage v_g → v: the interior L² estimate against the harmonic replacement #
What is proved #
ReplacementDatum.lean bounds σ 3^{-n} ‖u − v_g‖_{L²} against the
auxiliary forced replacement v_g. ABK26's display
e.homogenization.L2.interior is stated against the harmonic replacement
v, the two being reconciled by "the triangle inequality" applied to the
forcing correction. This module performs that passage:
σ 3^{-n} ‖u − v‖_{L²(Q)}
≤ σ 3^{-n} ‖u − v_g‖_{L²(Q)} (`ReplacementDatum`, datum discharged)
+ σ 3^{-n} ‖v_g − v‖_{L²(Q)} ,
and bounds the second summand by
σ 3^{-n} ‖v_g − v‖_{L²(Q)}
≤ 2 C_neg(d) [∇v_g − ∇v]_{B^{-s/2}(Q)} (negative norm to L²)
≤ 2 C_neg(d) K_s^{1/2} σ ‖∇v_g − ∇v‖_{L²(Q)} (negative ≤ L²)
≤ 2 C_neg(d) K_s^{1/2} sqrt d · 3^{s n} [g]_{B^s_{2,2}(Q)} (forcing correction)
where K_s = (1 − 3^{-s})^{-1}.
The s-envelope of the correction (reported, not hidden) #
K_s^{1/2} = (1 − 3^{-s})^{-1/2} behaves like (3/(2s))^{1/2} as s ↓ 0
(concavity of s ↦ 1 − 3^{-s} on [0,1] gives 1 − 3^{-s} ≥ 2s/3 there), so
the correction term's honest envelope is s^{-1/2}. It is not bounded by a
constant, and it is not simplified here: the closed form Real.sqrt ((geometricDiscount (s/2) 2)⁻¹) is carried verbatim in the statement.
The manuscript prints no separate correction term at all: its display
e.homogenization.L2.interior has the same shape before and after the
triangle step, because both corrections sit inside the same
C s^{-11/2} (1 + 𝓔) 3^{sn} [g] summand. The statement below therefore keeps
the two summands separate, which is strictly more informative.
References #
- ABK26,
l.harmonic.approximation.good.scales.
1. Scalar L² plumbing on the cube #
Scalar L² membership against the normalized cube measure.
Triangle inequality for the normalized scalar L² norm, subtractive form.
2. The harmonic corrector and the difference #
The chosen corrector of the harmonic replacement: u − v.
Equations
Instances For
The difference of the two correctors, ρ_g − ρ_0 = v − v_g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The difference solves the zero-trace problem with force −g.
This is the equation behind the forcing correction: subtracting the two
constant-coefficient problems removes the datum's own flux a₀∇u and leaves the
printed force.
3. The correction bound #
The s-dependent analytic factor of the correction: (1 − 3^{-s})^{-1/2},
carried in closed form. See the module docstring.
Equations
Instances For
The negative seminorm is dominated by the normalized Euclidean L²
norm, with the closed-form geometric factor.
The correction term of the triangle step.
σ 3^{-scale(Q)} ‖v_g − v‖_{L²(Q)}
≤ 2 C_neg(d) K_s^{1/2} sqrt d · 3^{s·scale(Q)} [g]_{B^s_{2,2}(Q)} .