Orthogonal line coordinates and Lebesgue sections #
For a unit vector e in a finite-dimensional real inner product space, the coordinates
(y, t) ↦ y + t • e, with y ∈ (ℝ ∙ e)ᗮ, preserve product volume. Consequently the volume
of a Lebesgue-measurable set is the integral of the lengths of its parallel line sections.
Replacing a set by a volume-a.e. equal representative changes almost every section only
on a one-dimensional null set. This permits line-section arguments for measurable sets
without choosing a Borel representative permanently.
The length of a line section is independent of its base point along the line, in any real module.
Dually, the volume is the integral over heights t of the volumes of the hyperplane sections
{y ∈ (ℝ ∙ e)ᗮ | y + t • e ∈ s}, and restricting the heights to a Borel set gives the volume
of the corresponding part of the set. Hyperplane sections of bounded sets have finite volume,
and hyperplane sections through interior points have positive volume. The heights of interior
points form an open set, and a set has positive volume at any open set of heights containing the
height of an interior point.
Pairing the line integrals y ↦ ∫ f (y + t • e) dt with a bounded transverse weight ψ is an
integral of ψ (y) f (y + t • e) over product coordinates
(TauCeti.integral_mul_integral_line_eq), so this pairing is continuous for L¹ convergence on the
whole space (TauCeti.tendsto_integral_mul_integral_line).
More generally, for any subspace K, Tonelli's theorem splits Lebesgue integrals over E along
the orthogonal decomposition E = Kᗮ ⊕ K (Submodule.lintegral_eq_lintegral_lintegral_add),
via Mathlib's Submodule.measurePreserving_measurableEquivProd. In these coordinates based at a
point p, a product of sets has the product volume, every point x is recovered as the sum of
its two coordinates and p, and each coordinate moves no farther than x does.
The coordinate construction uses Mathlib's Submodule.orthogonalDecomposition and
LinearIsometryEquiv.toSpanUnitSingleton; its normalization follows Mathlib's volume
preservation for linear isometries and for the L² product.
Moving the base point along the direction does not change the length of a line section.
Orthogonal line coordinates preserve the product of transverse and longitudinal volumes.
Integrating an a.e. measurable nonnegative function along parallel lines gives an a.e. measurable function of the transverse coordinate.
Tonelli's theorem in orthogonal line coordinates.
If ∫⁻ g n → 0, then along a subsequence the integrals of g along almost every line
parallel to e tend to 0. Applied to g n = ‖f n - u‖ₑ, L¹ convergence of f n to u
gives L¹ convergence of their restrictions on almost every line, along a subsequence.
The pairing of the line integrals of f with a bounded transverse weight ψ is an
integral in orthogonal line coordinates.
Pairing line integrals with a bounded transverse weight is continuous for L¹ convergence on
the whole space.
Volume-a.e. equal sets have a.e. equal parallel sections for almost every transverse point. The exceptional transverse null set is allowed to depend on the direction.
Having interval sections up to null sets is independent of the ambient a.e. representative, for each fixed unit direction. The intervals may be empty or unbounded.
A Lebesgue-measurable set has Lebesgue-measurable sections on almost every parallel line.
The lengths of the parallel sections of a Lebesgue-measurable set form an a.e. measurable extended nonnegative function on the orthogonal subspace.
Cavalieri's formula for Lebesgue-measurable sets in orthogonal line coordinates, with extended nonnegative values and no finite-volume assumption.
Finite ambient volume implies finite length of almost every parallel section.
A Lebesgue-measurable set is null exactly when almost every parallel line section is null.
The hyperplane sections of a Borel set along a unit vector have measurable volume as a function of the height.
Cavalieri's formula along a unit vector: the volume of a Lebesgue-measurable set is the integral over heights of the volumes of its orthogonal hyperplane sections.
The hyperplane sections of a bounded set have finite volume.
The heights along a unit vector of the interior points of a set form an open set.
The hyperplane section along a unit vector through an interior point of a set has positive volume.
If an interior point of s lies at a height along e in the open set I, then s has
positive volume at heights in I.
Cavalieri's formula for the part of a Lebesgue-measurable set at heights in a Borel set I
along a unit vector e.
On the line through y parallel to e, the second-moment integrand of a set u is
‖y‖ ^ 2 + t ^ 2 on the section of u.
Tonelli's theorem along an orthogonal decomposition E = Kᗮ ⊕ K.
In orthogonal coordinates along a subspace, a product of sets has the product volume.
A point is recovered from its orthogonal coordinates along a subspace based at p.
If k - p ∈ V, both orthogonal coordinates of x along V based at p are at most as far
from those of k as x is from k.