Weighted radial representation

This module upgrades the simple-function radial Radon-Nikodym representation to the measurable, essentially bounded radius weights used by the weak monotonicity argument.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ae_eq_comp_norm_on_ball_of_ae_eq_radius {n : ℕ} [NeZero n] {R0 : ℝ} {c d : ℝ → ℝ} (hcd : c =ᵐ[radiusIntervalMeasure R0] d) : (fun (x : Domain n) => c ‖x‖) =ᵐ[MeasureTheory.volume.restrict (Metric.ball 0 R0)] fun (x : Domain n) => d ‖x‖

An a.e. identity on the radius interval pulls back through the radius map to an a.e. identity on the Euclidean ball.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialRNDensity_radiusWeight_integral_eq {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} {c : ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hc : RadiusWeightOn R0 c) : ∫ (x : Domain n) in Metric.ball 0 R0, c ‖x‖ * f x = ∫ (rho : ℝ) in Set.Ioo 0 R0, c rho * radialRNDensity f R0 rho

The radial Radon-Nikodym density represents integration against every a.e. measurable and a.e. bounded radius weight.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ballIntegralRadiusWeightedRepresentationForWeights_euclidean (n : ℕ) : BallIntegralRadiusWeightedRepresentationForWeights n

Euclidean radial pushforward/coarea theorem for all radius weights needed in the weak monotonicity argument.