InteriorClause #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The interior clause's Caccioppoli input, in the frozen theorem's own carriers #
This module closes the interior Caccioppoli seam of §4.3.
⨍_{(x-z)+□_n} ∇u_tilde · ã_{L,n+2} ∇u_tilde
≤ C(d) ( σ_{n+2} 3^{-2(n+2)} ‖u - (u)_W‖²_{L²(W)}
+ s^{-11} σ_{n+2}^{-1} 3^{2s(n+2)} [g]²_{H^s(W)} ) ,
W = ((z+□_{n+2}) ∩ □_m) ,
almost surely on the anchor's good event 𝒢(n+2, z; s/8, 1/2), for every
H¹(□_m) solution u of the anchor's own Dirichlet problem whose forcing g
lies in H^s(W;ℝ^d), under the anchor's geometry binder and its interior
(frontier-empty) gate.
What each unit contributes #
- the force carrier:
ForceTransport.lean(the real-translation covariance of the Gagliardo seminorm and of the force datum) andBesovBridge.lean(Besov ≤ C(d)·3^{s(n+2)}·Gagliardo, and theForceBesovRegularitydischarge); - the
L²carrier:L2Bridge.lean(an exact identity, no constant);
Two disclosed frame facts (inputs to the consumer, not gaps in this estimate) #
- The left-hand side is stated in the translated frame — at the core
(x-z) + □_n, for the transported solutionu(· + z)and the flux-corrected family attranslateCutoffSample z ω, which is where every proved §4.3 cap lives. Reading the same quantity at the anchor's own corex + □_nis one application ofnormalizedSetAverage_translateSetaway once the flux-corrected family is rebuilt at the untranslated sample; that construction is not performed here.
The force binder, and where it differs from the frozen statement #
The frozen statement carries the equation but not the g- and
h-regularity clauses: it quantifies over an arbitrary g : Vec d → Vec d.
The estimate below carries the paper's own clause for g — in the anchor's own
window carriers — because l.coarse.grained.Caccioppoli has it as a premise.
(When the Gagliardo seminorm is ⊤ the frozen statement's interior clause is
trivially true, so only the finite-seminorm-but-not-H^s case is at issue.)
References #
- ABK26,
l.harmonic.approximation.good.scales;e.energy.bound.interior;l.coarse.grained.Caccioppoli.RHS.
1. The scale weight of the parent cube #
The Besov scale weight of an origin cube, as an explicit 3-power.
Its square, the weight the force leg carries.
2. The right-hand side in the anchor's carriers #
The interior Caccioppoli right-hand side, in the frozen theorem's own
carriers, on an arbitrary window W.
The mean-subtracted L² norm and the fractional force seminorm are the frozen
statement's own objects (eLpNorm … (normalizedVolumeMeasureOn W) and
normalizedGagliardo W s g); the 3- and s-powers are explicit. The
composed estimate below instantiates W at the anchor's own window
((z+□_{n+2}) ∩ □_m).
Equations
- One or more equations did not get rendered due to their size.
Instances For
3. The arithmetic stitch #
The right-hand-side conversion.
The L² leg is an identity; the force leg costs the Besov-versus-Gagliardo
constant.
5. The composed interior estimate #
The interior clause's Caccioppoli input.
Entered at the frozen theorem's own binders — its Dirichlet datum on □_m, its
geometry binder, its interior (frontier-empty) gate, its good event, its
hoisted smallness clauses and its s-range — and concluded in the anchor's own
right-hand-side carriers on the anchor's own window W = ((z+□_{n+2}) ∩ □_m):
⨍_{(x-z)+□_n} ∇u_tilde · ã_{L,n+2} ∇u_tilde · 1_𝒢
≤ Cout ( σ_{n+2} 3^{-2(n+2)} ‖u - (u)_W‖²_{L²(W)}
+ s^{-11} σ_{n+2}^{-1} 3^{2s(n+2)} [g]²_{H^s(W)} ) ,
where u_tilde = u(· + z) is the transported solution and ã_{L,n+2} the
flux-corrected field at the translated sample. The force hypothesis is the
manuscript's g ∈ H^s(W;ℝ^d) in the anchor's own carriers.