Radial Measure

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusIntervalMeasure (R0 : ℝ) : MeasureTheory.Measure ℝ

The one-dimensional measure on the radius interval (0, R0).

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusIntervalMeasure R0 = MeasureTheory.volume.restrict (Set.Ioo 0 R0)

instance LeanStationaryHarmonicMaps.StationaryHarmonicMap.sigmaFinite_radiusIntervalMeasure (R0 : ℝ) : MeasureTheory.SigmaFinite (radiusIntervalMeasure R0)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.normPushforwardVolume_absolutelyContinuous (n : ℕ) [NeZero n] : (MeasureTheory.Measure.map (fun (x : Domain n) => ‖x‖) MeasureTheory.volume).AbsolutelyContinuous MeasureTheory.volume

The pushforward of Euclidean volume by the radius map is absolutely continuous with respect to one-dimensional Lebesgue measure. This is the measure-theoretic core supplied by HaarToSphere, kept separate from the later Sobolev/radial-density bookkeeping.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusPushforward_absolutelyContinuous_euclidean {n : ℕ} [NeZero n] {R0 : ℝ} : (MeasureTheory.Measure.map (fun (x : Domain n) => ‖x‖) (MeasureTheory.volume.restrict (Metric.ball 0 R0))).AbsolutelyContinuous (radiusIntervalMeasure R0)

Radius pushforward on a fixed ball is absolutely continuous with respect to the restricted radius-interval measure. The only point lost when restricting to (0, R0) is the origin, a null set in positive dimension.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorMeasure_absolutelyContinuous_euclidean {n : ℕ} [NeZero n] {f : Domain n → ℝ} {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‖).AbsolutelyContinuous (radiusIntervalMeasure R0).toENNRealVectorMeasure

The radial signed pushforward of an L¹ scalar density on a ball is absolutely continuous with respect to the one-dimensional radius interval measure.

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

The Radon-Nikodym density of the radial signed pushforward of f dx on B_R0, with respect to the radius interval measure.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorMeasure_withDensity_rnDeriv_euclidean {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : (radiusIntervalMeasure R0).withDensityᵥ (radialRNDensity f R0) = ((MeasureTheory.volume.restrict (Metric.ball 0 R0)).withDensityᵥ f).map fun (x : Domain n) => ‖x‖

The radial signed pushforward is exactly the vector measure obtained by integrating its Radon-Nikodym density on the radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialRNDensity_setIntegral_eq_radialVectorMeasure {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} {s : Set ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hs : MeasurableSet s) : ∫ (rho : ℝ) in s, radialRNDensity f R0 rho ∂radiusIntervalMeasure R0 = ∫ (x : Domain n) in {x : Domain n | ‖x‖ ∈ s}, f x ∂MeasureTheory.volume.restrict (Metric.ball 0 R0)

The radial Radon-Nikodym density represents the signed radial pushforward on every measurable set of radii.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialRNDensity_indicatorConst_integral_eq {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 k : ℝ} {s : Set ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hs : MeasurableSet s) : ∫ (x : Domain n) in Metric.ball 0 R0, s.indicator (fun (x : ℝ) => k) ‖x‖ * f x = ∫ (rho : ℝ), s.indicator (fun (x : ℝ) => k) rho * radialRNDensity f R0 rho ∂radiusIntervalMeasure R0

The radial Radon-Nikodym density represents constant multiples of measurable radial indicators. This is the atomic step for passing from the set-level representation to finite simple radial weights.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialRNDensity_simpleFunc_integral_eq {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} (g : MeasureTheory.SimpleFunc ℝ ℝ) (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) : ∫ (x : Domain n) in Metric.ball 0 R0, g ‖x‖ * f x = ∫ (rho : ℝ), g rho * radialRNDensity f R0 rho ∂radiusIntervalMeasure R0

The radial Radon-Nikodym density represents every finite simple radial weight. This is the finite-step version of the desired weighted representation.

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

Set-integral version of radialRNDensity_simpleFunc_integral_eq, with the radius interval written explicitly.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialRNDensity_locallyIntegrableOn {n : ℕ} {f : Domain n → ℝ} {R0 : ℝ} : MeasureTheory.LocallyIntegrableOn (radialRNDensity f R0) (Set.Ioo 0 R0) MeasureTheory.volume

The radial Radon-Nikodym density is locally integrable on the open radius interval.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ae_ne_zero_on_ball {n : ℕ} [NeZero n] {R0 : ℝ} : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), x ≠ 0

In positive dimension, the origin is negligible even after restricting Lebesgue measure to a ball.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ae_norm_mem_Ioo_zero_radius_on_ball {n : ℕ} [NeZero n] {R0 : ℝ} (_hR0_pos : 0 < R0) : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖x‖ ∈ Set.Ioo 0 R0

In positive dimension and positive radius, points in the ball have radius in (0, R0) almost everywhere.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.measure_norm_eq_zero {n : ℕ} [NeZero n] {r : ℝ} : MeasureTheory.volume {x : Domain n | ‖x‖ = r} = 0

Each fixed radius sphere has zero Lebesgue measure in positive dimension.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.measure_norm_mem_countable_zero {n : ℕ} [NeZero n] {s : Set ℝ} (hs : s.Countable) : MeasureTheory.volume {x : Domain n | ‖x‖ ∈ s} = 0

The preimage under the radius map of a countable set of radii is null.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ae_norm_not_mem_countable_on_ball {n : ℕ} [NeZero n] {R0 : ℝ} {s : Set ℝ} (hs : s.Countable) : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖x‖ ∉ s

The radius of a ball point avoids any countable set of radii almost everywhere.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.ae_norm_not_mem_finset_on_ball {n : ℕ} [NeZero n] {R0 : ℝ} (s : Finset ℝ) : ∀ᵐ (x : Domain n) ∂MeasureTheory.volume.restrict (Metric.ball 0 R0), ‖x‖ ∉ ↑s

The radius of a ball point avoids any finite set of radii almost everywhere.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.tendsto_radiusWeight_mul_pullback_ae_of_tendsto_on_Ioo {n : ℕ} [NeZero n] {f : Domain n → ℝ} {R0 : ℝ} {c : ℝ → ℝ} {cSeq : ℕ → ℝ → ℝ} (hR0_pos : 0 < R0) (hlim : ∀ rho ∈ Set.Ioo 0 R0, Filter.Tendsto (fun (N : ℕ) => cSeq N rho) Filter.atTop (nhds (c rho))) : ∀ᵐ (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))

Pointwise convergence of radius weights on (0, R0) pulls back to a.e. convergence of the corresponding spatial integrands on the ball.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.tendsto_radiusWeight_mul_ae_of_tendsto_on_Ioo {R0 : ℝ} {c D : ℝ → ℝ} {cSeq : ℕ → ℝ → ℝ} (hlim : ∀ rho ∈ Set.Ioo 0 R0, Filter.Tendsto (fun (N : ℕ) => cSeq N rho) Filter.atTop (nhds (c rho))) : ∀ᵐ (rho : ℝ) ∂radiusIntervalMeasure R0, Filter.Tendsto (fun (N : ℕ) => cSeq N rho * D rho) Filter.atTop (nhds (c rho * D rho))

Pointwise convergence of radius weights on (0, R0) gives a.e. convergence after multiplying by any fixed one-dimensional factor on the radius interval.