OneStepBoundaryHonest #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary one-step contraction at the manuscript competitor v − ℓ_h − v₁ #
The proved boundary endpoint
at the met set
asks the met-face oddness and the classical harmonicity of the harmonic
replacement v itself; but v = h on the met portion of ∂□_m, so that
clause forces v to vanish there
(Regularity.StepFourBoundaryJoin.oddCompetitor_eq_zero_on_metUpperFace): the
proved branch is the [∇h] = 0 specialization, and indeed it calls the
one-step at K_h := 0.
Here the odd-class binders are asked of the manuscript's shifted competitor
V_odd = v − ℓ_h − v₁
— the object whose zero trace on the met faces the chain actually produces
(the split datum's localized zero trace) — while the
L² comparison binder stays on u − v, the anchor's own object. The datum
enters through the already existing K_h slot of
OneStepConditional.excessDecay_oneStep_of_harmonicApprox, at the printed
K_h ≍ [∇h]_{C^{0,1/2}(U_2)}.
What is not claimed #
No boundary Schauder estimate for ∇v itself is proved or assumed: the
C^{1,1/2} data lives on V_odd, and v₁ is never differentiated. This is
the honest reading ("subtract a controlled extension first"); the printed
sentence [∇v]_{C^{0,1/2}(U_3)} ≤^{-n/2}E(v,U_2) + C[∇h] is reproduced at the
level of the excess conclusion, not re-derived as a gradient-seminorm
statement.
1. The excess is invariant under subtracting an affine function #
Affine functions add.
The competitor set is unchanged by an affine shift. Subtracting a fixed affine function permutes the affine competitors, so it moves no distance.
The raw excess is invariant under an affine shift.
The excess is invariant under an affine shift.
The affine shift is excess-free. E(u − ℓ_h, W) = E(u, W): the
manuscript's datum subtraction costs no constant at all.
2. The L² price of an almost-everywhere bounded corrector #
L^∞ → L² at an almost-everywhere bound. The corrector's bound is
delivered a.e. by OneStepDatumSplit.exists_datumCorrector, so the pointwise
version of this step is not available.
3. The datum leg's constant, and the exact propagation identity #
The constant of the boundary datum leg:
triangleRemainderConst d C k · 3^{-5} · (3^k)^{1/2}.
Equations
- Algsuperdiff.Section4.Provider.ExcessDecay.boundaryDatumLegConst d Csch k = Algsuperdiff.Section4.Provider.ExcessDecay.triangleRemainderConst d Csch k * (1 / 243) * (3 ^ ↑k) ^ (1 / 2)
Instances For
The propagation is exact. The corrector's L² price, carried at the
remainder weight triangleRemainderConst d C k · 3^{-n}, is the printed
K_h-leg C_t · (3^{n-k})^{1/2} · K_h' at K_h' = boundaryDatumLegConst d C k · K_h. No inequality, no slack.
3b. The join's folding device, with the datum leg carried #
The datum leg's constant is nondecreasing in the Schauder constant.
The one-step conclusion's constant monotonicity with the printed datum
leg carried. The join raises both branches to max (schauderWindowConst d) C_b;
this is the three-leg version of that move, so the boundary branch's datum leg
travels with it.
4. The deterministic core #
The one-step contraction at the manuscript competitor, deterministic form.
The C^{1,1/2} data is asked of V_odd = v − ℓ_h − v₁ on U_3, the L²
comparison of u − v on U_2, and the corrector only through its L^∞ bound.
The K_h leg comes out in the printed shape. No probability, no good event.
5. The re-cut boundary one-step #
The re-cut boundary one-step contraction at the manuscript
competitor V_odd = v − ℓ_h − v₁, with the printed K_h leg.
The sibling of the proved boundary endpoint at the met set
in which the odd-class binders _hupv/_hlowv/_hharmclass are asked of the
shifted competitor — the object the chain's zero-trace supplier actually
produces — while _hharm stays on u − v. The conclusion is
OneStepConditional.excessDecay_oneStep_of_harmonicApprox's display at
K_h := boundaryDatumLegConst d C k * K_h, where K_h is the corrector's own
L^∞ scale, i.e. the printed [∇h]_{C^{0,1/2}(U_2)}.