Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(measure): prove Haar measure = Lebesgue measure on R (#8639)
- Loading branch information
1 parent
8e50863
commit 462359d
Showing
1 changed file
with
37 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,37 @@ | ||
/- | ||
Copyright (c) 2021 Floris van Doorn. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Floris van Doorn | ||
-/ | ||
import measure_theory.measure.lebesgue | ||
import measure_theory.measure.haar | ||
|
||
/-! | ||
# Relationship between the Haar and Lebesgue measures | ||
We prove that the Haar measure and Lebesgue measure are equal on `ℝ`. | ||
-/ | ||
|
||
open topological_space set | ||
|
||
/-- The interval `[0,1]` as a compact set with non-empty interior. -/ | ||
def topological_space.positive_compacts.Icc01 : positive_compacts ℝ := | ||
⟨Icc 0 1, is_compact_Icc, by simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one]⟩ | ||
|
||
namespace measure_theory | ||
|
||
open measure topological_space.positive_compacts | ||
|
||
lemma is_add_left_invariant_real_volume : is_add_left_invariant ⇑(volume : measure ℝ) := | ||
by simp [← map_add_left_eq_self, real.map_volume_add_left] | ||
|
||
/-- The Haar measure equals the Lebesgue measure on `ℝ`. -/ | ||
lemma haar_measure_eq_lebesgue_measure : add_haar_measure Icc01 = volume := | ||
begin | ||
convert (add_haar_measure_unique _ Icc01).symm, | ||
{ simp [Icc01] }, | ||
{ apply_instance }, | ||
{ exact is_add_left_invariant_real_volume } | ||
end | ||
|
||
end measure_theory |