Radius primitive formulas

This module contains primitive, increment, annulus, and interval-indicator forms of the radius derivative calculus.

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

Primitive form of the radius calculus: on every subinterval of (0, R0), both ball-energy functions are equal to their interval primitive of the stated derivative. This is the exact one-dimensional FTC statement extracted from coarea/radius differentiation.

Equations

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

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

Increment form of the radius calculus: the two ball-energy functions satisfy the fundamental theorem of calculus on every subinterval of [0, R0].

Equations

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

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

Interval integrability of the two radius derivatives on every subinterval of [0, R0].

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyRadiusDerivativeIntegrability_of_radius_ac {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) : WeakEnergyRadiusDerivativeIntegrability Du R0

Absolute continuity of the two radius functions supplies the interval integrability of their derivatives on all subintervals of [0, R0].

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBallEnergy_locallyIntegrableOn_Ioo_of_radius_ac {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakBallEnergy Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume

Absolute continuity of the energy radius function gives local integrability of the energy itself on the open radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.locallyIntegrableOn_deriv_weakBallEnergy_of_radius_ac {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => deriv (weakBallEnergy Du 0) rho) (Set.Ioo 0 R0) MeasureTheory.volume

Absolute continuity of the energy radius function gives local integrability of its a.e. derivative on the open radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.locallyIntegrableOn_deriv_weakBallRadialEnergy_of_radius_ac {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => deriv (weakBallRadialEnergy Du 0) rho) (Set.Ioo 0 R0) MeasureTheory.volume

Absolute continuity of the radial-energy radius function gives local integrability of its a.e. derivative on the open radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffDefect_locallyIntegrableOn_of_radius_ac {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume

The sharp-cutoff defect is locally integrable once the two radius energy functions are absolutely continuous on compact subintervals of [0, R0].

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyRadiusDerivativeIntegrability_of_radiusPrimitive {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hprim : WeakEnergyRadiusPrimitiveFormula Du R0) : WeakEnergyRadiusDerivativeIntegrability Du R0

The primitive/FTC radius package contains the derivative integrability field, so it can be projected out when needed by lower-level constructors.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyRadiusDerivativeIntegrability_of_radiusIncrement {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hinc : WeakEnergyRadiusIncrementFormula Du R0) : WeakEnergyRadiusDerivativeIntegrability Du R0

The increment/FTC radius package contains the derivative integrability field, so it can be projected out when needed by lower-level constructors.

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

Annulus form of the ball-energy increments. The open annulus is enough: the missing boundary spheres are null in the eventual geometric proof.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ball_diff_closedBall_ae_eq_ball_diff_ball {n : ℕ} [NeZero n] {a b : ℝ} : Metric.ball 0 b \ Metric.closedBall 0 a =ᵐ[MeasureTheory.volume] Metric.ball 0 b \ Metric.ball 0 a

The open annulus B_b \ closedBall_a differs from B_b \ B_a only by the inner sphere. In positive dimension that sphere has zero Lebesgue measure.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ball_annulus_indicator_integral_eq_energy_diff {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 : ℝ} (hab : a ≤ b) (hb : b ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 b) MeasureTheory.volume) : ∫ (x : Domain n) in Metric.ball 0 R0, (Set.Ioo a b).indicator (fun (x : ℝ) => 1) ‖x‖ * f x = (∫ (x : Domain n) in Metric.ball 0 b, f x) - ∫ (x : Domain n) in Metric.ball 0 a, f x

Integrating a radial indicator over a containing ball realizes the energy increment between the two open balls.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorMeasure_apply_Ioo_eq_ballIntegral_sub {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 : ℝ} (hab : a ≤ b) (hb : b ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : (((MeasureTheory.volume.restrict (Metric.ball 0 R0)).withDensityᵥ f).map fun (x : Domain n) => ‖x‖) (Set.Ioo a b) = (∫ (x : Domain n) in Metric.ball 0 b, f x) - ∫ (x : Domain n) in Metric.ball 0 a, f x

The radial signed pushforward of f dx on the ambient ball, evaluated on an interval of radii, is the corresponding ball-integral increment.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorMeasure_apply_Ioo_eq_integral_deriv_ballIntegral {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hac : BallIntegralRadiusAbsolutelyContinuous f R0) : (((MeasureTheory.volume.restrict (Metric.ball 0 R0)).withDensityᵥ f).map fun (x : Domain n) => ‖x‖) (Set.Ioo a b) = ∫ (rho : ℝ) in a..b, deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

If the ball-integral radius function is absolutely continuous, then the radial signed pushforward of f dx on (a, b) is the integral of the a.e. radius derivative over [a, b].

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormulaForIndicator_Ioo {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hac : BallIntegralRadiusAbsolutelyContinuous f R0) : ∫ (x : Domain n) in Metric.ball 0 R0, (Set.Ioo a b).indicator (fun (x : ℝ) => 1) ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, (Set.Ioo a b).indicator (fun (x : ℝ) => 1) rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

The ball-integral radius derivative formula for interval-indicator weights. This is the interval/simple-function core of the remaining extension to all bounded measurable radius weights.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormulaForIndicatorConst_Ioo {n : ℕ} [NeZero n] {f : Domain n → ℝ} {a b R0 k : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hac : BallIntegralRadiusAbsolutelyContinuous f R0) : ∫ (x : Domain n) in Metric.ball 0 R0, (Set.Ioo a b).indicator (fun (x : ℝ) => k) ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, (Set.Ioo a b).indicator (fun (x : ℝ) => k) rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

The interval-indicator radius derivative formula, with a scalar coefficient in front of the interval indicator.