mathlib documentation

measure_theory.measure.haar_lebesgue

Relationship between the Haar and Lebesgue measures #

We prove that the Haar measure and Lebesgue measure are equal on and on ℝ^ι, in measure_theory.add_haar_measure_eq_volume and measure_theory.add_haar_measure_eq_volume_pi.

We deduce basic properties of any Haar measure on a finite dimensional real vector space:

The interval [0,1] as a compact set with non-empty interior.

Equations

The set [0,1]^ι as a compact set with non-empty interior.

Equations

The Lebesgue measure is a Haar measure on and on ℝ^ι. #

Applying a linear map rescales Haar measure by the determinant #

We first prove this on ι → ℝ, using that this is already known for the product Lebesgue measure (thanks to matrices computations). Then, we extend this to any finite-dimensional real vector space by using a linear equiv with a space of the form ι → ℝ, and arguing that such a linear equiv maps Haar measure to Haar measure.

Basic properties of Haar measures on real vector spaces #

Rescaling a set by a factor r multiplies its measure by abs (r ^ dim).

We don't need to state map_add_haar_neg here, because it has already been proved for general Haar measures on general commutative groups.

Measure of balls #

theorem measure_theory.measure.add_haar_ball_pos {E : Type u_1} [normed_group E] [measurable_space E] (μ : measure_theory.measure E) [μ.is_add_haar_measure] (x : E) {r : } (hr : 0 < r) :
0 < μ (metric.ball x r)

The measure of a closed ball can be expressed in terms of the measure of the closed unit ball. Use instead add_haar_closed_ball, which uses the measure of the open unit ball as a standard form.