OneStepEvenBoundOdd #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The odd/even split of a face-odd competitor, and its cost on the doubled window #
reduced the boundary branch's odd-class defect to the even-part bound
‖even part of ℓ*‖_{L²(U₂)} ≤ C(d) · affineExcessRaw U₂ V , (★)
for V harmonic on the doubled window and odd about the met face, and ℓ* an
affine minimizer of V on U₂. This module proves the algebraic half of
(★): the exact reflection identities the analytic half consumes, and the
resulting L² bound for the affine residual on the doubled window.
The three identities #
Write ρ for the reflection through the met face {yᵢ = a}, a = (1/2)·3^m,
and split ℓ* = o + e into its odd (normal) and even parts of
OneStepDatumPriceOdd. Then, pointwise and with no hypothesis beyond
V ∘ ρ = -V:
o ∘ ρ = -o , e ∘ ρ = e , (V - ℓ*) ∘ ρ + (V - ℓ*) = -2 e .
The third is the identity the near-face slab comparison of OneStepEvenBound
runs on; the first two are what make it exact. Note that e ∘ ρ = e is not an
accident of the window: the even part has vanishing i-slope
(evenAffineSlope_apply_self), so it is constant along the reflection.
The cost on the doubled window #
V - o is odd about the met face, so the proved odd bridge
(OneStepBoundaryOdd.normalizedL2On_oddExtend_le) prices it on the doubled
window by 2^d times its cost on U₂. Subtracting the even part back gives
‖V - ℓ*‖_{L²(R)} ≤ 2^d (‖V - ℓ*‖_{L²(U₂)} + ‖e‖_{L²(U₂)}) + ‖e‖_{L²(R)} ,
which is exactly the input the interior Hessian estimate on the doubled window
needs: the Hessian of V - ℓ* at a near-face point is controlled by the
affine-subtracted L² norm, not by ‖V‖.
1. The even part is constant along the reflection #
A slope with vanishing i-coordinate does not see the i-face
reflection.
An affine function with vanishing i-slope is invariant under the i-face
reflection.
2. The two halves of the affine minimizer, as functions #
The even part of the affine datum (c, A) at the met upper i-face, as
a function on Vec d.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The odd (normal) part of the affine datum (c, A) at the met upper
i-face, as a function on Vec d.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The odd part is the normal ramp Aᵢ (yᵢ - a).
The split, as an identity of functions.
The odd part is odd about the met face.
The even part is even about the met face.
3. The reflection identity for the affine residual #
The reflection identity. For a competitor odd about the met face, the
affine residual and its reflection add up to -2 times the even part — an
exact pointwise identity, with no membership hypothesis.
The odd summand. Subtracting the odd part of the affine minimizer from a face-odd competitor leaves a face-odd function.
4. The affine residual on the doubled window #
The odd bridge for the affine residual. For V odd about the met face,
the residual V - ℓ* on the doubled window is priced by its cost on U₂
together with the even part's cost on both windows.
This is the input the interior Hessian estimate consumes: it is the
affine-subtracted residual, so no unsubtracted ‖V‖ ever appears.