Euclidean weak monotonicity interfaces #
This module contains the strongest Euclidean and restricted-weight packaged weak monotonicity interfaces.
This file is still part of the internal proof route: it closes the Euclidean
coarea and thin-shell ingredients before MainTheorem.lean packages the final
user-facing statement.
Current strongest packaged weak-map monotonicity interface: primitive
cutoffs are constructed, thin radial-shell volume control supplies radius
absolute continuity, and the final boundary-to-monotonicity increment is proved
inside Lean rather than supplied as an external hderive input.
Restricted-weight version of the strongest packaged weak-map monotonicity interface through primitive cutoffs and thin radial-shell volume control.
Same packaged interface as
weakTheta_monotone_from_weakStationaryMapIn_via_radialShellsVolume_primitiveCutoffs_closed,
but the local integrability of the sharp-cutoff defect is discharged from the
radius absolute-continuity package obtained via thin radial-shell volume
control.
Restricted-weight version of
weakTheta_monotone_from_W12Loc_radialShellsVolume_closed.
Strong packaged weak-map monotonicity interface where the two map-specific radius integration formulas are discharged from one generic ball-integral coarea/radius-derivative theorem.
Restricted-weight version of the strong packaged weak-map monotonicity interface: the generic coarea theorem only needs to hold for measurable essentially bounded radius weights.
Strong packaged weak-map monotonicity interface where the thin-shell input is reduced to absolute continuity of the Euclidean ball-volume radius function.
Restricted-weight version where the thin-shell input is reduced to absolute continuity of the Euclidean ball-volume radius function.
Strong packaged weak-map monotonicity interface with the Euclidean thin-shell estimate discharged from the explicit ball-volume formula. The only remaining geometric analysis input is the ball-integral coarea/radius-derivative formula.
Restricted-weight Euclidean weak-map monotonicity interface. The remaining coarea input only has to be proved for measurable essentially bounded radius weights.
Euclidean weak-map monotonicity from the concrete finite-interval
approximation bridge for bounded measurable radius weights. This removes the
abstract coarea/radius-derivative hypothesis from the final interface; the only
remaining input for this route is a bounded interval-step approximation of each
radius weight on (0, R0), with an exceptional set whose radial pullback is
null on the ball.
Same Euclidean weak-map monotonicity interface, but with the remaining coarea input split into a radial density representation plus a.e. derivative identification. This is the next target for replacing the abstract coarea assumption by a direct measure-theoretic proof.
Same Euclidean weak-map monotonicity interface with the final coarea input split into the pure weighted radial representation and the a.e. derivative identification of the representing density.
Same Euclidean weak-map monotonicity interface after the unrestricted one-dimensional derivative-identification theorem has been proved: the only remaining coarea-side input is the pure weighted radial representation.
Restricted-weight Euclidean weak-map monotonicity interface with the final coarea input split into the restricted weighted radial representation and the restricted a.e. derivative identification.
Restricted-weight Euclidean weak-map monotonicity interface after the restricted derivative-identification theorem has been proved: the only remaining coarea-side input is the restricted weighted radial representation.
Fully Euclidean weak-map monotonicity interface after the radial pushforward/coarea representation has been supplied by the Radon-Nikodym density.
Fully Euclidean weak-map increment formula in the origin-centered form.
This is the equality form of the monotonicity formula:
weakTheta r - weakTheta s is the annular radial-energy term
weakMonotonicityRhs s r.
Final packaged weak-map interface with the primitive-cutoff realization constructed from interval integrals and smooth bumps. The remaining one-dimensional inputs are the energy IBP formula and its integrability side conditions.