The inverse pow measure on Euclidean space

The measure ‖x‖^(- d) dx on EuclideanSpace ℝ (Fin d.succ), cancelling the radius contribution from the measure in spherical coordiantes.

The measures.

def Distribution.invPowMeasure {dm1 : ℕ} : MeasureTheory.Measure (EuclideanSpace ℝ (Fin dm1.succ))

The measure on EuclideanSpace ℝ (Fin 3) weighted by 1 / ‖x‖ ^ 2.

Equations

• Distribution.invPowMeasure = MeasureTheory.volume.withDensity fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ENNReal.ofReal (1 / ‖x‖ ^ dm1)

Integrals with respect to the measures.

theorem Distribution.integral_invPowMeasure {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) : ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), f x ∂invPowMeasure = ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), (1 / ‖x‖ ^ dm1) • f x

HasTemperateGrowth of measures

theorem Distribution.invPowMeasure_integrable_pow_neg_two {dm1 : ℕ} : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => (1 + ‖x‖) ^ (-(↑dm1 + 2))) invPowMeasure

instance Distribution.instHasTemperateGrowthEuclideanSpaceRealFinSuccInvPowMeasure (dm1 : ℕ) : invPowMeasure.HasTemperateGrowth