Radius absolute continuity inputs

This module contains the abstract absolute-continuity and integration-by-parts interfaces for the radius-variable energy functions.

These radius formulas are internal scaffolding. They remain visible so the coarea and one-dimensional calculus steps can be audited independently, while public users should rely on MainTheorem.lean.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakOneDimensionalIBPStep {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The one-dimensional integration-by-parts step to be proved from WeakRadialOneDimensionalIdentity.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakOneDimensionalIBPFormula {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The concrete integration-by-parts identity needed to turn the one-dimensional radial identity into a defect-derivative identity.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakBallEnergyIntegrationByPartsFormula {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The genuine one-dimensional energy integration-by-parts input: ∫ -phi' ((n-2)E) = ∫ ((n-2)phi) E'. This is the part that ultimately comes from absolute continuity of the ball energy function.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakOneDimensionalIBPIntegrability {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

Integrability side conditions needed only to justify splitting the Bochner integrals in the one-dimensional IBP algebra.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakEnergyAbsolutelyContinuousOnRadii {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The absolute-continuity target for the radius functions used in the weak monotonicity proof. This is the analytic statement one ultimately gets from coarea/radius differentiation in the W^{1,2}_{loc} setting.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusAbsolutelyContinuous {n : ℕ} (f : Domain n → ℝ) (R0 : ℝ) : Prop

Absolute continuity, in the radius variable, of the ball integral generated by a scalar integrand. This is the generic analytic statement supplied by the coarea/radius theorem for L¹ functions.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusACOfIntegrableOnBall (n : ℕ) : Prop

The reusable analytic theorem we still need from coarea/thin-annulus estimates: in positive dimension, every L¹ scalar integrand on B_R0 has an absolutely continuous ball-integral radius function on [0, R0]. The positive dimension assumption is essential: in dimension zero the open ball jumps at radius 0.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.locallyIntegrableOn_deriv_ballIntegral_of_radius_ac {n : ℕ} {f : Domain n → ℝ} {R0 : ℝ} (hac : BallIntegralRadiusAbsolutelyContinuous f R0) : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) (Set.Ioo 0 R0) MeasureTheory.volume

Absolute continuity of a scalar ball-integral radius function gives local integrability of its a.e. derivative on the open radius interval.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusDerivativeFormula (n : ℕ) : Prop

The reusable coarea/radius-derivative theorem still to be supplied geometrically: every L¹ scalar density on a ball has the radius integration formula against arbitrary scalar radius weights. The specialized weak energy and radial-energy formulas below are just applications of this statement to the two relevant densities.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusDerivativeFormulaForWeights (n : ℕ) : Prop

Restricted-weight version of BallIntegralRadiusDerivativeFormula, using the measurable essentially bounded radius weights that occur in the weak monotonicity proof.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusWeightedRepresentation (n : ℕ) : Prop

Pure radial pushforward/coarea input: a scalar density on a Euclidean ball has some one-dimensional radial density D representing all integrals against radius weights. No derivative of the ball integral is mentioned here.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusWeightedRepresentationForWeights (n : ℕ) : Prop

Restricted-weight version of the pure radial pushforward/coarea input.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusDerivativeIdentification (n : ℕ) : Prop

One-dimensional identification input: whenever a radial density represents all radius-weighted integrals of f, it agrees a.e. with the derivative of the ball integral radius function.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusDerivativeIdentificationForWeights (n : ℕ) : Prop

Restricted-weight version of the one-dimensional derivative identification input. This is the realistic version of the uniqueness step: bounded measurable test weights determine equality a.e. on the radius interval.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusDerivativeRepresentation (n : ℕ) : Prop

A more geometric way to supply BallIntegralRadiusDerivativeFormula: for each scalar density on a ball, produce a one-dimensional radial density D which both represents all radius-weighted integrals and agrees a.e. with the derivative of the ball integral radius function. This separates the genuine coarea/pushforward theorem from the one-dimensional derivative identification.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BallIntegralRadiusDerivativeRepresentationForWeights (n : ℕ) : Prop

Restricted-weight version of the combined radial-density representation.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormulaForWeights_of_unrestricted {n : ℕ} (hcoarea : BallIntegralRadiusDerivativeFormula n) : BallIntegralRadiusDerivativeFormulaForWeights n

The unrestricted generic coarea formula implies the restricted-weight version.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusWeightedRepresentationForWeights_of_unrestricted {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentation n) : BallIntegralRadiusWeightedRepresentationForWeights n

The unrestricted weighted representation implies its restricted-weight version.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeRepresentation_of_weightedRepresentation {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentation n) (hidentify : BallIntegralRadiusDerivativeIdentification n) : BallIntegralRadiusDerivativeRepresentation n

A pure weighted radial representation plus the a.e. derivative identification give the combined radial-density representation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeRepresentationForWeights_of_weightedRepresentation {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentationForWeights n) (hidentify : BallIntegralRadiusDerivativeIdentificationForWeights n) : BallIntegralRadiusDerivativeRepresentationForWeights n

Restricted weighted representation plus restricted a.e. derivative identification give the restricted combined representation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormula_of_representation {n : ℕ} (hrep : BallIntegralRadiusDerivativeRepresentation n) : BallIntegralRadiusDerivativeFormula n

The radial-density representation immediately gives the older packaged coarea/radius-derivative formula.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormulaForWeights_of_representation {n : ℕ} (hrep : BallIntegralRadiusDerivativeRepresentationForWeights n) : BallIntegralRadiusDerivativeFormulaForWeights n

The restricted radial-density representation gives the restricted packaged coarea/radius-derivative formula.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormulaForWeights_of_weightedRepresentation {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentationForWeights n) (hidentify : BallIntegralRadiusDerivativeIdentificationForWeights n) : BallIntegralRadiusDerivativeFormulaForWeights n

Restricted weighted representation and restricted derivative identification directly give the restricted coarea/radius-derivative formula.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.EuclideanBallVolumeAbsolutelyContinuous (n : ℕ) : Prop

A one-dimensional form of the remaining Euclidean geometry needed for the thin radial-shell estimate: the radius function r ↦ |B_r| is absolutely continuous on compact nonnegative intervals. This is discharged through the project Euclidean interface.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialOpenShell {n : ℕ} (r s : ℝ) : Set (Domain n)

The radial open shell between two radii. We use the unordered endpoints so that the shell attached to an interval in the absolute-continuity definition is independent of its orientation.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialOpenShell r s = {x : LeanStationaryHarmonicMaps.StationaryHarmonicMap.Domain n | ‖x‖ ∈ Set.Ioo (min r s) (max r s)}

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialOpenShells {n : ℕ} (E : ℕ × (ℕ → ℝ × ℝ)) : Set (Domain n)

The union of the radial open shells associated to a finite interval family from the absolute-continuity filter.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialOpenShells E = ⋃ i ∈ Finset.range E.1, LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialOpenShell (E.2 i).1 (E.2 i).2

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialOpenShellsVolumeTendstoZero (n : ℕ) : Prop

The geometric thin-annulus estimate needed for the L¹ radius theorem: finite unions of radial shells have volume tending to zero when the total one-dimensional length of the generating intervals tends to zero.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShell_measurable {n : ℕ} (r s : ℝ) : MeasurableSet (RadialOpenShell r s)

A radial open shell is Borel measurable.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShell_subset_uIoc {n : ℕ} (r s : ℝ) : RadialOpenShell r s ⊆ {x : Domain n | ‖x‖ ∈ Set.uIoc r s}

The open shell is contained in the unordered half-open interval shell used by the absolute-continuity filter.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShell_volume_le_ballVolume_dist {n : ℕ} [NeZero n] (r s : ℝ) : MeasureTheory.volume (RadialOpenShell r s) ≤ ENNReal.ofReal (dist (MeasureTheory.volume (Metric.ball 0 r)).toReal (MeasureTheory.volume (Metric.ball 0 s)).toReal)

A single radial shell has volume controlled by the variation of the ball volume radius function across its two endpoints.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShells_measurable {n : ℕ} (E : ℕ × (ℕ → ℝ × ℝ)) : MeasurableSet (RadialOpenShells E)

Finite unions of radial open shells are measurable.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShells_volume_le_ballVolume_variation {n : ℕ} [NeZero n] (E : ℕ × (ℕ → ℝ × ℝ)) : MeasureTheory.volume (RadialOpenShells E) ≤ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (MeasureTheory.volume (Metric.ball 0 (E.2 i).1)).toReal (MeasureTheory.volume (Metric.ball 0 (E.2 i).2)).toReal)

A finite union of radial shells is controlled by the corresponding variation sum of the ball-volume radius function.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShellsVolumeTendstoZero_of_ballVolume_ac {n : ℕ} (hball : EuclideanBallVolumeAbsolutelyContinuous n) : RadialOpenShellsVolumeTendstoZero n

Absolute continuity of the Euclidean ball-volume radius function implies the thin radial-shell volume estimate used in the weak monotonicity proof.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.pairwiseDisjoint_radialOpenShell_of_disjWithin {n : ℕ} {a b : ℝ} {E : ℕ × (ℕ → ℝ × ℝ)} (hE : E ∈ AbsolutelyContinuousOnInterval.disjWithin a b) : (↑(Finset.range E.1)).PairwiseDisjoint fun (i : ℕ) => RadialOpenShell (E.2 i).1 (E.2 i).2

Disjoint radius intervals give disjoint radial open shells.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShells_restrictVolume_tendstoZero {n : ℕ} [NeZero n] {a b R0 : ℝ} (hthin : RadialOpenShellsVolumeTendstoZero n) (ha : 0 ≤ a) (hab : a ≤ b) : Filter.Tendsto (fun (E : ℕ × (ℕ → ℝ × ℝ)) => (MeasureTheory.volume.restrict (Metric.ball 0 R0)) (RadialOpenShells E)) (AbsolutelyContinuousOnInterval.totalLengthFilter ⊓ Filter.principal (AbsolutelyContinuousOnInterval.disjWithin a b)) (nhds 0)

The thin-annulus volume estimate remains true after restricting the ambient measure to any fixed ball.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShells_lintegral_enorm_tendstoZero {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 : ℝ} (hthin : RadialOpenShellsVolumeTendstoZero n) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (ha : 0 ≤ a) (hab : a ≤ b) : Filter.Tendsto (fun (E : ℕ × (ℕ → ℝ × ℝ)) => ∫⁻ (x : Domain n) in RadialOpenShells E, ‖f x‖ₑ ∂MeasureTheory.volume.restrict (Metric.ball 0 R0)) (AbsolutelyContinuousOnInterval.totalLengthFilter ⊓ Filter.principal (AbsolutelyContinuousOnInterval.disjWithin a b)) (nhds 0)

Consequently, an L¹ integrand has vanishing integral over such thin radial shell unions.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyAbsolutelyContinuousOnRadii_of_ballIntegralRadiusAC {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (henergy_ac : BallIntegralRadiusAbsolutelyContinuous (fun (x : Domain n) => weakEnergyDensity Du x) R0) (hradial_ac : BallIntegralRadiusAbsolutelyContinuous (fun (x : Domain n) => weakRadialEnergyDensity Du 0 x) R0) : WeakEnergyAbsolutelyContinuousOnRadii Du R0

If the two scalar densities have absolutely continuous ball-integral radius functions, then the weak energy and weak radial energy radius functions are absolutely continuous.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyAbsolutelyContinuousOnRadii_of_locallyL2_ballIntegralAC {n m : ℕ} [NeZero n] {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hball_ac : BallIntegralRadiusACOfIntegrableOnBall n) (hDu_meas : GradientAEStronglyMeasurableIn Du Ω) (hgrad : GradientLocallyL2In Du Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) : WeakEnergyAbsolutelyContinuousOnRadii Du R0

Local L² control plus the generic L¹ ball-integral AC theorem supplies absolute continuity of the weak energy and weak radial energy radius functions.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyAbsolutelyContinuousOnRadii_of_W12LocIn_ballIntegralAC {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hball_ac : BallIntegralRadiusACOfIntegrableOnBall n) (hW : W12LocIn u Du Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) : WeakEnergyAbsolutelyContinuousOnRadii Du R0

The W^{1,2}_{loc} packaged version of radius absolute continuity, using the generic L¹ ball-integral AC theorem.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakBallEnergyOneDimensionalCalculus {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

A single package for the one-dimensional radius calculus still needed after radial stationarity has been reduced to scalar cutoffs. The first field records the intended absolute-continuity theorem; the last two fields are the concrete IBP and integrability consequences consumed by the existing algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyAbsolutelyContinuousOnRadii_of_oneDimensionalCalculus {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hcalc : WeakBallEnergyOneDimensionalCalculus Du R0) : WeakEnergyAbsolutelyContinuousOnRadii Du R0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBallEnergyIntegrationByPartsFormula_of_oneDimensionalCalculus {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hcalc : WeakBallEnergyOneDimensionalCalculus Du R0) : WeakBallEnergyIntegrationByPartsFormula Du R0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakOneDimensionalIBPIntegrability_of_oneDimensionalCalculus {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hcalc : WeakBallEnergyOneDimensionalCalculus Du R0) : WeakOneDimensionalIBPIntegrability Du R0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.integral_Ioo_zero_radius_indicator_Ioo_eq_intervalIntegral {f : ℝ → ℝ} {a b R0 : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ R0) : ∫ (rho : ℝ) in Set.Ioo 0 R0, (Set.Ioo a b).indicator (fun (x : ℝ) => 1) rho * f rho = ∫ (rho : ℝ) in a..b, f rho

Trimming an integral over (0, R0) by the indicator of (a, b) gives the usual interval integral over a..b, provided 0 ≤ a ≤ b ≤ R0.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.absolutelyContinuousOnInterval_congr_uIcc {f g : ℝ → ℝ} {a b : ℝ} (hfg : Set.EqOn f g (Set.uIcc a b)) (hg : AbsolutelyContinuousOnInterval g a b) : AbsolutelyContinuousOnInterval f a b

Absolute continuity is unchanged when two functions agree on the closed interval where it is tested.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.euclideanBallVolumeAbsolutelyContinuous (n : ℕ) : EuclideanBallVolumeAbsolutelyContinuous n

The Euclidean ball-volume radius function is absolutely continuous on every compact nonnegative radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialOpenShellsVolumeTendstoZero_euclidean (n : ℕ) : RadialOpenShellsVolumeTendstoZero n

The thin radial-shell volume estimate in Euclidean space.