HarmonicApproximationProvider #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
l.harmonic.approximation.good.scales, the provider #
What is proved #
One public theorem, harmonic_approximation_provider, and it carries no
hypothesis beyond the anchor's own regime, funding line and geometry binders:
for every dimension d there is a constant C > 0 such that, almost surely in
the cutoff sample, every Dirichlet solution u on □_m with datum h and
force g, and every weakly ã-harmonic competitor v = u − w on the child
cube x + □_n (w ∈ H¹₀), satisfies two displays.
The general clause, at every centre
z, gated on the good event𝒢(n+3, z; s/8, C⁻¹ s⁴):1_𝒢 ‖u − v‖_{L²(x+□_n)} ≤ C s^{-4} 𝓔_{n+3} ( ‖u − (u)_{W'}‖_{L²(W')} + s^{-3/2} 3^n |(∇h)_W| ) + C s^{-7} σ_n^{-1} 3^{(1+s)n} [g]_{H^s(W')} + C s^{-6} 3^{(1+s)n} [∇h]_{H^s(W')} + C s^{-6} 𝓔_{n+3} 3^n |(∇h)_W| , W = (z + □_{n+2}) ∩ □_m , W' = (z + □_{n+3}) ∩ □_m .The interior clause, triggered by the frontier-empty gate
(z + □_{n+2}) ∩ ∂□_m = ∅and gated at the literal1/2event𝒢(n+2, z; s/8, 1/2), with its ownn+2windows and its owns-powers.
Here 𝓔_{n+3} = fluxCorrectedErrorRepresentative M L (n+3) ⟨s/8⟩ (τ_z ω) is the
coarse-graining error factor read at the clause's own flux slot, and σ_n is
the annealed comparator at the child scale.
The flux-corrected error factor on the flat leg #
The last leg is the manuscript's scale-weighted window average of ∇h, carried
multiplied by 𝓔. Bounding 𝓔 · 1_𝒢 by a constant multiple of the event's
own threshold is a monotone one-way step; the chain below declines it on that
row, so the leg vanishes with the flux-corrected error instead of being priced
against it. The row is re-proved rather than transferred, through
AssemblyComposedErrorWeighted and ResidueRouteOneErrorWeighted (the two
composition sites), ResiduePluginErrorWeighted and
StitchDisplayLegsErrorWeighted (the residue lane's second consumer),
AssemblyBoundaryClauseErrorWeighted and ProviderBoundaryErrorWeighted (the
repackaging), and RebaseGeneralClauseErrorWeighted, RebaseJoinErrorWeighted,
RebaseSealDistanceErrorWeighted (statement-only re-typings, the leg being pure
nonnegative slack on the frontier-empty branch).
The last step, and what it costs #
exists_harmonicApproximation_provider_of_boundaryClauseReal_errorWeighted
delivers the display with that leg still in normalized-L² form. The mean-zero
fractional Poincaré inequality on the n+3 window (GradHSplit) turns it into
the printed average leg plus a multiple of the display's own Gagliardo ∇h leg,
‖∇h‖_{L²(W')} ≤ ‖(∇h)_W‖ + C(d)·3^{ns}·[∇h]_{H^s(W')} ,
and 3^n · 3^{ns} = 3^{(1+s)n} is exactly that leg's weight, so no s-power
is consumed. The remainder carries 𝓔, which is shed under the good-event
indicator by the proved caps step
ReindexSlot.ae_errorRepresentative_le_harmonicSlot_addThree (𝓔 ≤ C_𝓔/2
there). The whole price is the constant re-choice
C := max ((1 + κ(d)·C_𝓔/2)·C₀) (max 2 C_𝓔), a function of d alone.
References #
- ABK26,
l.harmonic.approximation.good.scales; the coarse-graining energy slot and the flat∇hleg.
l.harmonic.approximation.good.scales, the provider — unconditional.
The harmonic-approximation display on good scales, with the general clause's
flat leg carried as the manuscript's own scale-weighted window average of ∇h
at the n+2 window, multiplied by the clause's own coarse-graining error factor
𝓔. Proved by running the boundary chain with the monotone error discard
declined on that one row (ProviderBoundaryErrorWeighted,
RebaseSealDistanceErrorWeighted) and then applying the fractional Poincaré
split of GradHSplit.