Native Hausdorff density

Abstract

Native Hausdorff three-measure and its coordinate density.

Coordinates3 is UpperHalfSpace over Complex: the positive-height subtype of the Euclidean space WithLp 2 (Complex times Real). Native3 is HyperbolicThreeSpace. If D is Euclidean coordinate distance and hx, hy are the two positive heights, native distance is 2 arsinh(D/(2 sqrt(hx hy))). Both spaces have their Borel measurable structures; in the formulas, borel and BorelSpace denote this choice and its compatibility with the topology.

$C oor d ina t es 3 = UpperHalfSpace (C o m pl e x)$

$N a t i v e 3 = Hy p er b o l i c T h ree Sp a ce$

$measurableSpace (C oor d ina t es 3) = borel (C oor d ina t es 3)$

$BorelSpace (C oor d ina t es 3)$

$measurableSpace (N a t i v e 3) = borel (N a t i v e 3)$

$BorelSpace (N a t i v e 3)$

coordinatesEquiv is the measurable equivalence underlying the coordinate homeomorphism. It sends a native point to its coordinates, and its inverse is the constructor mk.

$coor d ina t es Eq u i v = toMeasurableEquiv (coordinatesHomeomorph (C o m pl e x))$

$\forall z \in N a t i v e 3, coordinatesEquiv (z) = coordinates (z)$

$\forall s \in Set (C oor d ina t es 3), preimage (coor d ina t es Eq u i v, s) = image (mk, s)$

The two raw measures are Mathlib’s unnormalized Hausdorff three-measures on their respective metric spaces. heightDensity takes values in the extended nonnegative reals; ofReal is the canonical map from real numbers to that space.

$r a wC oor d ina t e M e a s u re = hausdorffMeasure (3, C oor d ina t es 3)$

$r a wN a t i v e M e a s u re = hausdorffMeasure (3, N a t i v e 3)$

$\forall x \in C oor d ina t es 3, heightDensity (x) = ofReal (inv (height (x))^{3})$

Theorem 1.1 (Raw Hausdorff density identity).

$map (r a wN a t i v e M e a s u re, coor d ina t es Eq u i v) = withDensity (r a wC oor d ina t e M e a s u re, h e i g h t De n s i t y)$

Proof. Machine-checked in Lean as D5/S3/Geometry/HyperbolicNormalizedDensity.raw_native_density (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here map denotes measure pushforward, and withDensity denotes multiplication of a measure by a nonnegative measurable density through the lower integral. The equality has no hypotheses and is an equality of measures, including sets with zero or infinite measure. The two sides use the original native and coordinate metrics. The argument combines local metric distortion, pointwise height bounds, countable additivity and an extended-real limit.

For a positive radius below the height of its centre, local Hausdorff comparison and the preimage identity above give the following bounds on each Borel subset of the coordinate ball. Every ball in this exposition uses the Euclidean coordinate metric.

$\forall p \in C oor d ina t es 3, \forall r \in R e a l, (0 < r \land r < height (p)) \Rightarrow (\forall s \in Set (C oor d ina t es 3), (MeasurableSet (s) \land s \subseteq ball (p, r)) \Rightarrow (mass (r a wC oor d ina t e M e a s u re, s) \leq ofReal (height (p) + 2 \cdot r)^{3} \cdot mass (map (r a wN a t i v e M e a s u re, coor d ina t es Eq u i v), s) \land mass (map (r a wN a t i v e M e a s u re, coor d ina t es Eq u i v), s) \leq ofReal (inv (height (p) - r))^{3} \cdot mass (r a wC oor d ina t e M e a s u re, s)))$

Define the distortion factor for real epsilon by the formula below. For zero less than epsilon less than one, pointwise bounds on height over a ball of radius epsilon times the centre height bound the density from above and below. Combining these bounds with local Hausdorff comparison yields the two inequalities with the same factor.

$\forall e p s i l o n \in R e a l, distortionFactor (e p s i l o n) = ofReal ((\frac{1 + 2 \cdot e p s i l o n}{1 - e p s i l o n})^{3})$

$\forall e p s i l o n \in R e a l, (0 < e p s i l o n \land e p s i l o n < 1) \Rightarrow (\forall p \in C oor d ina t es 3, \forall s \in Set (C oor d ina t es 3), (MeasurableSet (s) \land s \subseteq ball (p, e p s i l o n \cdot height (p))) \Rightarrow (mass (withDensity (r a wC oor d ina t e M e a s u re, h e i g h t De n s i t y), s) \leq distortionFactor (e p s i l o n) \cdot mass (map (r a wN a t i v e M e a s u re, coor d ina t es Eq u i v), s) \land mass (map (r a wN a t i v e M e a s u re, coor d ina t es Eq u i v), s) \leq distortionFactor (e p s i l o n) \cdot mass (withDensity (r a wC oor d ina t e M e a s u re, h e i g h t De n s i t y), s)))$

These balls cover Coordinates3. A Lindelof countable subcover can be disjointified into Borel pieces Dn. For a Borel set s, the sets s intersect Dn form a countable measurable partition of s. Applying the local estimates to each piece and summing in the extended nonnegative reals gives the global bounds.

$\forall e p s i l o n \in R e a l, (0 < e p s i l o n \land e p s i l o n < 1) \Rightarrow (\forall s \in Set (C oor d ina t es 3), MeasurableSet (s) \Rightarrow (mass (withDensity (r a wC oor d ina t e M e a s u re, h e i g h t De n s i t y), s) \leq distortionFactor (e p s i l o n) \cdot mass (map (r a wN a t i v e M e a s u re, coor d ina t es Eq u i v), s) \land mass (map (r a wN a t i v e M e a s u re, coor d ina t es Eq u i v), s) \leq distortionFactor (e p s i l o n) \cdot mass (withDensity (r a wC oor d ina t e M e a s u re, h e i g h t De n s i t y), s)))$

Take epsilon(n)=1/(n+2) for natural n. The distortion factors tend to one. For every fixed extended nonnegative real b, their products with b tend to b: multiplication is continuous at the nonzero limiting factor even if b is infinite. Closedness of the order relation therefore turns the two global inequalities into equality on every Borel set, which determines equality of measures.

An application is the usual Euclidean volume normalization. In the same L2 ambient space A, let Q be the parallelepiped of the standard real orthonormal basis, c3 its raw Hausdorff three-mass, j the coordinate subtype inclusion, and coordinateHaar the pullback of canonical ambient volume along j.

$A = WithLp (2, Product (C o m pl e x, R e a l))$

$Q = parallelepiped (toBasis (stdOrthonormalBasis (R e a l, A)))$

$c 3 = mass (hausdorffMeasure (3, A), Q)$

$j = s u b t y p e Va l$

$coor d ina t eH aa r = comap (volume (A), j)$

The real dimension of A is three. Its raw Hausdorff measure is an additive Haar measure. Haar uniqueness and orthonormal-cube calibration identify it with c3 times canonical volume. The cube has nonempty interior and is compact, so c3 is strictly positive and finite. The inclusion j is isometric and an open measurable embedding, giving the coordinate calibration below.

$0 < c 3 \land c 3 < \infty$

$hausdorffMeasure (3, A) = smul (c 3, volume (A))$

$r a wC oor d ina t e M e a s u re = smul (c 3, coor d ina t eH aa r)$

Substituting this calibration into the raw identity and cancelling c3 once gives the normalized formula. No set mass is divided out, and no sup-norm Hausdorff measure is substituted for the L2 measure.

$map (smul (inv (c 3), r a wN a t i v e M e a s u re), coor d ina t es Eq u i v) = withDensity (coor d ina t eH aa r, h e i g h t De n s i t y)$

Natural-dimension application of the same local-distortion and squeeze argument. For every natural d, let Hcoord_d and Hnative_d be raw Hausdorff d-measure in the unchanged Euclidean coordinate and native H3 metrics. Then map(Hnative_d,coordinatesEquiv)=withDensity(Hcoord_d,x |-> ofReal(height(x)^(-d))). In the local Hausdorff image inequalities, use the original ball_distortion with powers d; on a ball of radius epsilonheight(p), the common density distortion factor is ((1+2epsilon)/(1-epsilon))^d. The same countable Borel partition and extended-real squeeze prove the equality, including d=0 and sets of infinite measure.

For d=2 this identifies the native H3 surface-dimension measure with height^(-2) times ambient Euclidean-coordinate Hausdorff two-measure. Ambient three-dimensional Hausdorff two-measure is not assumed sigma-finite: the argument evaluates withDensity only on Borel sets, uses countable additivity with values in the extended nonnegative reals, and cancels only finite positive local distortion scalars. This application does not replace that coordinate two-measure by three-dimensional volume. For normalized Hausdorff measure use Mathlib euclideanHausdorffMeasure d: it multiplies raw Hausdorff d-measure by a scalar depending only on d. Multiplying both sides by this same scalar gives the normalized density identity in every natural dimension, independently of c3.

For dimension two, let U be the Euclidean subtype {z in Complex : Im(z)>0}, j(z)=(Re(z),0,Im(z)) in the original L2 coordinate half-space, and V the original vertical map from native H2 to native H3. The map from H2 to U retaining the same point is a homeomorphism; j is a Euclidean isometric measurable embedding with relatively closed image, while V is an isometry for the original hyperbolic metrics. They obey mk(j(z))=V(z). Mathlib InnerProductSpace.euclideanHausdorffMeasure_eq_volume independently calibrates normalized Hausdorff two-measure on Complex as its canonical volume. Restrict the normalized ambient density identity to j(U), then use Isometry.map_euclideanHausdorffMeasure and MeasurePreserving.setLIntegral_comp_emb to transport its height^(-2) integral. This gives normalized native H2 Hausdorff two-measure equal to Mathlib UpperHalfPlane.volume, namely dxdy/y^2. No ambient H3 Hausdorff two-measure sigma-finiteness is required.

Consequently every isometry e from the original H2 into the original H3 satisfies map(volume_H2,e)=restrict(normalizedHausdorff2_H3,range(e)). In particular normalizedHausdorff2_H3(e(A))=volume_H2(A) for every subset A, with zero and infinite values included. The map need not be onto ambient H3. For the supporting_plane_isometry realization, range(e) is the entire original Lorentz plane. This supplies the surface measure of that actual plane; a coordinate chart still needs its own derivative and substitution formula.

The density identity concerns measures on the whole upper half-space. It gives no Gram-map Jacobian, frame-independence statement, finite positive mass for a specified geometric body, Schlaefli variation formula or strictly positive flat-boundary limit.

References

Truth anchor: D5/S3/Geometry/HyperbolicNormalizedDensity.raw_native_density
Dependency: D5/S3/Geometry/HyperbolicHausdorffComparison
Dependency: D5/S3/Geometry/HyperbolicTopology

Keyboard shortcuts

trureturing — Discovering truth

Native Hausdorff density

Abstract

References