Weak radial integrability #
This module contains the weak radial integrands and the integrability lemmas that discharge the side conditions in the radial stationarity identity.
noncomputable def
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainIntegrand
{n m : ℕ}
(Du : Domain n → Gradient n m)
(phi : ℝ → ℝ)
(x : Domain n)
:
The main energy integrand in the weak radial identity at center 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsIntegrand
{n m : ℕ}
(Du : Domain n → Gradient n m)
(phi : ℝ → ℝ)
(x : Domain n)
:
The radial-energy integrand in the weak radial identity at center 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.integrableOn_bdd_mul_of_integrableOn
{n : ℕ}
{Ω : Set (Domain n)}
{c g : Domain n → ℝ}
{C : ℝ}
(hg : MeasureTheory.IntegrableOn g Ω MeasureTheory.volume)
(hc_meas : MeasureTheory.AEStronglyMeasurable c (MeasureTheory.volume.restrict Ω))
(hc_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖c x‖ ≤ C)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => c x * g x) Ω MeasureTheory.volume
Multiplication by an a.e. bounded scalar coefficient preserves integrability on a set.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.integrableOn_of_norm_le_integrableOn
{n : ℕ}
{Ω : Set (Domain n)}
{f g : Domain n → ℝ}
(hg : MeasureTheory.IntegrableOn g Ω MeasureTheory.volume)
(hf_meas : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict Ω))
(hbound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖f x‖ ≤ g x)
:
A function dominated in norm by an integrable scalar function is integrable on the set.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyDensity_integrableOn_of_energy_bound
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
(henergy : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) Ω MeasureTheory.volume)
(hradial_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x)
(MeasureTheory.volume.restrict Ω))
(hradial_bound :
∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialEnergyDensity Du 0 x‖ ≤ weakEnergyDensity Du x)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x) Ω MeasureTheory.volume
Radial energy is integrable once it is a.e. dominated by the weak energy density.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyDensity_integrableOn_of_energy
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
(henergy : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) Ω MeasureTheory.volume)
(hradial_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x)
(MeasureTheory.volume.restrict Ω))
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x) Ω MeasureTheory.volume
Radial energy is integrable on a set as soon as weak energy is integrable there, provided the radial-energy density is a.e. strongly measurable.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialMainIntegrand_integrableOn_of_bounded_coeff
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{phi : ℝ → ℝ}
{C : ℝ}
(henergy : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) Ω MeasureTheory.volume)
(hcoeff_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x)
(MeasureTheory.volume.restrict Ω))
(hcoeff_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialMainCoeff n phi x‖ ≤ C)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialMainIntegrand Du phi x) Ω MeasureTheory.volume
If the radial main coefficient is a.e. bounded and the weak energy is integrable, then the main radial integrand is integrable.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialRhsIntegrand_integrableOn_of_bounded_coeff
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{phi : ℝ → ℝ}
{C : ℝ}
(hradial : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x) Ω MeasureTheory.volume)
(hcoeff_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x) (MeasureTheory.volume.restrict Ω))
(hcoeff_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialRhsCoeff phi x‖ ≤ C)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialRhsIntegrand Du phi x) Ω MeasureTheory.volume
If the radial right-hand coefficient is a.e. bounded and the weak radial energy is integrable, then the right-hand radial integrand is integrable.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_cutoff_integrable_of_bounded_coefficients
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{phi : ℝ → ℝ}
{Cmain Crhs : ℝ}
(henergy : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) Ω MeasureTheory.volume)
(hradial : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x) Ω MeasureTheory.volume)
(hmain_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x)
(MeasureTheory.volume.restrict Ω))
(hmain_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialMainCoeff n phi x‖ ≤ Cmain)
(hrhs_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x) (MeasureTheory.volume.restrict Ω))
(hrhs_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialRhsCoeff phi x‖ ≤ Crhs)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialMainIntegrand Du phi x) Ω MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialRhsIntegrand Du phi x) Ω MeasureTheory.volume
A single package for the two integrability estimates needed in the weak radial identity.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_cutoff_integrable_of_energy_bound
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{phi : ℝ → ℝ}
{Cmain Crhs : ℝ}
(henergy : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) Ω MeasureTheory.volume)
(hradial_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x)
(MeasureTheory.volume.restrict Ω))
(hradial_bound :
∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialEnergyDensity Du 0 x‖ ≤ weakEnergyDensity Du x)
(hmain_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x)
(MeasureTheory.volume.restrict Ω))
(hmain_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialMainCoeff n phi x‖ ≤ Cmain)
(hrhs_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x) (MeasureTheory.volume.restrict Ω))
(hrhs_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialRhsCoeff phi x‖ ≤ Crhs)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialMainIntegrand Du phi x) Ω MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialRhsIntegrand Du phi x) Ω MeasureTheory.volume
The two radial-integrability estimates using only weak-energy integrability, provided radial energy is a.e. dominated by weak energy.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_cutoff_integrable_of_energy
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{phi : ℝ → ℝ}
{Cmain Crhs : ℝ}
(henergy : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) Ω MeasureTheory.volume)
(hradial_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x)
(MeasureTheory.volume.restrict Ω))
(hmain_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialMainCoeff n phi x)
(MeasureTheory.volume.restrict Ω))
(hmain_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialMainCoeff n phi x‖ ≤ Cmain)
(hrhs_meas :
MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialRhsCoeff phi x) (MeasureTheory.volume.restrict Ω))
(hrhs_bound : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict Ω, ‖weakRadialRhsCoeff phi x‖ ≤ Crhs)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialMainIntegrand Du phi x) Ω MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialRhsIntegrand Du phi x) Ω MeasureTheory.volume
The two radial-integrability estimates using weak-energy integrability and
the pointwise bound weakRadialEnergyDensity ≤ weakEnergyDensity.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_cutoff_integrable_of_locallyL2
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 M0 M1 : ℝ}
{phi : ℝ → ℝ}
(hDu_meas : GradientAEStronglyMeasurableIn Du Ω)
(hgrad : GradientLocallyL2In Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
(hphi_c1 : ContDiff ℝ 1 phi)
(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)
:
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
The two radial-integrability estimates on a ball, with weak-gradient measurability and weak-energy integrability supplied on a containing set.
The coefficient measurability comes from ContDiff ℝ 1 phi, and the a.e.
bounds come from pointwise bounds for phi and phi' on [0, R0].
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_cutoff_integrable_of_locallyL2_cutoff
{n m : ℕ}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 M0 M1 : ℝ}
{phi : ℝ → ℝ}
(hDu_meas : GradientAEStronglyMeasurableIn Du Ω)
(hgrad : GradientLocallyL2In Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
(hcut : AdmissibleRadialCutoff n R0 M0 M1 phi)
:
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
Cutoff-integrability on a ball, using the packaged cutoff interface.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_cutoff_integrable_of_W12Loc_cutoff
{n m : ℕ}
{u : Domain n → Target m}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 M0 M1 : ℝ}
{phi : ℝ → ℝ}
(hW : W12LocIn u Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
(hcut : AdmissibleRadialCutoff n R0 M0 M1 phi)
:
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
Cutoff-integrability on a ball from the W^{1,2}_{loc} interface.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_cutoff_integrable_of_W12Loc_contDiffBump
{n m : ℕ}
{u : Domain n → Target m}
{Du : Domain n → Gradient n m}
{Ω : Set (Domain n)}
{R0 : ℝ}
(hW : W12LocIn u Du Ω)
(hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω)
(f : ContDiffBump 0)
(hRout : f.rOut < R0)
:
MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialMainIntegrand Du (fun (t : ℝ) => ↑f t) x) (Metric.ball 0 R0)
MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (x : Domain n) => weakRadialRhsIntegrand Du (fun (t : ℝ) => ↑f t) x)
(Metric.ball 0 R0) MeasureTheory.volume
Cutoff-integrability for a one-dimensional smooth bump cutoff.