Weak radius formula constructors #
This module constructs the weak radius integration and one-dimensional calculus packages from local L2, coarea, and annulus inputs.
Integrability of the weak energy and weak radial energy on the ambient ball turns the open-annulus identity into the packaged annulus formula.
Local L² control and a.e. measurability supply the annulus formula on a
closed ball contained in the weak map domain.
A W^{1,2}_{loc} map with chosen weak gradient automatically has the
annulus formula on any closed ball contained in the domain.
The generic ball-integral radius derivative formula specializes to the weak energy radius formula.
The restricted generic ball-integral radius derivative formula specializes to the restricted weak energy radius formula.
The generic ball-integral radius derivative formula specializes to the weak radial-energy radius formula.
The restricted generic ball-integral radius derivative formula specializes to the restricted weak radial-energy radius formula.
Local L² control plus the generic ball-integral radius derivative theorem
supplies both weak radius integration formulas on a contained ball.
Local L² control plus the restricted generic ball-integral radius
derivative theorem supplies both restricted weak radius integration formulas on
a contained ball.
W^{1,2}_{loc} data plus the generic ball-integral radius derivative
theorem supplies both weak radius integration formulas.
W^{1,2}_{loc} data plus the restricted generic ball-integral radius
derivative theorem supplies both restricted weak radius integration formulas.
W^{1,2}_{loc} data plus bounded a.e. interval-step approximation of
radius weights supplies the two restricted weak radius integration formulas.
This is the direct bridge from the finite-step cutoff/coarea core to the weak
map package.
The radius integration formula, after localization to an annulus, gives the increment/FTC form of the radius calculus.
Restricted-weight radius integration is enough for the annulus-localized
increment/FTC form, since the localization weight is the bounded measurable
indicator of (a, b).
The increment/FTC form gives the primitive form by fixing the left endpoint and applying the increment identity to each intermediate radius.
The radius primitive formula immediately gives absolute continuity of the ball-energy and radial-energy radius functions.
The increment/FTC form gives absolute continuity of the two radius energy functions.
Absolute continuity of the ball-energy radius function gives the concrete one-dimensional energy integration-by-parts formula.
Absolute continuity of the ball-energy and radial-energy radius functions also gives the integrability side conditions used in the one-dimensional algebraic splitting.
Constructor for the packaged one-dimensional calculus: on a nonnegative
radius interval, absolute continuity of E(r) and Q(r) supplies both the
energy IBP formula and the integrability side conditions.
Constructor for the packaged one-dimensional calculus from the increment/FTC form of the radius energy identities.
Constructor for the packaged one-dimensional calculus from radius integration localized to annuli.
Restricted-weight radius integration over annuli gives the packaged one-dimensional calculus.
Radius integration over annuli plus radius absolute continuity gives the one-dimensional calculus package; the derivative integrability is extracted automatically from the absolute-continuity input.
Restricted-weight radius integration over annuli plus radius absolute continuity gives the one-dimensional calculus package.
Local L² control supplies the annulus formula needed by the radius
integration route to the one-dimensional calculus package.
Local L² control supplies the annulus formula needed by the
restricted-weight radius integration route to the one-dimensional calculus
package.
W^{1,2}_{loc} supplies the annulus formula needed by the radius
integration route to the one-dimensional calculus package.
W^{1,2}_{loc} supplies the annulus formula needed by the
restricted-weight radius integration route to the one-dimensional calculus
package.
Local L² supplies the annulus formula, while radius absolute continuity
supplies derivative integrability; this is the annulus route without a separate
WeakEnergyRadiusDerivativeIntegrability assumption.
Local L² supplies the annulus formula, while radius absolute continuity
supplies derivative integrability; this is the restricted-weight annulus route
without a separate derivative-integrability hypothesis.
W^{1,2}_{loc} supplies the annulus formula, while radius absolute
continuity supplies derivative integrability; this is the W^{1,2} packaged
version with no separate derivative-integrability hypothesis.
W^{1,2}_{loc} supplies the annulus formula, while radius absolute
continuity supplies derivative integrability; this is the restricted-weight
packaged version with no separate derivative-integrability hypothesis.
The radius-integration route with the generic L¹ ball-integral AC theorem
supplying the radius absolute-continuity input from W^{1,2}_{loc}.
The restricted-weight radius-integration route with the generic L¹
ball-integral AC theorem supplying the radius absolute-continuity input from
W^{1,2}_{loc}.
The radius-integration route with thin radial-shell volume control supplying
the radius absolute-continuity input from W^{1,2}_{loc}.
The restricted-weight radius-integration route with thin radial-shell
volume control supplying the radius absolute-continuity input from
W^{1,2}_{loc}.