Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor(measure_theory/group/basic): rename and split (#11952)
* Rename `measure_theory/group/basic` -> `measure_theory/group/measure`. It was not the bottom file in this folder in the import hierarchy (arithmetic is below it). * Split off some results to `measure_theory/group/integration`. This reduces imports in some files, and makes the organization more clear. Furthermore, I will add some integrability results and more integrals in a follow-up PR. * Prove a general instance `pi.is_mul_left_invariant` * Remove lemmas specifically about `volume` on `real` in favor on the general lemmas. ```lean real.map_volume_add_left -> map_add_left_eq_self real.map_volume_pi_add_left -> map_add_left_eq_self real.volume_preimage_add_left -> measure_preimage_add real.volume_pi_preimage_add_left -> measure_preimage_add real.map_volume_add_right -> map_add_right_eq_self real.volume_preimage_add_right -> measure_preimage_add_right ```
- Loading branch information
1 parent
60d3233
commit 822244f
Showing
13 changed files
with
156 additions
and
130 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
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
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
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
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,108 @@ | ||
/- | ||
Copyright (c) 2022 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.integral.bochner | ||
import measure_theory.group.measure | ||
|
||
/-! | ||
# Integration on Groups | ||
We develop properties of integrals with a group as domain. | ||
This file contains properties about integrability, Lebesgue integration and Bochner integration. | ||
-/ | ||
|
||
namespace measure_theory | ||
|
||
open measure topological_space | ||
open_locale ennreal | ||
|
||
variables {𝕜 G E : Type*} [measurable_space G] {μ : measure G} | ||
variables [normed_group E] [second_countable_topology E] [normed_space ℝ E] [complete_space E] | ||
[measurable_space E] [borel_space E] | ||
|
||
section measurable_mul | ||
|
||
variables [group G] [has_measurable_mul G] | ||
|
||
/-- Translating a function by left-multiplication does not change its `lintegral` with respect to | ||
a left-invariant measure. -/ | ||
@[to_additive] | ||
lemma lintegral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → ℝ≥0∞) (g : G) : | ||
∫⁻ x, f (g * x) ∂μ = ∫⁻ x, f x ∂μ := | ||
begin | ||
convert (lintegral_map_equiv f $ measurable_equiv.mul_left g).symm, | ||
simp [map_mul_left_eq_self μ g] | ||
end | ||
|
||
/-- Translating a function by right-multiplication does not change its `lintegral` with respect to | ||
a right-invariant measure. -/ | ||
@[to_additive] | ||
lemma lintegral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → ℝ≥0∞) (g : G) : | ||
∫⁻ x, f (x * g) ∂μ = ∫⁻ x, f x ∂μ := | ||
begin | ||
convert (lintegral_map_equiv f $ measurable_equiv.mul_right g).symm, | ||
simp [map_mul_right_eq_self μ g] | ||
end | ||
|
||
/-- Translating a function by left-multiplication does not change its integral with respect to a | ||
left-invariant measure. -/ | ||
@[to_additive] | ||
lemma integral_mul_left_eq_self [is_mul_left_invariant μ] (f : G → E) (g : G) : | ||
∫ x, f (g * x) ∂μ = ∫ x, f x ∂μ := | ||
begin | ||
have h_mul : measurable_embedding (λ x, g * x) := | ||
(measurable_equiv.mul_left g).measurable_embedding, | ||
rw [← h_mul.integral_map, map_mul_left_eq_self] | ||
end | ||
|
||
/-- Translating a function by right-multiplication does not change its integral with respect to a | ||
right-invariant measure. -/ | ||
@[to_additive] | ||
lemma integral_mul_right_eq_self [is_mul_right_invariant μ] (f : G → E) (g : G) : | ||
∫ x, f (x * g) ∂μ = ∫ x, f x ∂μ := | ||
begin | ||
have h_mul : measurable_embedding (λ x, x * g) := | ||
(measurable_equiv.mul_right g).measurable_embedding, | ||
rw [← h_mul.integral_map, map_mul_right_eq_self] | ||
end | ||
|
||
/-- If some left-translate of a function negates it, then the integral of the function with respect | ||
to a left-invariant measure is 0. -/ | ||
@[to_additive] | ||
lemma integral_zero_of_mul_left_eq_neg [is_mul_left_invariant μ] {f : G → E} {g : G} | ||
(hf' : ∀ x, f (g * x) = - f x) : | ||
∫ x, f x ∂μ = 0 := | ||
by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self] | ||
|
||
/-- If some right-translate of a function negates it, then the integral of the function with respect | ||
to a right-invariant measure is 0. -/ | ||
@[to_additive] | ||
lemma integral_zero_of_mul_right_eq_neg [is_mul_right_invariant μ] {f : G → E} {g : G} | ||
(hf' : ∀ x, f (x * g) = - f x) : | ||
∫ x, f x ∂μ = 0 := | ||
by simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self] | ||
|
||
end measurable_mul | ||
|
||
|
||
section topological_group | ||
|
||
variables [topological_space G] [group G] [topological_group G] [borel_space G] | ||
[is_mul_left_invariant μ] | ||
|
||
/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function | ||
`f` is 0 iff `f` is 0. -/ | ||
@[to_additive] | ||
lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (hμ : μ ≠ 0) | ||
{f : G → ℝ≥0∞} (hf : continuous f) : | ||
∫⁻ x, f x ∂μ = 0 ↔ f = 0 := | ||
begin | ||
haveI := is_open_pos_measure_of_mul_left_invariant_of_regular hμ, | ||
rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero] | ||
end | ||
|
||
end topological_group | ||
|
||
end measure_theory |
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
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
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
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
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
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
Oops, something went wrong.