# mathlibdocumentation

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:

• map_linear_map_add_haar_eq_smul_add_haar: a linear map rescales the Haar measure by the absolute value of its determinant.
• add_haar_smul : the measure of r • s is |r| ^ dim * μ s.
• add_haar_ball: the measure of ball x r is r ^ dim * μ (ball 0 1).
• add_haar_closed_ball: the measure of closed_ball x r is r ^ dim * μ (ball 0 1).
• add_haar_sphere: spheres have zero measure.

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 ℝ^ι. #

The Haar measure equals the Lebesgue measure on ℝ.

The Haar measure equals the Lebesgue measure on ℝ^ι.

@[instance]

### 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.

theorem measure_theory.measure.map_linear_map_add_haar_pi_eq_smul_add_haar {ι : Type u_1} [fintype ι] {f : (ι → ) →ₗ[] ι → } (hf : 0) (μ : measure_theory.measure (ι → ))  :
@[simp]
theorem measure_theory.measure.haar_preimage_linear_map {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) {f : E →ₗ[] E} (hf : 0) (s : set E) :
μ (f ⁻¹' s) = * μ s

### Basic properties of Haar measures on real vector spaces #

theorem measure_theory.measure.map_add_haar_smul {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) {r : } (hr : r 0) :
theorem measure_theory.measure.add_haar_preimage_smul {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) {r : } (hr : r 0) (s : set E) :
μ ⁻¹' s) = * μ s
theorem measure_theory.measure.add_haar_smul {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) (r : ) (s : set E) :
μ (r s) = * μ s

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_center {E : Type u_1} [normed_group E] [borel_space E] (μ : measure_theory.measure E) (x : E) (r : ) :
μ r) = μ r)
theorem measure_theory.measure.add_haar_closed_ball_center {E : Type u_1} [normed_group E] [borel_space E] (μ : measure_theory.measure E) (x : E) (r : ) :
μ r) = μ r)
theorem measure_theory.measure.add_haar_ball_lt_top {E : Type u_1} [normed_group E] [proper_space E] (μ : measure_theory.measure E) (x : E) (r : ) :
μ r) <
theorem measure_theory.measure.add_haar_ball_pos {E : Type u_1} [normed_group E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 < r) :
0 < μ r)
theorem measure_theory.measure.add_haar_closed_ball_pos {E : Type u_1} [normed_group E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 < r) :
0 < μ r)
theorem measure_theory.measure.add_haar_ball_of_pos {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 < r) :
μ r) = * μ 1)
theorem measure_theory.measure.add_haar_ball {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) [nontrivial E] (x : E) {r : } (hr : 0 r) :
μ r) = * μ 1)
theorem measure_theory.measure.add_haar_closed_ball' {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 r) :
μ r) = * μ 1)

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.

theorem measure_theory.measure.add_haar_closed_ball {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : 0 r) :
μ r) = * μ 1)
theorem measure_theory.measure.add_haar_sphere_of_ne_zero {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) (x : E) {r : } (hr : r 0) :
μ r) = 0
theorem measure_theory.measure.add_haar_sphere {E : Type u_1} [normed_group E] [ E] [borel_space E] (μ : measure_theory.measure E) [nontrivial E] (x : E) (r : ) :
μ r) = 0