Densities of weight w, and why one construction covers three domains

Start with the concrete case. A probability density p on a line is integrated against a length to give a probability, a pure number, so p carries Length⁻¹: the density's unit is the reciprocal of the unit its argument is measured in. Change the length unit and the density's numerical values change with it.

Generalizing the exponent is the whole construction. A space with measure unit μ induces, for each rational weight w, a space of densities of weight w carrying unit μ^(-w). The density above is the case w = 1. Fixing other values of w recovers things usually treated as unrelated:

w	what it is	domain
0	ordinary scalar functions	–
1/2	half-densities (see below)	quantum mechanics
1	probability densities	statistics
-1	the measure itself	–

A half-density is a density of weight 1/2, the square root of a density: the object whose square integrates to a number, which is what a quantum mechanical wavefunction is, since ∫|ψ|² dx = 1.

The sections that follow are connections to particular domains. They are independent of each other and of the definitions below, and a reader who wants only the construction can skip to it.

An aside on the half-density case

The normalization condition ∫|ψ|² dx = 1 gives a wavefunction the unit of a half-density, whose square is a weight-1 density (modulus_sq_of_half). Geometric quantization, a construction in mathematical physics with different motives, arrives at the same half-densities.

What this buys in statistics

Because log requires an argument at unit 1, log p for a probability density p over a measure whose unit is not 1 fails to typecheck (density_ne_triv). That is the base-measure problem: a density only means something relative to the measure it was taken against, and representing a distribution by its density silently discards that measure. Radul and Alexeev (arXiv:2010.09647) identify exactly this failure in probabilistic programming systems, and solve it by library convention: standardizing on Hausdorff measure and tracking corrections in a Bijector architecture. Here it is a type error instead, and the checker does the tracking.

The classical consequence falls straight out. Differential entropy, -∫ p log p, the continuous analogue of Shannon entropy, is ill-typed. The Kullback–Leibler divergence ∫ p log(p/q), which measures how far one distribution sits from another, is fine, because a ratio of equal-weight densities has weight 0. The well-known fact that differential entropy is not invariant under a change of units while relative entropy is becomes a distinction the checker enforces rather than one you are expected to remember.

What this buys in general relativity

A metric is a map V ⊸ dual V ⊗ d, so its entries carry d/(δᵢδⱼ) and lowering an index lands in the dual space scaled by d. The invariant volume element then works out to d^(n/2), independent of the coordinate units, as it must be.

Note the exponent. Rational weights are not a convenience here: w = 1/2 for wavefunctions and n/2 for volume elements in odd dimension both require them, as volatility at Time^(-1/2) does (LambdaS.Uom).

def LambdaS.Density {B : Type u_1} (μ : Uom B) (w : ℚ) (I : Type u_3) : Space B I

The space of densities of weight w over an index type I whose measure carries unit μ. Uniform, as densities are.

Equations

• LambdaS.Density μ w I x✝ = μ ^ (-w)

@[simp]

theorem LambdaS.density_apply {B : Type u_1} {I : Type u_2} (μ : Uom B) (w : ℚ) (i : I) : Density μ w I i = μ ^ (-w)

theorem LambdaS.density_zero {B : Type u_1} {I : Type u_2} (μ : Uom B) : Density μ 0 I = Space.triv B I

Weight 0 has unit 1, so log accepts its quantities. If μ ≠ 1, density_ne_triv excludes every nonzero weight; if μ = 1, every weight has unit 1.

theorem LambdaS.density_mul {B : Type u_1} {I : Type u_2} (μ : Uom B) (w₁ w₂ : ℚ) (i : I) : Density μ w₁ I i * Density μ w₂ I i = Density μ (w₁ + w₂) I i

Weights add under multiplication of densities.

theorem LambdaS.modulus_sq_of_half {B : Type u_1} {I : Type u_2} (μ : Uom B) (i : I) : Density μ (1 / 2) I i * Density μ (1 / 2) I i = Density μ 1 I i

Squaring the unit of a half-density gives the unit of a weight-1 density. This is the unit identity used when interpreting |ψ|² as a probability density; it does not define an integration operation or prove normalization.

theorem LambdaS.integrate_weight_one {B : Type u_1} {I : Type u_2} (μ : Uom B) (i : I) : Density μ 1 I i * μ = 1

A weight-1 density multiplied by its measure has unit 1. This identity supports the interpretation as integration; the artifact defines no integration operator.

theorem LambdaS.ratio_weight_zero {B : Type u_1} {I : Type u_2} (μ : Uom B) (w : ℚ) (i : I) : Density μ w I i / Density μ w I i = Density μ 0 I i

The ratio of two densities of equal weight is dimensionless, whatever that weight is.

This is the whole KL-versus-entropy distinction: log (p/q) typechecks because the ratio has unit 1. In contrast, log p is rejected when the weight is nonzero and the measure unit is not 1.

theorem LambdaS.density_ne_triv {B : Type u_1} {I : Type u_2} (μ : Uom B) {w : ℚ} (hw : w ≠ 0) (i : I) {b : B} (hμ : μ.exp b ≠ 0) : Density μ w I i ≠ Space.triv B I i

A density of nonzero weight does not have unit 1 when the measure unit has a nonzero exponent. This is the statement that log p genuinely fails: the failure is not an artifact of how the weight is written.

General relativity, on the same machinery

theorem LambdaS.metric_entry {B : Type u_1} {I : Type u_2} (V : Space B I) (d : Uom B) (j i : I) : entry V (V.dual ⊗ d) j i = d / (V j * V i)

A metric is a map V ⊸ dual V ⊗ d, where d is the unit of the invariant interval. Its entries carry d / (δⱼ δᵢ), symmetric in the two indices, as a metric must be, and dimensionally consistent with gᵢⱼxⁱxʲ having unit d.

theorem LambdaS.lower_index {B : Type u_1} {I : Type u_2} (V : Space B I) (d : Uom B) (i : I) : (V.dual ⊗ d) i = d / V i

Lowering an index lands in the dual scaled by d. In coordinates, xⁱ carries δᵢ and xᵢ carries d / δᵢ.

theorem LambdaS.interval_unit {B : Type u_1} {I : Type u_2} (V : Space B I) (d : Uom B) (j i : I) : V j * entry V (V.dual ⊗ d) j i * V i = d

The interval carries unit d. Each term xʲ gⱼᵢ xⁱ of the double contraction lands at d, whatever units the coordinates carry.