Weak radial stationarity identity #
This module turns weak stationarity tested against radial vector fields into
the weak radial integral identity, with integrability side conditions supplied
by RadialIntegrability.
def
LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialStationarityIdentity
{n m : ℕ}
(u : Domain n → Target m)
(R0 : ℝ)
:
The radial identity obtained by testing stationarity with X(x) = phi(|x|) x.
This is equation (1) in the LaTeX proof, stated for the smooth model and center 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialStationarityIdentity
{n m : ℕ}
(Du : Domain n → Gradient n m)
(R0 : ℝ)
:
Weak radial identity obtained by testing stationarity with X(x)=phi(|x|)x,
stated at center 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakStationarityIntegrand_radialVectorField_ae
{n m : ℕ}
[NeZero n]
(Du : Domain n → Gradient n m)
{phi : ℝ → ℝ}
(hphi : Differentiable ℝ phi)
(R0 : ℝ)
:
(fun (x : Domain n) =>
weakStationarityIntegrand Du (radialVectorField phi) x) =ᵐ[MeasureTheory.volume.restrict (Metric.ball 0 R0)] fun (x : Domain n) => weakRadialMainIntegrand Du phi x - 2 * weakRadialRhsIntegrand Du phi x
The pointwise radial integrand simplification holds almost everywhere on balls: the only excluded point is the origin.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity
{n m : ℕ}
[NeZero n]
{Du : Domain n → Gradient n m}
{R0 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
{phi : ℝ → ℝ}
(hphi : Differentiable ℝ phi)
(hXdiff : ContDiff ℝ 1 (radialVectorField phi))
(hXcompact : HasCompactSupport (radialVectorField phi))
(hXsupport : tsupport (radialVectorField phi) ⊆ Metric.ball 0 R0)
(hmain_int :
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialMainIntegrand Du phi x) (Metric.ball 0 R0)
MeasureTheory.volume)
(hrhs_int :
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialRhsIntegrand Du phi x) (Metric.ball 0 R0)
MeasureTheory.volume)
:
∫ (x : Domain n) in Metric.ball 0 R0, weakRadialMainIntegrand Du phi x = 2 * ∫ (x : Domain n) in Metric.ball 0 R0, weakRadialRhsIntegrand Du phi x
Weak stationarity plus the radial vector-field computation gives the weak
radial identity, once the two resulting radial integrands are known to be
integrable on the ball. The integrability hypotheses will later be discharged
from W^{1,2}_{loc} and compact support of the cutoff.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity_of_energy_bound
{n m : ℕ}
[NeZero n]
{Du : Domain n → Gradient n m}
{R0 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
{phi : ℝ → ℝ}
(hphi : Differentiable ℝ phi)
(hXdiff : ContDiff ℝ 1 (radialVectorField phi))
(hXcompact : HasCompactSupport (radialVectorField phi))
(hXsupport : tsupport (radialVectorField phi) ⊆ Metric.ball 0 R0)
{Cmain Crhs : ℝ}
(henergy :
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) (Metric.ball 0 R0) MeasureTheory.volume)
(hradial_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x)
(MeasureTheory.volume.restrict (Metric.ball 0 R0)))
(hradial_bound :
∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖weakRadialEnergyDensity Du 0 x‖ ≤ weakEnergyDensity Du x)
(hmain_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x)
(MeasureTheory.volume.restrict (Metric.ball 0 R0)))
(hmain_bound :
∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖weakRadialMainCoeff n phi x‖ ≤ Cmain)
(hrhs_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x)
(MeasureTheory.volume.restrict (Metric.ball 0 R0)))
(hrhs_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖weakRadialRhsCoeff phi x‖ ≤ Crhs)
:
∫ (x : Domain n) in Metric.ball 0 R0, weakRadialMainIntegrand Du phi x = 2 * ∫ (x : Domain n) in Metric.ball 0 R0, weakRadialRhsIntegrand Du phi x
Weak stationarity gives the radial identity when the integrability side conditions are discharged from weak-energy integrability and bounded cutoff coefficients.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity_of_energy
{n m : ℕ}
[NeZero n]
{Du : Domain n → Gradient n m}
{R0 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
{phi : ℝ → ℝ}
(hphi : Differentiable ℝ phi)
(hXdiff : ContDiff ℝ 1 (radialVectorField phi))
(hXcompact : HasCompactSupport (radialVectorField phi))
(hXsupport : tsupport (radialVectorField phi) ⊆ Metric.ball 0 R0)
{Cmain Crhs : ℝ}
(henergy :
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) (Metric.ball 0 R0) MeasureTheory.volume)
(hradial_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x)
(MeasureTheory.volume.restrict (Metric.ball 0 R0)))
(hmain_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x)
(MeasureTheory.volume.restrict (Metric.ball 0 R0)))
(hmain_bound :
∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖weakRadialMainCoeff n phi x‖ ≤ Cmain)
(hrhs_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x)
(MeasureTheory.volume.restrict (Metric.ball 0 R0)))
(hrhs_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖weakRadialRhsCoeff phi x‖ ≤ Crhs)
:
∫ (x : Domain n) in Metric.ball 0 R0, weakRadialMainIntegrand Du phi x = 2 * ∫ (x : Domain n) in Metric.ball 0 R0, weakRadialRhsIntegrand Du phi x
Weak stationarity gives the radial identity from weak-energy integrability.
The radial-energy integrability is supplied by the pointwise estimate
weakRadialEnergyDensity ≤ weakEnergyDensity.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity_of_locallyL2
{n m : ℕ}
[NeZero n]
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 M0 M1 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
(hDu_meas : GradientAEStronglyMeasurableIn Du Ω)
(hgrad : GradientLocallyL2In Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
{phi : ℝ → ℝ}
(hphi : Differentiable ℝ phi)
(hphi_c1 : ContDiff ℝ 1 phi)
(hXdiff : ContDiff ℝ 1 (radialVectorField phi))
(hXcompact : HasCompactSupport (radialVectorField phi))
(hXsupport : tsupport (radialVectorField phi) ⊆ Metric.ball 0 R0)
(hphi_bound : ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖phi t‖ ≤ M0)
(hdphi_bound : ∀ (t : ℝ), 0 ≤ t → t ≤ R0 → ‖deriv phi t‖ ≤ M1)
(hR0_nonneg : 0 ≤ R0)
:
∫ (x : Domain n) in Metric.ball 0 R0, weakRadialMainIntegrand Du phi x = 2 * ∫ (x : Domain n) in Metric.ball 0 R0, weakRadialRhsIntegrand Du phi x
Weak stationarity gives the radial identity on a ball directly from
gradient measurability, GradientLocallyL2In on a containing set, and elementary
cutoff bounds.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity_of_locallyL2_cutoff
{n m : ℕ}
[NeZero n]
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 M0 M1 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
(hDu_meas : GradientAEStronglyMeasurableIn Du Ω)
(hgrad : GradientLocallyL2In Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
{phi : ℝ → ℝ}
(hcut : AdmissibleRadialCutoff n R0 M0 M1 phi)
:
∫ (x : Domain n) in Metric.ball 0 R0, weakRadialMainIntegrand Du phi x = 2 * ∫ (x : Domain n) in Metric.ball 0 R0, weakRadialRhsIntegrand Du phi x
Weak radial identity on a ball from local L² data and the packaged cutoff
interface.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity_of_W12Loc_cutoff
{n m : ℕ}
[NeZero n]
{u : Domain n → Target m}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 M0 M1 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
(hW : W12LocIn u Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
{phi : ℝ → ℝ}
(hcut : AdmissibleRadialCutoff n R0 M0 M1 phi)
:
∫ (x : Domain n) in Metric.ball 0 R0, weakRadialMainIntegrand Du phi x = 2 * ∫ (x : Domain n) in Metric.ball 0 R0, weakRadialRhsIntegrand Du phi x
Weak radial identity on a ball from the W^{1,2}_{loc} interface and the
packaged cutoff interface. The stationarity hypothesis is still stated on the
ball; proving its restriction from a larger domain is a separate localization
step.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity_of_W12Loc_contDiffBump
{n m : ℕ}
[NeZero n]
{u : Domain n → Target m}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
(hW : W12LocIn u Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
(f : ContDiffBump 0)
(hRout : f.rOut < R0)
:
∫ (x : Domain n) in Metric.ball 0 R0, weakRadialMainIntegrand Du (fun (t : ℝ) => ↑f t) x = 2 * ∫ (x : Domain n) in Metric.ball 0 R0, weakRadialRhsIntegrand Du (fun (t : ℝ) => ↑f t) x
Weak radial identity for a one-dimensional smooth bump cutoff. The
derivative-bound constant required by AdmissibleRadialCutoff is produced from
compactness of [0, R0].
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_identity_from_stationarity_with_integrability
{n m : ℕ}
[NeZero n]
{Du : Domain n → Gradient n m}
{R0 : ℝ}
(hstationary : WeakStationaryIn Du (Metric.ball 0 R0))
(hintegrable :
∀ (phi : ℝ → ℝ),
Differentiable ℝ phi →
ContDiff ℝ 1 (radialVectorField phi) →
HasCompactSupport (radialVectorField phi) →
tsupport (radialVectorField phi) ⊆ Metric.ball 0 R0 →
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialMainIntegrand Du phi x) (Metric.ball 0 R0)
MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialRhsIntegrand Du phi x) (Metric.ball 0 R0)
MeasureTheory.volume)
:
Full weak radial identity from weak stationarity, packaged with the
integrability estimates needed to split the integral of A - 2B.