Boundary identity from radial stationarity #
This module turns one-dimensional cutoff, coarea, and integration-by-parts inputs into the weak boundary identity.
The theorems here are internal scaffolding for the proof route from radial
stationarity to the boundary identity. The recommended public entry point is
the final theorem in MainTheorem.lean.
Energy integration by parts plus integrability of the expanded terms gives the concrete one-dimensional IBP formula used downstream.
The packaged one-dimensional calculus input gives the concrete IBP formula used by the defect-to-distribution argument.
Direct distributional sharp-cutoff identity from weak stationarity, using only the primitive cutoffs constructed for the given one-dimensional test function. This avoids any global regularity assumption on all scalar cutoffs: the constructed primitive is constant near the origin, so its radial vector field is admissible.
Restricted-weight version of the direct distributional sharp-cutoff identity from weak stationarity and primitive cutoffs.
Boundary identity from weak stationarity through the primitive-cutoff
distributional route. The only one-dimensional analytic input is the packaged
radius energy calculus; no global hflat/hX hypothesis is needed.
Restricted-weight version of the boundary identity from weak stationarity through the primitive-cutoff distributional route.
A concrete integration-by-parts formula discharges the abstract one dimensional IBP step.
Once the defect pairs to zero against all primitive cutoff derivatives, the primitive family gives the full distributional sharp-cutoff identity.
Factored version of the one-dimensional sharp-cutoff-to-distribution step: first integrate by parts, then use primitive cutoffs for arbitrary test functions.
The distributional one-dimensional cutoff step, plus local integrability of the defect, gives the a.e. sharp-cutoff step.
The cutoff-limit step can be factored into coarea/radius differentiation followed by a one-dimensional sharp-cutoff approximation.
Step 1: compute the derivative and divergence of X(x) = phi(|x|) x.
In the full proof this should produce the integrand `((n - 2) * phi |x| + |x| * phi' |x|) * |du|^2
- 2 * |x| * phi' |x| * |partial_r u|^2`.
Step 2: stationarity implies the radial identity.
Step 3: approximate the sharp radial cutoff and pass to Lebesgue points.
Weak version of the cutoff-to-boundary step: the radial stationarity identity is first converted into the sharp-cutoff a.e. radius identity, then algebraically rewritten as the weak boundary identity.
The full weak radial-to-boundary route, with the two analytic ingredients kept separate: coarea/radius differentiation and one-dimensional sharp cutoffs.
Fully factored weak radial-to-boundary route: a concrete coarea/radius formula plus the one-dimensional distributional sharp-cutoff argument imply the weak boundary identity.
Even more granular weak radial-to-boundary route: after the coarea/radius formula, the one-dimensional sharp-cutoff part is split into integration by parts and primitive cutoff construction.
Version of the previous route using the concrete one-dimensional integration-by-parts formula.
The most decomposed route currently used by the formalization: vector-field regularity, coarea/radius integration, one-dimensional IBP, and primitive cutoffs are independent ingredients.
Same fully decomposed route, with radial vector-field regularity discharged from the natural flat-at-origin condition on scalar cutoffs.
Same route with the coarea ingredient supplied as the two standard radius integral formulas for energy and radial energy.
Boundary identity from the W^{1,2}_{loc}-friendly scalar-cutoff radial
stationarity interface and the split analytic ingredients.
Boundary identity from the scalar-cutoff radial stationarity interface and restricted-weight radius formulas.
Same scalar-cutoff route, but with the old one-dimensional IBP and primitive-family black boxes replaced by their concrete split ingredients.
Same scalar-cutoff route, with restricted-weight radius formulas and the one-dimensional IBP/primitive pieces in their concrete split form.
Same scalar-cutoff route, with the one-dimensional radius calculus bundled as a single input.
Same scalar-cutoff route, with restricted-weight radius formulas and the one-dimensional radius calculus bundled as a single input.
Boundary identity with both remaining one-dimensional pieces packaged: the energy calculus is an input, while primitive cutoffs are constructed from interval integrals and a smooth bump.
Boundary identity from scalar-cutoff stationarity and absolute continuity of the two radius energy functions. The primitive cutoff is the constructed interval-integral/smooth-bump one.
Boundary identity with the primitive-cutoff realization constructed from the interval primitive and a smooth bump.