From 55b81f8b49e10d5f618be1263158999dfedccafa Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 21 Nov 2021 11:11:05 +0000 Subject: [PATCH] feat(measure_theory): measure preserving maps and integrals (#10326) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If `f` is a measure preserving map, then `∫ y, g y ∂ν = ∫ x, g (f x) ∂μ`. It was two rewrites with the old API (`hf.map_eq`, then a lemma about integral over map measure); it's one `rw` now. Also add versions for special cases when `f` is a measurable embedding (in this case we don't need to assume measurability of `g`). --- src/data/equiv/fin.lean | 13 ++ src/dynamics/ergodic/measure_preserving.lean | 18 ++ src/measure_theory/constructions/pi.lean | 203 ++++++------------ src/measure_theory/function/l1_space.lean | 10 + src/measure_theory/integral/bochner.lean | 5 + .../integral/integrable_on.lean | 10 + src/measure_theory/integral/lebesgue.lean | 29 +++ src/measure_theory/integral/set_integral.lean | 10 + src/measure_theory/measure/measure_space.lean | 2 + 9 files changed, 161 insertions(+), 139 deletions(-) diff --git a/src/data/equiv/fin.lean b/src/data/equiv/fin.lean index 7d09dc585f3ed..1d6f8bd4588c0 100644 --- a/src/data/equiv/fin.lean +++ b/src/data/equiv/fin.lean @@ -50,6 +50,19 @@ non-dependent version and `prod_equiv_pi_fin_two` for a version with inputs `α left_inv := λ f, funext $ fin.forall_fin_two.2 ⟨rfl, rfl⟩, right_inv := λ ⟨x, y⟩, rfl } +lemma fin.preimage_apply_01_prod {α : fin 2 → Type u} (s : set (α 0)) (t : set (α 1)) : + (λ f : Π i, α i, (f 0, f 1)) ⁻¹' (s.prod t) = + set.pi set.univ (fin.cons s $ fin.cons t fin.elim0) := +begin + ext f, + have : (fin.cons s (fin.cons t fin.elim0) : Π i, set (α i)) 1 = t := rfl, + simp [fin.forall_fin_two, this] +end + +lemma fin.preimage_apply_01_prod' {α : Type u} (s t : set α) : + (λ f : fin 2 → α, (f 0, f 1)) ⁻¹' (s.prod t) = set.pi set.univ ![s, t] := +fin.preimage_apply_01_prod s t + /-- A product space `α × β` is equivalent to the space `Π i : fin 2, γ i`, where `γ = fin.cons α (fin.cons β fin_zero_elim)`. See also `pi_fin_two_equiv` and `fin_two_arrow_equiv`. -/ diff --git a/src/dynamics/ergodic/measure_preserving.lean b/src/dynamics/ergodic/measure_preserving.lean index f493ce9c1f168..db9baf60918d3 100644 --- a/src/dynamics/ergodic/measure_preserving.lean +++ b/src/dynamics/ergodic/measure_preserving.lean @@ -42,6 +42,11 @@ structure measure_preserving (f : α → β) (μa : measure α . volume_tac) (measurable : measurable f) (map_eq : map f μa = μb) +protected lemma _root_.measurable.measure_preserving {f : α → β} + (h : measurable f) (μa : measure α) : + measure_preserving f μa (map f μa) := +⟨h, rfl⟩ + namespace measure_preserving protected lemma id (μ : measure α) : measure_preserving id μ μ := @@ -52,6 +57,19 @@ lemma symm {e : α ≃ᵐ β} {μa : measure α} {μb : measure β} (h : measure ⟨e.symm.measurable, by rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]⟩ +lemma restrict_preimage {f : α → β} (hf : measure_preserving f μa μb) {s : set β} + (hs : measurable_set s) : measure_preserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) := +⟨hf.measurable, by rw [← hf.map_eq, restrict_map hf.measurable hs]⟩ + +lemma restrict_preimage_emb {f : α → β} (hf : measure_preserving f μa μb) + (h₂ : measurable_embedding f) (s : set β) : + measure_preserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) := +⟨hf.measurable, by rw [← hf.map_eq, h₂.restrict_map]⟩ + +lemma restrict_image_emb {f : α → β} (hf : measure_preserving f μa μb) (h₂ : measurable_embedding f) + (s : set α) : measure_preserving f (μa.restrict s) (μb.restrict (f '' s)) := +by simpa only [preimage_image_eq _ h₂.injective] using hf.restrict_preimage_emb h₂ (f '' s) + protected lemma quasi_measure_preserving {f : α → β} (hf : measure_preserving f μa μb) : quasi_measure_preserving f μa μb := ⟨hf.1, hf.2.absolutely_continuous⟩ diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean index fcd29e3840ae4..c420e31ebe12d 100644 --- a/src/measure_theory/constructions/pi.lean +++ b/src/measure_theory/constructions/pi.lean @@ -54,6 +54,8 @@ noncomputable theory open function set measure_theory.outer_measure filter measurable_space encodable open_locale classical big_operators topological_space ennreal +universes u v + variables {ι ι' : Type*} {α : ι → Type*} /-! We start with some measurability properties -/ @@ -364,21 +366,6 @@ lemma pi_closed_ball [∀ i, metric_space (α i)] (x : Π i, α i) {r : ℝ} measure.pi μ (metric.closed_ball x r) = ∏ i, μ i (metric.closed_ball (x i) r) := by rw [closed_ball_pi _ hr, pi_pi] -lemma pi_unique_eq_map {β : Type*} {m : measurable_space β} (μ : measure β) (α : Type*) [unique α] : - measure.pi (λ a : α, μ) = map (measurable_equiv.fun_unique α β).symm μ := -begin - set e := measurable_equiv.fun_unique α β, - have : pi_premeasure (λ _ : α, μ.to_outer_measure) = map e.symm μ, - { ext1 s, - rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply], - congr' 1, exact e.to_equiv.image_eq_preimage s }, - simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure], -end - -lemma map_fun_unique {α β : Type*} [unique α] {m : measurable_space β} (μ : measure β) : - map (measurable_equiv.fun_unique α β) (measure.pi $ λ _, μ) = μ := -(measurable_equiv.fun_unique α β).map_apply_eq_iff_map_symm_apply_eq.2 (pi_unique_eq_map μ _).symm - instance pi.sigma_finite : sigma_finite (measure.pi μ) := (finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in)).sigma_finite @@ -392,36 +379,6 @@ begin exact is_empty_elim end -lemma {u} pi_fin_two_eq_map {α : fin 2 → Type u} {m : Π i, measurable_space (α i)} - (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] : - measure.pi μ = map (measurable_equiv.pi_fin_two α).symm ((μ 0).prod (μ 1)) := -begin - refine pi_eq (λ s hs, _), - rw [measurable_equiv.map_apply, fin.prod_univ_succ, fin.prod_univ_succ, fin.prod_univ_zero, - mul_one, ← measure.prod_prod], - congr' 1, - ext ⟨a, b⟩, - simp [fin.forall_fin_succ, is_empty.forall_iff] -end - -lemma {u} map_pi_fin_two {α : fin 2 → Type u} {m : Π i, measurable_space (α i)} - (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] : - map (measurable_equiv.pi_fin_two α) (measure.pi μ) = ((μ 0).prod (μ 1)) := -(measurable_equiv.pi_fin_two α).map_apply_eq_iff_map_symm_apply_eq.2 (pi_fin_two_eq_map μ).symm - -lemma prod_eq_map_fin_two_arrow {α : Type*} {m : measurable_space α} (μ ν : measure α) - [sigma_finite μ] [sigma_finite ν] : - μ.prod ν = map measurable_equiv.fin_two_arrow (measure.pi ![μ, ν]) := -begin - haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩, - exact (map_pi_fin_two ![μ, ν]).symm -end - -lemma prod_eq_map_fin_two_arrow_same {α : Type*} {m : measurable_space α} (μ : measure α) - [sigma_finite μ] : - μ.prod μ = map measurable_equiv.fin_two_arrow (measure.pi $ λ _, μ) := -by rw [prod_eq_map_fin_two_arrow, matrix.vec_single_eq_const, matrix.vec_cons_const] - lemma pi_eval_preimage_null {i : ι} {s : set (α i)} (hs : μ i s = 0) : measure.pi μ (eval i ⁻¹' s) = 0 := begin @@ -576,7 +533,6 @@ begin end end measure - instance measure_space.pi [Π i, measure_space (α i)] : measure_space (Π i, α i) := ⟨measure.pi (λ i, volume)⟩ @@ -599,114 +555,83 @@ lemma volume_pi_closed_ball [Π i, measure_space (α i)] [∀ i, sigma_finite (v volume (metric.closed_ball x r) = ∏ i, volume (metric.closed_ball (x i) r) := measure.pi_closed_ball _ _ hr -section fun_unique /-! -### Integral over `ι → α` with `[unique ι]` +### Measure preserving equivalences -In this section we prove some lemmas that relate integrals over `ι → β`, where `ι` is a type with -unique element (e.g., `unit` or `fin 1`) and integrals over `β`. +In this section we prove that some measurable equivalences (e.g., between `fin 1 → α` and `α` or +between `fin 2 → α` and `α × α`) preserve measure or volume. These lemmas can be used to prove that +measures of corresponding sets (images or preimages) have equal measures and functions `f ∘ e` and +`f` have equal integrals, see lemmas in the `measure_theory.measure_preserving` prefix. -/ -variables {β E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] - [topological_space.second_countable_topology E] [borel_space E] [complete_space E] - -lemma integral_fun_unique_pi (ι) [unique ι] {m : measurable_space β} (μ : measure β) - (f : (ι → β) → E) : - ∫ y, f y ∂(measure.pi (λ _, μ)) = ∫ x, f (λ _, x) ∂μ := -by rw [measure.pi_unique_eq_map μ ι, integral_map_equiv]; refl - -lemma integral_fun_unique_pi' (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β) - (f : β → E) : - ∫ y : ι → β, f (y (default ι)) ∂(measure.pi (λ _, μ)) = ∫ x, f x ∂μ := -integral_fun_unique_pi ι μ _ - -lemma integral_fun_unique (ι : Type*) [unique ι] [measure_space β] (f : (ι → β) → E) : - ∫ y, f y = ∫ x, f (λ _, x) := -integral_fun_unique_pi ι volume f - -lemma integral_fun_unique' (ι : Type*) [unique ι] [measure_space β] (f : β → E) : - ∫ y : ι → β, f (y (default ι)) = ∫ x, f x := -integral_fun_unique_pi' ι volume f +section measure_preserving -lemma set_integral_fun_unique_pi (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β) - (f : (ι → β) → E) (s : set (ι → β)) : - ∫ y in s, f y ∂(measure.pi (λ _, μ)) = ∫ x in const ι ⁻¹' s, f (λ _, x) ∂μ := -by rw [measure.pi_unique_eq_map μ ι, set_integral_map_equiv]; refl - -lemma set_integral_fun_unique_pi' (ι : Type*) [unique ι] {m : measurable_space β} (μ : measure β) - (f : β → E) (s : set β) : - ∫ y : ι → β in function.eval (default ι) ⁻¹' s, f (y (default ι)) ∂(measure.pi (λ _, μ)) = - ∫ x in s, f x ∂μ := -by erw [set_integral_fun_unique_pi, (equiv.fun_unique ι β).symm_preimage_preimage] - -lemma set_integral_fun_unique (ι : Type*) [unique ι] [measure_space β] (f : (ι → β) → E) - (s : set (ι → β)) : - ∫ y in s, f y = ∫ x in const ι ⁻¹' s, f (λ _, x) := -by convert set_integral_fun_unique_pi ι volume f s - -lemma set_integral_fun_unique' (ι : Type*) [unique ι] [measure_space β] (f : β → E) (s : set β) : - ∫ y : ι → β in @function.eval ι (λ _, β) (default ι) ⁻¹' s, f (y (default ι)) = ∫ x in s, f x := -by convert set_integral_fun_unique_pi' ι volume f s +lemma measure_preserving_fun_unique {β : Type u} {m : measurable_space β} (μ : measure β) + (α : Type v) [unique α] : + measure_preserving (measurable_equiv.fun_unique α β) (measure.pi (λ a : α, μ)) μ := +begin + set e := measurable_equiv.fun_unique α β, + have : pi_premeasure (λ _ : α, μ.to_outer_measure) = measure.map e.symm μ, + { ext1 s, + rw [pi_premeasure, fintype.prod_unique, to_outer_measure_apply, e.symm.map_apply], + congr' 1, exact e.to_equiv.image_eq_preimage s }, + simp only [measure.pi, outer_measure.pi, this, bounded_by_measure, to_outer_measure_to_measure], + exact ((measurable_equiv.fun_unique α β).symm.measurable.measure_preserving _).symm +end -end fun_unique +lemma volume_preserving_fun_unique (α : Type u) (β : Type v) [unique α] [measure_space β] : + measure_preserving (measurable_equiv.fun_unique α β) volume volume := +measure_preserving_fun_unique volume α -section fin_two_arrow +lemma measure_preserving_pi_fin_two {α : fin 2 → Type u} {m : Π i, measurable_space (α i)} + (μ : Π i, measure (α i)) [∀ i, sigma_finite (μ i)] : + measure_preserving (measurable_equiv.pi_fin_two α) (measure.pi μ) ((μ 0).prod (μ 1)) := +begin + refine ⟨measurable_equiv.measurable _, (measure.prod_eq $ λ s t hs ht, _).symm⟩, + rw [measurable_equiv.map_apply, measurable_equiv.pi_fin_two_apply, fin.preimage_apply_01_prod, + measure.pi_pi, fin.prod_univ_two], + refl +end -variables {β E : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] - [topological_space.second_countable_topology E] [borel_space E] [complete_space E] +lemma volume_preserving_pi_fin_two (α : fin 2 → Type u) [Π i, measure_space (α i)] + [∀ i, sigma_finite (volume : measure (α i))] : + measure_preserving (measurable_equiv.pi_fin_two α) volume volume := +measure_preserving_pi_fin_two _ -lemma integral_fin_two_arrow_pi {m : measurable_space β} (μ ν : measure β) - [sigma_finite μ] [sigma_finite ν] (f : (fin 2 → β) → E) : - ∫ y, f y ∂(measure.pi ![μ, ν]) = ∫ x, f ![x.1, x.2] ∂(μ.prod ν) := +lemma measure_preserving_fin_two_arrow_vec {α : Type u} {m : measurable_space α} + (μ ν : measure α) [sigma_finite μ] [sigma_finite ν] : + measure_preserving measurable_equiv.fin_two_arrow (measure.pi ![μ, ν]) (μ.prod ν) := begin haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩, - rw [measure.pi_fin_two_eq_map, integral_map_equiv], refl + exact measure_preserving_pi_fin_two _ end -lemma integral_fin_two_arrow_pi' {m : measurable_space β} (μ ν : measure β) [sigma_finite μ] - [sigma_finite ν] (f : β × β → E) : - ∫ y : fin 2 → β, f (y 0, y 1) ∂(measure.pi ![μ, ν]) = ∫ x, f x ∂(μ.prod ν) := -by { rw [measure.prod_eq_map_fin_two_arrow, integral_map_equiv], refl } - -lemma integral_fin_two_arrow [measure_space β] [sigma_finite (volume : measure β)] - (f : (fin 2 → β) → E) : - ∫ y, f y = ∫ x : β × β, f ![x.1, x.2] := -by rw [volume_pi, measure.volume_eq_prod, ← integral_fin_two_arrow_pi, matrix.vec_single_eq_const, - matrix.vec_cons_const] - -lemma integral_fin_two_arrow' [measure_space β] [sigma_finite (volume : measure β)] - (f : β × β → E) : - ∫ y : fin 2 → β, f (y 0, y 1) = ∫ x, f x := -by rw [volume_pi, measure.volume_eq_prod, ← integral_fin_two_arrow_pi', matrix.vec_single_eq_const, - matrix.vec_cons_const] - -lemma set_integral_fin_two_arrow_pi {m : measurable_space β} (μ ν : measure β) - [sigma_finite μ] [sigma_finite ν] (f : (fin 2 → β) → E) (s : set (fin 2 → β)) : - ∫ y in s, f y ∂(measure.pi ![μ, ν]) = - ∫ x : β × β in (fin_two_arrow_equiv β).symm ⁻¹' s, f ![x.1, x.2] ∂(μ.prod ν) := +lemma measure_preserving_fin_two_arrow {α : Type u} {m : measurable_space α} + (μ : measure α) [sigma_finite μ] : + measure_preserving measurable_equiv.fin_two_arrow (measure.pi (λ _, μ)) (μ.prod μ) := +by simpa only [matrix.vec_single_eq_const, matrix.vec_cons_const] + using measure_preserving_fin_two_arrow_vec μ μ + +lemma volume_preserving_fin_two_arrow (α : Type u) [measure_space α] + [sigma_finite (volume : measure α)] : + measure_preserving (@measurable_equiv.fin_two_arrow α _) volume volume := +measure_preserving_fin_two_arrow volume + +lemma measure_preserving_pi_empty {ι : Type u} {α : ι → Type v} [is_empty ι] + {m : Π i, measurable_space (α i)} (μ : Π i, measure (α i)) : + measure_preserving (measurable_equiv.of_unique_of_unique (Π i, α i) unit) + (measure.pi μ) (measure.dirac ()) := begin - haveI : ∀ i, sigma_finite (![μ, ν] i) := fin.forall_fin_two.2 ⟨‹_›, ‹_›⟩, - rw [measure.pi_fin_two_eq_map, set_integral_map_equiv], refl + set e := (measurable_equiv.of_unique_of_unique (Π i, α i) unit), + refine ⟨e.measurable, _⟩, + rw [measure.pi_of_empty, measure.map_dirac e.measurable], refl end -lemma set_integral_fin_two_arrow_pi' {m : measurable_space β} (μ ν : measure β) - [sigma_finite μ] [sigma_finite ν] (f : β × β → E) (s : set (β × β)) : - ∫ y : fin 2 → β in fin_two_arrow_equiv β ⁻¹' s, f (y 0, y 1) ∂(measure.pi ![μ, ν]) = - ∫ x in s, f x ∂(μ.prod ν) := -by { rw [set_integral_fin_two_arrow_pi, equiv.symm_preimage_preimage], simp } - -lemma set_integral_fin_two_arrow [measure_space β] [sigma_finite (volume : measure β)] - (f : (fin 2 → β) → E) (s : set (fin 2 → β)) : - ∫ y in s, f y = ∫ x in (fin_two_arrow_equiv β).symm ⁻¹' s, f ![x.1, x.2] := -by rw [measure.volume_eq_prod, ← set_integral_fin_two_arrow_pi, volume_pi, - matrix.vec_single_eq_const, matrix.vec_cons_const] - -lemma set_integral_fin_two_arrow' [measure_space β] [sigma_finite (volume : measure β)] - (f : β × β → E) (s : set (β × β)) : - ∫ y : fin 2 → β in fin_two_arrow_equiv β ⁻¹' s, f (y 0, y 1) = ∫ x in s, f x := -by rw [measure.volume_eq_prod, ← set_integral_fin_two_arrow_pi', volume_pi, - matrix.vec_single_eq_const, matrix.vec_cons_const] - -end fin_two_arrow +lemma volume_preserving_pi_empty {ι : Type u} (α : ι → Type v) [is_empty ι] + [Π i, measure_space (α i)] : + measure_preserving (measurable_equiv.of_unique_of_unique (Π i, α i) unit) volume volume := +measure_preserving_pi_empty (λ _, volume) + +end measure_preserving end measure_theory diff --git a/src/measure_theory/function/l1_space.lean b/src/measure_theory/function/l1_space.lean index ec45f50147a73..a6ee6983b1120 100644 --- a/src/measure_theory/function/l1_space.lean +++ b/src/measure_theory/function/l1_space.lean @@ -466,6 +466,16 @@ lemma integrable_map_equiv (f : α ≃ᵐ δ) (g : δ → β) : integrable g (measure.map f μ) ↔ integrable (g ∘ f) μ := f.measurable_embedding.integrable_map_iff +lemma measure_preserving.integrable_comp [opens_measurable_space β] {ν : measure δ} {g : δ → β} + {f : α → δ} (hf : measure_preserving f μ ν) (hg : ae_measurable g ν) : + integrable (g ∘ f) μ ↔ integrable g ν := +by { rw ← hf.map_eq at hg ⊢, exact (integrable_map_measure hg hf.measurable).symm } + +lemma measure_preserving.integrable_comp_emb {f : α → δ} {ν} (h₁ : measure_preserving f μ ν) + (h₂ : measurable_embedding f) {g : δ → β} : + integrable (g ∘ f) μ ↔ integrable g ν := +h₁.map_eq ▸ iff.symm h₂.integrable_map_iff + lemma lintegral_edist_lt_top [second_countable_topology β] [opens_measurable_space β] {f g : α → β} (hf : integrable f μ) (hg : integrable g μ) : ∫⁻ a, edist (f a) (g a) ∂μ < ∞ := diff --git a/src/measure_theory/integral/bochner.lean b/src/measure_theory/integral/bochner.lean index f40724b47fd2e..65bbe4e4a7e73 100644 --- a/src/measure_theory/integral/bochner.lean +++ b/src/measure_theory/integral/bochner.lean @@ -1267,6 +1267,11 @@ lemma integral_map_equiv {β} [measurable_space β] (e : α ≃ᵐ β) (f : β ∫ y, f y ∂(measure.map e μ) = ∫ x, f (e x) ∂μ := e.measurable_embedding.integral_map f +lemma measure_preserving.integral_comp {β} {_ : measurable_space β} {f : α → β} {ν} + (h₁ : measure_preserving f μ ν) (h₂ : measurable_embedding f) (g : β → E) : + ∫ x, g (f x) ∂μ = ∫ y, g y ∂ν := +h₁.map_eq ▸ (h₂.integral_map g).symm + @[simp] lemma integral_dirac' [measurable_space α] (f : α → E) (a : α) (hfm : measurable f) : ∫ x, f x ∂(measure.dirac a) = f a := calc ∫ x, f x ∂(measure.dirac a) = ∫ x, f a ∂(measure.dirac a) : diff --git a/src/measure_theory/integral/integrable_on.lean b/src/measure_theory/integral/integrable_on.lean index 0fb400772b063..f236b0cf483a4 100644 --- a/src/measure_theory/integral/integrable_on.lean +++ b/src/measure_theory/integral/integrable_on.lean @@ -181,6 +181,16 @@ lemma integrable_on_map_equiv [measurable_space β] (e : α ≃ᵐ β) {f : β integrable_on f s (measure.map e μ) ↔ integrable_on (f ∘ e) (e ⁻¹' s) μ := by simp only [integrable_on, e.restrict_map, integrable_map_equiv e] +lemma measure_preserving.integrable_on_comp_preimage [measurable_space β] {e : α → β} {ν} + (h₁ : measure_preserving e μ ν) (h₂ : measurable_embedding e) {f : β → E} {s : set β} : + integrable_on (f ∘ e) (e ⁻¹' s) μ ↔ integrable_on f s ν := +(h₁.restrict_preimage_emb h₂ s).integrable_comp_emb h₂ + +lemma measure_preserving.integrable_on_image [measurable_space β] {e : α → β} {ν} + (h₁ : measure_preserving e μ ν) (h₂ : measurable_embedding e) {f : β → E} {s : set α} : + integrable_on f (e '' s) ν ↔ integrable_on (f ∘ e) s μ := +((h₁.restrict_image_emb h₂ s).integrable_comp_emb h₂).symm + lemma integrable_indicator_iff (hs : measurable_set s) : integrable (indicator s f) μ ↔ integrable_on f s μ := by simp [integrable_on, integrable, has_finite_integral, nnnorm_indicator_eq_indicator_nnnorm, diff --git a/src/measure_theory/integral/lebesgue.lean b/src/measure_theory/integral/lebesgue.lean index 8cf65d6d5b4ce..3ae3768be33e7 100644 --- a/src/measure_theory/integral/lebesgue.lean +++ b/src/measure_theory/integral/lebesgue.lean @@ -7,6 +7,7 @@ import measure_theory.measure.mutually_singular import measure_theory.constructions.borel_space import algebra.indicator_function import algebra.support +import dynamics.ergodic.measure_preserving /-! # Lebesgue integral for `ℝ≥0∞`-valued functions @@ -1918,6 +1919,34 @@ lemma lintegral_map_equiv [measurable_space β] (f : β → ℝ≥0∞) (g : α ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ := g.measurable_embedding.lintegral_map f +lemma measure_preserving.lintegral_comp {mb : measurable_space β} {ν : measure β} {g : α → β} + (hg : measure_preserving g μ ν) {f : β → ℝ≥0∞} (hf : measurable f) : + ∫⁻ a, f (g a) ∂μ = ∫⁻ b, f b ∂ν := +by rw [← hg.map_eq, lintegral_map hf hg.measurable] + +lemma measure_preserving.lintegral_comp_emb {mb : measurable_space β} {ν : measure β} {g : α → β} + (hg : measure_preserving g μ ν) (hge : measurable_embedding g) (f : β → ℝ≥0∞) : + ∫⁻ a, f (g a) ∂μ = ∫⁻ b, f b ∂ν := +by rw [← hg.map_eq, hge.lintegral_map] + +lemma measure_preserving.set_lintegral_comp_preimage {mb : measurable_space β} {ν : measure β} + {g : α → β} (hg : measure_preserving g μ ν) {s : set β} (hs : measurable_set s) + {f : β → ℝ≥0∞} (hf : measurable f) : + ∫⁻ a in g ⁻¹' s, f (g a) ∂μ = ∫⁻ b in s, f b ∂ν := +by rw [← hg.map_eq, set_lintegral_map hs hf hg.measurable] + +lemma measure_preserving.set_lintegral_comp_preimage_emb {mb : measurable_space β} {ν : measure β} + {g : α → β} (hg : measure_preserving g μ ν) (hge : measurable_embedding g) (f : β → ℝ≥0∞) + (s : set β) : + ∫⁻ a in g ⁻¹' s, f (g a) ∂μ = ∫⁻ b in s, f b ∂ν := +by rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map] + +lemma measure_preserving.set_lintegral_comp_emb {mb : measurable_space β} {ν : measure β} + {g : α → β} (hg : measure_preserving g μ ν) (hge : measurable_embedding g) (f : β → ℝ≥0∞) + (s : set α) : + ∫⁻ a in s, f (g a) ∂μ = ∫⁻ b in g '' s, f b ∂ν := +by rw [← hg.set_lintegral_comp_preimage_emb hge, preimage_image_eq _ hge.injective] + section dirac_and_count variable [measurable_space α] diff --git a/src/measure_theory/integral/set_integral.lean b/src/measure_theory/integral/set_integral.lean index 47b6f186ee825..7a56caccf6985 100644 --- a/src/measure_theory/integral/set_integral.lean +++ b/src/measure_theory/integral/set_integral.lean @@ -315,6 +315,16 @@ lemma _root_.closed_embedding.set_integral_map [topological_space α] [borel_spa ∫ y in s, f y ∂(measure.map g μ) = ∫ x in g ⁻¹' s, f (g x) ∂μ := hg.measurable_embedding.set_integral_map _ _ +lemma measure_preserving.set_integral_preimage_emb {β} {_ : measurable_space β} {f : α → β} {ν} + (h₁ : measure_preserving f μ ν) (h₂ : measurable_embedding f) (g : β → E) (s : set β) : + ∫ x in f ⁻¹' s, g (f x) ∂μ = ∫ y in s, g y ∂ν := +(h₁.restrict_preimage_emb h₂ s).integral_comp h₂ _ + +lemma measure_preserving.set_integral_image_emb {β} {_ : measurable_space β} {f : α → β} {ν} + (h₁ : measure_preserving f μ ν) (h₂ : measurable_embedding f) (g : β → E) (s : set α) : + ∫ y in f '' s, g y ∂ν = ∫ x in s, g (f x) ∂μ := +eq.symm $ (h₁.restrict_image_emb h₂ s).integral_comp h₂ _ + lemma set_integral_map_equiv {β} [measurable_space β] (e : α ≃ᵐ β) (f : β → E) (s : set β) : ∫ y in s, f y ∂(measure.map e μ) = ∫ x in e ⁻¹' s, f (e x) ∂μ := e.measurable_embedding.set_integral_map f s diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean index 88f4191010f58..32dcf982e85f4 100644 --- a/src/measure_theory/measure/measure_space.lean +++ b/src/measure_theory/measure/measure_space.lean @@ -1134,6 +1134,8 @@ variable [measurable_space α] def dirac (a : α) : measure α := (outer_measure.dirac a).to_measure (by simp) +instance : measure_space punit := ⟨dirac punit.star⟩ + lemma le_dirac_apply {a} : s.indicator 1 a ≤ dirac a s := outer_measure.dirac_apply a s ▸ le_to_measure_apply _ _ _