Weighted radius derivative formulas

This module upgrades interval-indicator radius derivative formulas to general radius weights and identifies the radial derivative density.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.integrable_indicatorConst_norm_mul_of_integrableOn_ball {n : ℕ} {f : Domain n → ℝ} {a b R0 k : ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : Domain n) => (Set.Ioo a b).indicator (fun (x : ℝ) => k) ‖x‖ * f x) (MeasureTheory.volume.restrict (Metric.ball 0 R0))

A bounded interval-indicator radius coefficient preserves ball integrability.

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

A bounded interval-indicator radius coefficient preserves integrability of the derivative of the ball-integral radius function on (0, R0).

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadiusWeightOn.integrable_mul_deriv_ballIntegral_on_radiusInterval {n : ℕ} {f : Domain n → ℝ} {R0 : ℝ} {c : ℝ → ℝ} (hc : RadiusWeightOn R0 c) (hR0_nonneg : 0 ≤ R0) (hac : BallIntegralRadiusAbsolutelyContinuous f R0) : MeasureTheory.Integrable (fun (rho : ℝ) => c rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) (radiusIntervalMeasure R0)

An arbitrary admissible radius weight preserves integrability of the derivative of the ball-integral radius function on (0, R0).

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormulaForFiniteIndicatorConst_Ioo {n : ℕ} [NeZero n] {ι : Type u_1} {s : Finset ι} {f : Domain n → ℝ} {R0 : ℝ} {a b k : ι → ℝ} (ha : ∀ i ∈ s, 0 ≤ a i) (hab : ∀ i ∈ s, a i ≤ b i) (hb : ∀ i ∈ s, b i ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hac : BallIntegralRadiusAbsolutelyContinuous f R0) (hleft_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (x : Domain n) => (Set.Ioo (a i) (b i)).indicator (fun (x : ℝ) => k i) ‖x‖ * f x) (MeasureTheory.volume.restrict (Metric.ball 0 R0))) (hright_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (rho : ℝ) => (Set.Ioo (a i) (b i)).indicator (fun (x : ℝ) => k i) rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) (MeasureTheory.volume.restrict (Set.Ioo 0 R0))) : ∫ (x : Domain n) in Metric.ball 0 R0, (∑ i ∈ s, (Set.Ioo (a i) (b i)).indicator (fun (x : ℝ) => k i) ‖x‖) * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, (∑ i ∈ s, (Set.Ioo (a i) (b i)).indicator (fun (x : ℝ) => k i) rho) * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

Finite linear combinations of interval indicators satisfy the radius derivative formula, once the finite-sum integrability needed for Bochner linearity is supplied. The next measure-theoretic step is to discharge those integrability hypotheses from boundedness of the weights.

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

Finite linear combinations of interval indicators satisfy the radius derivative formula. The integrability side conditions are automatic from boundedness of the interval-indicator coefficients and absolute continuity of the ball-integral radius function.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormula_of_dominated_approx {n : ℕ} {f : Domain n → ℝ} {R0 : ℝ} {c : ℝ → ℝ} {cSeq : ℕ → ℝ → ℝ} {boundLeft : Domain n → ℝ} {boundRight : ℝ → ℝ} (hleft_meas : ∀ (N : ℕ), MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => cSeq N ‖x‖ * f x) (MeasureTheory.volume.restrict (Metric.ball 0 R0))) (hleft_bound_int : MeasureTheory.Integrable boundLeft (MeasureTheory.volume.restrict (Metric.ball 0 R0))) (hleft_bound : ∀ (N : ℕ), ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖cSeq N ‖x‖ * f x‖ ≤ boundLeft x) (hleft_lim : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), Filter.Tendsto (fun (N : ℕ) => cSeq N ‖x‖ * f x) Filter.atTop (nhds (c ‖x‖ * f x))) (hright_meas : ∀ (N : ℕ), MeasureTheory.AEStronglyMeasurable (fun (rho : ℝ) => cSeq N rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) (MeasureTheory.volume.restrict (Set.Ioo 0 R0))) (hright_bound_int : MeasureTheory.Integrable boundRight (MeasureTheory.volume.restrict (Set.Ioo 0 R0))) (hright_bound : ∀ (N : ℕ), ∀ᵐ (rho : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 R0), ‖cSeq N rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho‖ ≤ boundRight rho) (hright_lim : ∀ᵐ (rho : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 R0), Filter.Tendsto (fun (N : ℕ) => cSeq N rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) Filter.atTop (nhds (c rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho))) (hformula : ∀ (N : ℕ), ∫ (x : Domain n) in Metric.ball 0 R0, cSeq N ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, cSeq N rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) : ∫ (x : Domain n) in Metric.ball 0 R0, c ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, c rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

A dominated-convergence transfer principle for passing the radius derivative formula from approximating radius weights to the limiting radius weight. This is the measure-theoretic bridge needed after constructing finite interval-step approximations of a general admissible radius weight.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormula_congr_ae_weight {n : ℕ} {f : Domain n → ℝ} {R0 : ℝ} {c d : ℝ → ℝ} (hleft : (fun (x : Domain n) => c ‖x‖ * f x) =ᵐ[MeasureTheory.volume.restrict (Metric.ball 0 R0)] fun (x : Domain n) => d ‖x‖ * f x) (hright : (fun (rho : ℝ) => c rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) =ᵐ[MeasureTheory.volume.restrict (Set.Ioo 0 R0)] fun (rho : ℝ) => d rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) (hformula : ∫ (x : Domain n) in Metric.ball 0 R0, c ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, c rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho) : ∫ (x : Domain n) in Metric.ball 0 R0, d ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, d rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

The radius derivative formula is unchanged under a.e. modification of the radius weight, provided the pulled-back spatial coefficient is also unchanged a.e. on the ball.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormula_of_finiteIntervalStepApprox {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} {c : ℝ → ℝ} (hR0_nonneg : 0 ≤ R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hac : BallIntegralRadiusAbsolutelyContinuous f R0) (happrox : RadiusWeightFiniteIntervalStepApprox R0 c) : ∫ (x : Domain n) in Metric.ball 0 R0, c ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, c rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

A finite interval-step approximation of a radius weight upgrades the finite-interval radius derivative formula to that limiting weight.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormula_of_finiteIntervalStepApproxAE {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} {c : ℝ → ℝ} (hR0_pos : 0 < R0) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hac : BallIntegralRadiusAbsolutelyContinuous f R0) (happrox : RadiusWeightFiniteIntervalStepApproxAE R0 c) : ∫ (x : Domain n) in Metric.ball 0 R0, c ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, c rho * deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho

A finite interval-step approximation away from a countable exceptional set also upgrades the finite-interval radius derivative formula to the limiting weight.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeIdentificationForWeights_on_Ioo {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} {D : ℝ → ℝ} {a b : ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hD_loc : MeasureTheory.LocallyIntegrableOn D (Set.Ioo 0 R0) MeasureTheory.volume) (hweighted : ∀ (c : ℝ → ℝ), RadiusWeightOn R0 c → ∫ (x : Domain n) in Metric.ball 0 R0, c ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, c rho * D rho) (ha : 0 < a) (hab : a ≤ b) (hb : b < R0) : ∀ᵐ (rho : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), deriv (fun (r : ℝ) => ∫ (x : Domain n) in Metric.ball 0 r, f x) rho = D rho

Local one-dimensional derivative identification for the radial density obtained from all restricted radius-weighted integral identities. On every compact subinterval of (0, R0), the representing density agrees a.e. with the derivative of the ball integral radius function.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeIdentificationForWeights (n : ℕ) : BallIntegralRadiusDerivativeIdentificationForWeights n

The restricted-weight radial representation determines the a.e. derivative of the ball integral radius function on the whole radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeIdentification (n : ℕ) : BallIntegralRadiusDerivativeIdentification n

Unrestricted radius-weighted identities imply the same derivative identification, by forgetting the restriction on test weights.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeRepresentationForWeights_of_weightedRepresentation_identified {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentationForWeights n) : BallIntegralRadiusDerivativeRepresentationForWeights n

After the derivative-identification theorem is proved, a restricted weighted radial representation alone gives the combined radial-density representation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormulaForWeights_of_weightedRepresentation_identified {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentationForWeights n) : BallIntegralRadiusDerivativeFormulaForWeights n

After the derivative-identification theorem is proved, a restricted weighted radial representation alone gives the packaged radius-derivative formula.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeRepresentation_of_weightedRepresentation_identified {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentation n) : BallIntegralRadiusDerivativeRepresentation n

After the unrestricted derivative-identification theorem is proved, an unrestricted weighted radial representation alone gives the combined radial-density representation.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusDerivativeFormula_of_weightedRepresentation_identified {n : ℕ} (hweighted : BallIntegralRadiusWeightedRepresentation n) : BallIntegralRadiusDerivativeFormula n

After the unrestricted derivative-identification theorem is proved, an unrestricted weighted radial representation alone gives the packaged radius-derivative formula.