From 6d3e93626dc338de8d107e2a45106460036c1efd Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 28 Jul 2021 22:58:41 +0000 Subject: [PATCH] feat(measure_theory): add @[to_additive] (#8142) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds `@[to_additive]` to `haar_measure` and everything that depends on. This will allow us to define the Lebesgue measure on `ℝ` and `ℝ ^ n` as the Haar measure (or just show that it is equal to it). Co-authored-by: Floris van Doorn --- src/algebra/group/to_additive.lean | 4 +- src/measure_theory/arithmetic.lean | 84 +++++++++++-------- .../conditional_expectation.lean | 8 +- src/measure_theory/content.lean | 5 +- src/measure_theory/group.lean | 8 +- src/measure_theory/haar_measure.lean | 57 ++++++++++++- src/measure_theory/lp_space.lean | 42 +++++----- src/measure_theory/prod_group.lean | 17 +++- src/topology/algebra/group.lean | 3 +- 9 files changed, 151 insertions(+), 77 deletions(-) diff --git a/src/algebra/group/to_additive.lean b/src/algebra/group/to_additive.lean index e54da8649ea96..7e451f2c896f2 100644 --- a/src/algebra/group/to_additive.lean +++ b/src/algebra/group/to_additive.lean @@ -137,7 +137,7 @@ structure value_type : Type := /-- `add_comm_prefix x s` returns `"comm_" ++ s` if `x = tt` and `s` otherwise. -/ meta def add_comm_prefix : bool → string → string -| tt s := ("comm_" ++ s) +| tt s := "comm_" ++ s | ff s := s /-- Dictionary used by `to_additive.guess_name` to autogenerate names. -/ @@ -163,6 +163,8 @@ meta def tr : bool → list string → list string | is_comm ("subgroup" :: s) := ("add_" ++ add_comm_prefix is_comm "subgroup") :: tr ff s | is_comm ("semigroup" :: s) := ("add_" ++ add_comm_prefix is_comm "semigroup") :: tr ff s | is_comm ("magma" :: s) := ("add_" ++ add_comm_prefix is_comm "magma") :: tr ff s +| is_comm ("haar" :: s) := ("add_" ++ add_comm_prefix is_comm "haar") :: tr ff s +| is_comm ("prehaar" :: s) := ("add_" ++ add_comm_prefix is_comm "prehaar") :: tr ff s | is_comm ("comm" :: s) := tr tt s | is_comm (x :: s) := (add_comm_prefix is_comm x :: tr ff s) | tt [] := ["comm"] diff --git a/src/measure_theory/arithmetic.lean b/src/measure_theory/arithmetic.lean index 7372b6fb316d9..e6645ab74e848 100644 --- a/src/measure_theory/arithmetic.lean +++ b/src/measure_theory/arithmetic.lean @@ -25,9 +25,21 @@ because on some types (e.g., `ℕ`, `ℝ≥0∞`) division and/or subtraction ar For instances relating, e.g., `has_continuous_mul` to `has_measurable_mul` see file `measure_theory.borel_space`. +## Implementation notes + +For the heuristics of `@[to_additive]` it is important that the type with a multiplication +(or another multiplicative operations) is the first (implicit) argument of all declarations. + ## Tags measurable function, arithmetic operator + +## Todo + +* Uniformize the treatment of `pow` and `smul`. +* Use `@[to_additive]` to send `has_measurable_pow` to `has_measurable_smul₂`. +* This might require changing the definition (swapping the arguments in the function that is + in the conclusion of `measurable_smul`.) -/ universes u v @@ -35,8 +47,6 @@ universes u v open_locale big_operators open measure_theory -variables {α : Type*} [measurable_space α] - /-! ### Binary operations: `(+)`, `(*)`, `(-)`, `(/)` -/ @@ -73,7 +83,7 @@ export has_measurable_mul₂ (measurable_mul) section mul -variables {M : Type*} [measurable_space M] [has_mul M] +variables {M α : Type*} [measurable_space M] [has_mul M] [measurable_space α] @[to_additive, measurability] lemma measurable.const_mul [has_measurable_mul M] {f : α → M} (hf : measurable f) (c : M) : @@ -148,8 +158,8 @@ end⟩ section pow -variables {β γ : Type*} [measurable_space β] [measurable_space γ] [has_pow β γ] - [has_measurable_pow β γ] +variables {β γ α : Type*} [measurable_space β] [measurable_space γ] [has_pow β γ] + [has_measurable_pow β γ] [measurable_space α] @[measurability] lemma measurable.pow {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) : @@ -213,7 +223,7 @@ export has_measurable_div₂ (measurable_div) section div -variables {G : Type*} [measurable_space G] [has_div G] +variables {G α : Type*} [measurable_space G] [has_div G] [measurable_space α] @[to_additive, measurability] lemma measurable.const_div [has_measurable_div G] {f : α → G} (hf : measurable f) (c : G) : @@ -313,7 +323,7 @@ instance has_measurable_div_of_mul_inv (G : Type*) [measurable_space G] section inv -variables {G : Type*} [has_inv G] [measurable_space G] [has_measurable_inv G] +variables {G α : Type*} [has_inv G] [measurable_space G] [has_measurable_inv G] [measurable_space α] @[to_additive, measurability] lemma measurable.inv {f : α → G} (hf : measurable f) : @@ -406,7 +416,8 @@ instance has_measurable_smul₂_of_mul (M : Type*) [monoid M] [measurable_space section smul -variables {M β : Type*} [measurable_space M] [measurable_space β] [has_scalar M β] +variables {M β α : Type*} [measurable_space M] [measurable_space β] [has_scalar M β] + [measurable_space α] @[measurability] lemma measurable.smul [has_measurable_smul₂ M β] @@ -460,8 +471,8 @@ end smul section mul_action -variables {M β : Type*} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] - [has_measurable_smul M β] {f : α → β} {μ : measure α} +variables {M β α : Type*} [measurable_space M] [measurable_space β] [monoid M] [mul_action M β] + [has_measurable_smul M β] [measurable_space α] {f : α → β} {μ : measure α} variables {G : Type*} [group G] [measurable_space G] [mul_action G β] [has_measurable_smul G β] @@ -506,9 +517,11 @@ end mul_action ### Big operators: `∏` and `∑` -/ +section monoid +variables {M α : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M] [measurable_space α] + @[to_additive, measurability] -lemma list.measurable_prod' {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M] - (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) : +lemma list.measurable_prod' (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) : measurable l.prod := begin induction l with f l ihl, { exact measurable_one }, @@ -518,9 +531,8 @@ begin end @[to_additive, measurability] -lemma list.ae_measurable_prod' {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M] - {μ : measure α} (l : list (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) : - ae_measurable l.prod μ := +lemma list.ae_measurable_prod' {μ : measure α} (l : list (α → M)) + (hl : ∀ f ∈ l, ae_measurable f μ) : ae_measurable l.prod μ := begin induction l with f l ihl, { exact ae_measurable_one }, rw [list.forall_mem_cons] at hl, @@ -529,68 +541,66 @@ begin end @[to_additive, measurability] -lemma list.measurable_prod {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M] - (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) : +lemma list.measurable_prod (l : list (α → M)) (hl : ∀ f ∈ l, measurable f) : measurable (λ x, (l.map (λ f : α → M, f x)).prod) := by simpa only [← pi.list_prod_apply] using l.measurable_prod' hl @[to_additive, measurability] -lemma list.ae_measurable_prod {M : Type*} [monoid M] [measurable_space M] [has_measurable_mul₂ M] - {μ : measure α} (l : list (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) : +lemma list.ae_measurable_prod {μ : measure α} (l : list (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) : ae_measurable (λ x, (l.map (λ f : α → M, f x)).prod) μ := by simpa only [← pi.list_prod_apply] using l.ae_measurable_prod' hl +end monoid + +section comm_monoid +variables {M ι α : Type*} [comm_monoid M] [measurable_space M] [has_measurable_mul₂ M] + [measurable_space α] + @[to_additive, measurability] -lemma multiset.measurable_prod' {M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] (l : multiset (α → M)) (hl : ∀ f ∈ l, measurable f) : +lemma multiset.measurable_prod' (l : multiset (α → M)) (hl : ∀ f ∈ l, measurable f) : measurable l.prod := by { rcases l with ⟨l⟩, simpa using l.measurable_prod' (by simpa using hl) } @[to_additive, measurability] -lemma multiset.ae_measurable_prod' {M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] {μ : measure α} (l : multiset (α → M)) (hl : ∀ f ∈ l, ae_measurable f μ) : - ae_measurable l.prod μ := +lemma multiset.ae_measurable_prod' {μ : measure α} (l : multiset (α → M)) + (hl : ∀ f ∈ l, ae_measurable f μ) : ae_measurable l.prod μ := by { rcases l with ⟨l⟩, simpa using l.ae_measurable_prod' (by simpa using hl) } @[to_additive, measurability] -lemma multiset.measurable_prod {M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] (s : multiset (α → M)) (hs : ∀ f ∈ s, measurable f) : +lemma multiset.measurable_prod (s : multiset (α → M)) (hs : ∀ f ∈ s, measurable f) : measurable (λ x, (s.map (λ f : α → M, f x)).prod) := by simpa only [← pi.multiset_prod_apply] using s.measurable_prod' hs @[to_additive, measurability] -lemma multiset.ae_measurable_prod {M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] {μ : measure α} (s : multiset (α → M)) (hs : ∀ f ∈ s, ae_measurable f μ) : - ae_measurable (λ x, (s.map (λ f : α → M, f x)).prod) μ := +lemma multiset.ae_measurable_prod {μ : measure α} (s : multiset (α → M)) + (hs : ∀ f ∈ s, ae_measurable f μ) : ae_measurable (λ x, (s.map (λ f : α → M, f x)).prod) μ := by simpa only [← pi.multiset_prod_apply] using s.ae_measurable_prod' hs @[to_additive, measurability] -lemma finset.measurable_prod' {ι M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) : +lemma finset.measurable_prod' {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) : measurable (∏ i in s, f i) := finset.prod_induction _ _ (λ _ _, measurable.mul) (@measurable_one M _ _ _ _) hf @[to_additive, measurability] -lemma finset.measurable_prod {ι M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) : +lemma finset.measurable_prod {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, measurable (f i)) : measurable (λ a, ∏ i in s, f i a) := by simpa only [← finset.prod_apply] using s.measurable_prod' hf @[to_additive, measurability] -lemma finset.ae_measurable_prod' {ι M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] {μ : measure α} {f : ι → α → M} (s : finset ι) +lemma finset.ae_measurable_prod' {μ : measure α} {f : ι → α → M} (s : finset ι) (hf : ∀i ∈ s, ae_measurable (f i) μ) : ae_measurable (∏ i in s, f i) μ := multiset.ae_measurable_prod' _ $ λ g hg, let ⟨i, hi, hg⟩ := multiset.mem_map.1 hg in (hg ▸ hf _ hi) @[to_additive, measurability] -lemma finset.ae_measurable_prod {ι M : Type*} [comm_monoid M] [measurable_space M] - [has_measurable_mul₂ M] {f : ι → α → M} {μ : measure α} (s : finset ι) +lemma finset.ae_measurable_prod {f : ι → α → M} {μ : measure α} (s : finset ι) (hf : ∀i ∈ s, ae_measurable (f i) μ) : ae_measurable (λ a, ∏ i in s, f i a) μ := by simpa only [← finset.prod_apply] using s.ae_measurable_prod' hf +end comm_monoid + attribute [measurability] list.measurable_sum' list.ae_measurable_sum' list.measurable_sum list.ae_measurable_sum multiset.measurable_sum' multiset.ae_measurable_sum' multiset.measurable_sum multiset.ae_measurable_sum finset.measurable_sum' diff --git a/src/measure_theory/conditional_expectation.lean b/src/measure_theory/conditional_expectation.lean index 3ea640096b6ca..15c5fdeda25fe 100644 --- a/src/measure_theory/conditional_expectation.lean +++ b/src/measure_theory/conditional_expectation.lean @@ -43,14 +43,14 @@ lemma add [has_add β] [has_measurable_add₂ β] (hf : ae_measurable' m f μ) begin rcases hf with ⟨f', h_f'_meas, hff'⟩, rcases hg with ⟨g', h_g'_meas, hgg'⟩, - exact ⟨f' + g', @measurable.add α m _ _ _ _ f' g' h_f'_meas h_g'_meas, hff'.add hgg'⟩, + exact ⟨f' + g', @measurable.add _ _ _ _ m _ f' g' h_f'_meas h_g'_meas, hff'.add hgg'⟩, end lemma const_smul [has_scalar 𝕜 β] [has_measurable_smul 𝕜 β] (c : 𝕜) (hf : ae_measurable' m f μ) : ae_measurable' m (c • f) μ := begin rcases hf with ⟨f', h_f'_meas, hff'⟩, - refine ⟨c • f', @measurable.const_smul α m _ _ _ _ _ _ f' h_f'_meas c, _⟩, + refine ⟨c • f', @measurable.const_smul _ _ _ _ _ _ m _ f' h_f'_meas c, _⟩, exact eventually_eq.fun_comp hff' (λ x, c • x), end @@ -216,7 +216,7 @@ begin refine eventually_eq.trans _ (@Lp.coe_fn_add _ _ m _ _ _ _ _ _ _ _).symm, refine ae_eq_trim_of_measurable hm _ _ _, { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, }, - { exact @measurable.add _ m _ _ _ _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _) + { exact @measurable.add _ _ _ _ m _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _) (@Lp.measurable _ _ m _ _ _ _ _ _ _), }, refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _, refine eventually_eq.trans _ @@ -234,7 +234,7 @@ begin refine eventually_eq.trans _ (@Lp.coe_fn_smul _ _ m _ _ _ _ _ _ _ _ _ _ _ _ _).symm, refine ae_eq_trim_of_measurable hm _ _ _, { exact @Lp.measurable _ _ m _ _ _ _ _ _ _, }, - { exact @measurable.const_smul _ m _ _ _ _ _ _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _) c, }, + { exact @measurable.const_smul _ _ _ _ _ _ m _ _ (@Lp.measurable _ _ m _ _ _ _ _ _ _) c, }, refine (Lp_meas_to_Lp_trim_ae_eq hm _).trans _, refine (Lp.coe_fn_smul c _).trans _, refine (Lp_meas_to_Lp_trim_ae_eq hm f).mono (λ x hx, _), diff --git a/src/measure_theory/content.lean b/src/measure_theory/content.lean index 1868daf7c95f6..fa0e6c33ca914 100644 --- a/src/measure_theory/content.lean +++ b/src/measure_theory/content.lean @@ -193,7 +193,7 @@ lemma is_mul_left_invariant_inner_content [group G] [topological_group G] (U : opens G) : μ.inner_content (U.comap $ continuous_mul_left g) = μ.inner_content U := by convert μ.inner_content_comap (homeomorph.mul_left g) (λ K, h g) U --- @[to_additive] (fails for now) +@[to_additive] lemma inner_content_pos_of_is_mul_left_invariant [t2_space G] [group G] [topological_group G] (h3 : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K) (K : compacts G) (hK : 0 < μ K) (U : opens G) (hU : (U : set G).nonempty) : @@ -299,7 +299,7 @@ begin apply inner_content_mono' end --- @[to_additive] (fails for now) +@[to_additive] lemma outer_measure_pos_of_is_mul_left_invariant [group G] [topological_group G] (h3 : ∀ (g : G) {K : compacts G}, μ (K.map _ $ continuous_mul_left g) = μ K) (K : compacts G) (hK : 0 < μ K) {U : set G} (h1U : is_open U) (h2U : U.nonempty) : @@ -307,7 +307,6 @@ lemma outer_measure_pos_of_is_mul_left_invariant [group G] [topological_group G] by { convert μ.inner_content_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U, exact μ.outer_measure_opens ⟨U, h1U⟩ } - variables [S : measurable_space G] [borel_space G] include S diff --git a/src/measure_theory/group.lean b/src/measure_theory/group.lean index 665be5817e00d..aa93e4abdcdbd 100644 --- a/src/measure_theory/group.lean +++ b/src/measure_theory/group.lean @@ -155,7 +155,7 @@ section group variables [group G] [topological_group G] /-! Properties of regular left invariant measures -/ -@[to_additive measure_theory.measure.is_add_left_invariant.null_iff_empty] +@[to_additive] lemma is_mul_left_invariant.null_iff_empty [regular μ] (h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) : μ s = 0 ↔ s = ∅ := begin @@ -177,7 +177,7 @@ begin rwa [inv_mul_cancel_right] } end -@[to_additive measure_theory.measure.is_add_left_invariant.null_iff] +@[to_additive] lemma is_mul_left_invariant.null_iff [regular μ] (h2μ : is_mul_left_invariant μ) {s : set G} (hs : is_open s) : μ s = 0 ↔ s = ∅ ∨ μ = 0 := begin @@ -186,7 +186,7 @@ begin exact h2μ.null_iff_empty h3μ hs, end -@[to_additive measure_theory.measure.is_add_left_invariant.measure_ne_zero_iff_nonempty] +@[to_additive] lemma is_mul_left_invariant.measure_ne_zero_iff_nonempty [regular μ] (h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) : μ s ≠ 0 ↔ s.nonempty := @@ -194,7 +194,7 @@ by simp_rw [← ne_empty_iff_nonempty, ne.def, h2μ.null_iff_empty h3μ hs] /-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function `f` is 0 iff `f` is 0. -/ --- @[to_additive] (fails for now) +@[to_additive] lemma lintegral_eq_zero_of_is_mul_left_invariant [regular μ] (h2μ : is_mul_left_invariant μ) (h3μ : μ ≠ 0) {f : G → ℝ≥0∞} (hf : continuous f) : ∫⁻ x, f x ∂μ = 0 ↔ f = 0 := diff --git a/src/measure_theory/haar_measure.lean b/src/measure_theory/haar_measure.lean index 1715db6223de8..8f82e78172986 100644 --- a/src/measure_theory/haar_measure.lean +++ b/src/measure_theory/haar_measure.lean @@ -70,9 +70,11 @@ namespace haar /-- The index or Haar covering number or ratio of `K` w.r.t. `V`, denoted `(K : V)`: it is the smallest number of (left) translates of `V` that is necessary to cover `K`. It is defined to be 0 if no finite number of translates cover `K`. -/ +@[to_additive add_index "additive version of `measure_theory.measure.haar.index`"] def index (K V : set G) : ℕ := Inf $ finset.card '' {t : finset G | K ⊆ ⋃ g ∈ t, (λ h, g * h) ⁻¹' V } +@[to_additive add_index_empty] lemma index_empty {V : set G} : index ∅ V = 0 := begin simp only [index, nat.Inf_eq_zero], left, use ∅, @@ -86,21 +88,26 @@ variables [topological_space G] and `K` is any compact set. The argument `K` is a (bundled) compact set, so that we can consider `prehaar K₀ U` as an element of `haar_product` (below). -/ +@[to_additive "additive version of `measure_theory.measure.haar.prehaar`"] def prehaar (K₀ U : set G) (K : compacts G) : ℝ := (index K.1 U : ℝ) / index K₀ U +@[to_additive] lemma prehaar_empty (K₀ : positive_compacts G) {U : set G} : prehaar K₀.1 U ⊥ = 0 := by { simp only [prehaar, compacts.bot_val, index_empty, nat.cast_zero, zero_div] } +@[to_additive] lemma prehaar_nonneg (K₀ : positive_compacts G) {U : set G} (K : compacts G) : 0 ≤ prehaar K₀.1 U K := by apply div_nonneg; norm_cast; apply zero_le /-- `haar_product K₀` is the product of intervals `[0, (K : K₀)]`, for all compact sets `K`. For all `U`, we can show that `prehaar K₀ U ∈ haar_product K₀`. -/ +@[to_additive "additive version of `measure_theory.measure.haar.haar_product`"] def haar_product (K₀ : set G) : set (compacts G → ℝ) := pi univ (λ K, Icc 0 $ index K.1 K₀) -@[simp] lemma mem_prehaar_empty {K₀ : set G} {f : compacts G → ℝ} : +@[simp, to_additive] +lemma mem_prehaar_empty {K₀ : set G} {f : compacts G → ℝ} : f ∈ haar_product K₀ ↔ ∀ K : compacts G, f K ∈ Icc (0 : ℝ) (index K.1 K₀) := by simp only [haar_product, pi, forall_prop_of_true, mem_univ, mem_set_of_eq] @@ -109,6 +116,7 @@ by simp only [haar_product, pi, forall_prop_of_true, mem_univ, mem_set_of_eq] `compacts G → ℝ`, with the topology of pointwise convergence. We show that the intersection of all these sets is nonempty, and the Haar measure on compact sets is defined to be an element in the closure of this intersection. -/ +@[to_additive "additive version of `measure_theory.measure.haar.cl_prehaar`"] def cl_prehaar (K₀ : set G) (V : open_nhds_of (1 : G)) : set (compacts G → ℝ) := closure $ prehaar K₀ '' { U : set G | U ⊆ V.1 ∧ is_open U ∧ (1 : G) ∈ U } @@ -120,14 +128,17 @@ variables [topological_group G] /-- If `K` is compact and `V` has nonempty interior, then the index `(K : V)` is well-defined, there is a finite set `t` satisfying the desired properties. -/ +@[to_additive add_index_defined] lemma index_defined {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) : ∃ n : ℕ, n ∈ finset.card '' {t : finset G | K ⊆ ⋃ g ∈ t, (λ h, g * h) ⁻¹' V } := by { rcases compact_covered_by_mul_left_translates hK hV with ⟨t, ht⟩, exact ⟨t.card, t, ht, rfl⟩ } +@[to_additive add_index_elim] lemma index_elim {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) : ∃ (t : finset G), K ⊆ (⋃ g ∈ t, (λ h, g * h) ⁻¹' V) ∧ finset.card t = index K V := by { have := nat.Inf_mem (index_defined hK hV), rwa [mem_image] at this } +@[to_additive le_add_index_mul] lemma le_index_mul (K₀ : positive_compacts G) (K : compacts G) {V : set G} (hV : (interior V).nonempty) : index K.1 V ≤ index K.1 K₀.1 * index K₀.1 V := begin @@ -142,6 +153,7 @@ begin exact mem_bUnion (finset.mul_mem_mul hg₃ hg₁) h2V end +@[to_additive add_index_pos] lemma index_pos (K : positive_compacts G) {V : set G} (hV : (interior V).nonempty) : 0 < index K.1 V := begin @@ -152,6 +164,7 @@ begin { exact index_defined K.2.1 hV } end +@[to_additive add_index_mono] lemma index_mono {K K' V : set G} (hK' : is_compact K') (h : K ⊆ K') (hV : (interior V).nonempty) : index K V ≤ index K' V := begin @@ -159,6 +172,7 @@ begin apply nat.Inf_le, rw [mem_image], refine ⟨s, subset.trans h h1s, h2s⟩ end +@[to_additive add_index_union_le] lemma index_union_le (K₁ K₂ : compacts G) {V : set G} (hV : (interior V).nonempty) : index (K₁.1 ∪ K₂.1) V ≤ index K₁.1 V + index K₂.1 V := begin @@ -172,6 +186,7 @@ begin simp only [mem_def, multiset.mem_union, finset.union_val, hg, or_true, true_or] end +@[to_additive add_index_union_eq] lemma index_union_eq (K₁ K₂ : compacts G) {V : set G} (hV : (interior V).nonempty) (h : disjoint (K₁.1 * V⁻¹) (K₂.1 * V⁻¹)) : index (K₁.1 ∪ K₂.1) V = index K₁.1 V + index K₂.1 V := @@ -202,6 +217,7 @@ begin simp only [mul_inv_rev, mul_inv_cancel_left] } end +@[to_additive add_left_add_index_le] lemma mul_left_index_le {K : set G} (hK : is_compact K) {V : set G} (hV : (interior V).nonempty) (g : G) : index ((λ h, g * h) '' K) V ≤ index K V := begin @@ -215,6 +231,7 @@ begin refine ⟨_, hg₂, _⟩, simp only [mul_assoc, hg₁, inv_mul_cancel_left] } end +@[to_additive is_left_invariant_add_index] lemma is_left_invariant_index {K : set G} (hK : is_compact K) (g : G) {V : set G} (hV : (interior V).nonempty) : index ((λ h, g * h) '' K) V = index K V := begin @@ -227,6 +244,7 @@ end ### Lemmas about `prehaar` -/ +@[to_additive add_prehaar_le_add_index] lemma prehaar_le_index (K₀ : positive_compacts G) {U : set G} (K : compacts G) (hU : (interior U).nonempty) : prehaar K₀.1 U K ≤ index K.1 K₀.1 := begin @@ -235,10 +253,12 @@ begin { exact index_pos K₀ hU } end +@[to_additive] lemma prehaar_pos (K₀ : positive_compacts G) {U : set G} (hU : (interior U).nonempty) {K : set G} (h1K : is_compact K) (h2K : (interior K).nonempty) : 0 < prehaar K₀.1 U ⟨K, h1K⟩ := by { apply div_pos; norm_cast, apply index_pos ⟨K, h1K, h2K⟩ hU, exact index_pos K₀ hU } +@[to_additive] lemma prehaar_mono {K₀ : positive_compacts G} {U : set G} (hU : (interior U).nonempty) {K₁ K₂ : compacts G} (h : K₁.1 ⊆ K₂.1) : prehaar K₀.1 U K₁ ≤ prehaar K₀.1 U K₂ := begin @@ -246,10 +266,12 @@ begin exact_mod_cast index_pos K₀ hU end +@[to_additive] lemma prehaar_self {K₀ : positive_compacts G} {U : set G} (hU : (interior U).nonempty) : prehaar K₀.1 U ⟨K₀.1, K₀.2.1⟩ = 1 := by { simp only [prehaar], rw [div_self], apply ne_of_gt, exact_mod_cast index_pos K₀ hU } +@[to_additive] lemma prehaar_sup_le {K₀ : positive_compacts G} {U : set G} (K₁ K₂ : compacts G) (hU : (interior U).nonempty) : prehaar K₀.1 U (K₁ ⊔ K₂) ≤ prehaar K₀.1 U K₁ + prehaar K₀.1 U K₂ := begin @@ -257,11 +279,13 @@ begin exact_mod_cast index_union_le K₁ K₂ hU, exact_mod_cast index_pos K₀ hU end +@[to_additive] lemma prehaar_sup_eq {K₀ : positive_compacts G} {U : set G} {K₁ K₂ : compacts G} (hU : (interior U).nonempty) (h : disjoint (K₁.1 * U⁻¹) (K₂.1 * U⁻¹)) : prehaar K₀.1 U (K₁ ⊔ K₂) = prehaar K₀.1 U K₁ + prehaar K₀.1 U K₂ := by { simp only [prehaar], rw [div_add_div_same], congr', exact_mod_cast index_union_eq K₁ K₂ hU h } +@[to_additive] lemma is_left_invariant_prehaar {K₀ : positive_compacts G} {U : set G} (hU : (interior U).nonempty) (g : G) (K : compacts G) : prehaar K₀.1 U (K.map _ $ continuous_mul_left g) = prehaar K₀.1 U K := by simp only [prehaar, compacts.map_val, is_left_invariant_index K.2 _ hU] @@ -270,10 +294,12 @@ by simp only [prehaar, compacts.map_val, is_left_invariant_index K.2 _ hU] ### Lemmas about `haar_product` -/ +@[to_additive] lemma prehaar_mem_haar_product (K₀ : positive_compacts G) {U : set G} (hU : (interior U).nonempty) : prehaar K₀.1 U ∈ haar_product K₀.1 := by { rintro ⟨K, hK⟩ h2K, rw [mem_Icc], exact ⟨prehaar_nonneg K₀ _, prehaar_le_index K₀ _ hU⟩ } +@[to_additive] lemma nonempty_Inter_cl_prehaar (K₀ : positive_compacts G) : (haar_product K₀.1 ∩ ⋂ (V : open_nhds_of (1 : G)), cl_prehaar K₀.1 V).nonempty := begin @@ -302,20 +328,25 @@ end This is roughly equal to the Haar measure on compact sets, but it can differ slightly. We do know that `haar_measure K₀ (interior K.1) ≤ chaar K₀ K ≤ haar_measure K₀ K.1`. -/ +@[to_additive add_chaar "additive version of `measure_theory.measure.haar.chaar`"] def chaar (K₀ : positive_compacts G) (K : compacts G) : ℝ := classical.some (nonempty_Inter_cl_prehaar K₀) K +@[to_additive add_chaar_mem_add_haar_product] lemma chaar_mem_haar_product (K₀ : positive_compacts G) : chaar K₀ ∈ haar_product K₀.1 := (classical.some_spec (nonempty_Inter_cl_prehaar K₀)).1 +@[to_additive add_chaar_mem_cl_add_prehaar] lemma chaar_mem_cl_prehaar (K₀ : positive_compacts G) (V : open_nhds_of (1 : G)) : chaar K₀ ∈ cl_prehaar K₀.1 V := by { have := (classical.some_spec (nonempty_Inter_cl_prehaar K₀)).2, rw [mem_Inter] at this, exact this V } +@[to_additive add_chaar_nonneg] lemma chaar_nonneg (K₀ : positive_compacts G) (K : compacts G) : 0 ≤ chaar K₀ K := by { have := chaar_mem_haar_product K₀ K (mem_univ _), rw mem_Icc at this, exact this.1 } +@[to_additive add_chaar_empty] lemma chaar_empty (K₀ : positive_compacts G) : chaar K₀ ⊥ = 0 := begin let eval : (compacts G → ℝ) → ℝ := λ f, f ⊥, @@ -327,6 +358,7 @@ begin { apply continuous_iff_is_closed.mp this, exact is_closed_singleton }, end +@[to_additive add_chaar_self] lemma chaar_self (K₀ : positive_compacts G) : chaar K₀ ⟨K₀.1, K₀.2.1⟩ = 1 := begin let eval : (compacts G → ℝ) → ℝ := λ f, f ⟨K₀.1, K₀.2.1⟩, @@ -339,6 +371,7 @@ begin { apply continuous_iff_is_closed.mp this, exact is_closed_singleton } end +@[to_additive add_chaar_mono] lemma chaar_mono {K₀ : positive_compacts G} {K₁ K₂ : compacts G} (h : K₁.1 ⊆ K₂.1) : chaar K₀ K₁ ≤ chaar K₀ K₂ := begin @@ -352,6 +385,7 @@ begin { apply continuous_iff_is_closed.mp this, exact is_closed_Ici }, end +@[to_additive add_chaar_sup_le] lemma chaar_sup_le {K₀ : positive_compacts G} (K₁ K₂ : compacts G) : chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂ := begin @@ -367,6 +401,7 @@ begin { apply continuous_iff_is_closed.mp this, exact is_closed_Ici }, end +@[to_additive add_chaar_sup_eq] lemma chaar_sup_eq [t2_space G] {K₀ : positive_compacts G} {K₁ K₂ : compacts G} (h : disjoint K₁.1 K₂.1) : chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂ := begin @@ -397,6 +432,7 @@ begin { apply continuous_iff_is_closed.mp this, exact is_closed_singleton }, end +@[to_additive is_left_invariant_add_chaar] lemma is_left_invariant_chaar {K₀ : positive_compacts G} (g : G) (K : compacts G) : chaar K₀ (K.map _ $ continuous_mul_left g) = chaar K₀ K := begin @@ -414,6 +450,7 @@ end variable [t2_space G] /-- The function `chaar` interpreted in `ℝ≥0`, as a content -/ +@[to_additive "additive version of `measure_theory.measure.haar.haar_content`"] def haar_content (K₀ : positive_compacts G) : content G := { to_fun := λ K, ⟨chaar K₀ K, chaar_nonneg _ _⟩, mono' := λ K₁ K₂ h, by simp only [←nnreal.coe_le_coe, subtype.coe_mk, chaar_mono, h], @@ -423,19 +460,23 @@ def haar_content (K₀ : positive_compacts G) : content G := /-! We only prove the properties for `haar_content` that we use at least twice below. -/ +@[to_additive] lemma haar_content_apply (K₀ : positive_compacts G) (K : compacts G) : haar_content K₀ K = show nnreal, from ⟨chaar K₀ K, chaar_nonneg _ _⟩ := rfl /-- The variant of `chaar_self` for `haar_content` -/ +@[to_additive] lemma haar_content_self {K₀ : positive_compacts G} : haar_content K₀ ⟨K₀.1, K₀.2.1⟩ = 1 := by { simp_rw [← ennreal.coe_one, haar_content_apply, ennreal.coe_eq_coe, chaar_self], refl } /-- The variant of `is_left_invariant_chaar` for `haar_content` -/ +@[to_additive] lemma is_left_invariant_haar_content {K₀ : positive_compacts G} (g : G) (K : compacts G) : haar_content K₀ (K.map _ $ continuous_mul_left g) = haar_content K₀ K := by simpa only [ennreal.coe_eq_coe, ←nnreal.coe_eq, haar_content_apply] using is_left_invariant_chaar g K +@[to_additive] lemma haar_content_outer_measure_self_pos {K₀ : positive_compacts G} : 0 < (haar_content K₀).outer_measure K₀.1 := begin @@ -459,15 +500,19 @@ open haar variables [topological_space G] [t2_space G] [topological_group G] [measurable_space G] [borel_space G] -/-- the Haar measure on `G`, scaled so that `haar_measure K₀ K₀ = 1`. -/ +/-- The Haar measure on the locally compact group `G`, scaled so that `haar_measure K₀ K₀ = 1`. -/ +@[to_additive "The Haar measure on the locally compact additive group `G`, +scaled so that `add_haar_measure K₀ K₀ = 1`."] def haar_measure (K₀ : positive_compacts G) : measure G := ((haar_content K₀).outer_measure K₀.1)⁻¹ • (haar_content K₀).measure +@[to_additive] lemma haar_measure_apply {K₀ : positive_compacts G} {s : set G} (hs : measurable_set s) : haar_measure K₀ s = (haar_content K₀).outer_measure s / (haar_content K₀).outer_measure K₀.1 := by simp only [haar_measure, hs, div_eq_mul_inv, mul_comm, content.measure_apply, algebra.id.smul_eq_mul, pi.smul_apply, measure.coe_smul] +@[to_additive] lemma is_mul_left_invariant_haar_measure (K₀ : positive_compacts G) : is_mul_left_invariant (haar_measure K₀) := begin @@ -478,6 +523,7 @@ begin apply is_left_invariant_haar_content, end +@[to_additive] lemma haar_measure_self [locally_compact_space G] {K₀ : positive_compacts G} : haar_measure K₀ K₀.1 = 1 := begin @@ -486,6 +532,7 @@ begin { exact ne_of_lt (content.outer_measure_lt_top_of_is_compact _ K₀.2.1) } end +@[to_additive] lemma haar_measure_pos_of_is_open [locally_compact_space G] {K₀ : positive_compacts G} {U : set G} (hU : is_open U) (h2U : U.nonempty) : 0 < haar_measure K₀ U := begin @@ -497,6 +544,7 @@ begin end /-- The Haar measure is regular. -/ +@[to_additive] instance regular_haar_measure [locally_compact_space G] {K₀ : positive_compacts G} : (haar_measure K₀).regular := begin @@ -508,9 +556,9 @@ end section unique variables [locally_compact_space G] [second_countable_topology G] {μ : measure G} [sigma_finite μ] - /-- The Haar measure is unique up to scaling. More precisely: every σ-finite left invariant measure is a scalar multiple of the Haar measure. -/ +@[to_additive] theorem haar_measure_unique (hμ : is_mul_left_invariant μ) (K₀ : positive_compacts G) : μ = μ K₀.1 • haar_measure K₀ := begin @@ -520,7 +568,8 @@ begin rw [← this (by norm_num), smul_apply], end -theorem regular_of_left_invariant (hμ : is_mul_left_invariant μ) {K} (hK : is_compact K) +@[to_additive] +theorem regular_of_is_mul_left_invariant (hμ : is_mul_left_invariant μ) {K} (hK : is_compact K) (h2K : (interior K).nonempty) (hμK : μ K < ∞) : regular μ := begin rw [haar_measure_unique hμ ⟨K, hK, h2K⟩], diff --git a/src/measure_theory/lp_space.lean b/src/measure_theory/lp_space.lean index 2372d09c92dab..3475758e81576 100644 --- a/src/measure_theory/lp_space.lean +++ b/src/measure_theory/lp_space.lean @@ -261,7 +261,7 @@ section const lemma snorm'_const (c : F) (hq_pos : 0 < q) : snorm' (λ x : α , c) q μ = (nnnorm c : ℝ≥0∞) * (μ set.univ) ^ (1/q) := begin - rw [snorm', lintegral_const, @ennreal.mul_rpow_of_nonneg _ _ (1/q) (by simp [hq_pos.le])], + rw [snorm', lintegral_const, ennreal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)], congr, rw ←ennreal.rpow_mul, suffices hq_cancel : q * (1/q) = 1, by rw [hq_cancel, ennreal.rpow_one], @@ -555,7 +555,7 @@ begin simp_rw snorm', congr' 1, refine lintegral_trim hm _, - refine @measurable.pow_const _ m _ _ _ _ _ _ _ (@measurable.coe_nnreal_ennreal _ m _ _) _, + refine @measurable.pow_const _ _ _ _ _ _ _ m _ (@measurable.coe_nnreal_ennreal _ m _ _) _, exact @measurable.nnnorm E _ _ _ _ m _ hf, end @@ -665,7 +665,7 @@ begin rw [snorm', ←ennreal.rpow_one (snorm_ess_sup f μ)], nth_rewrite 1 ←mul_inv_cancel (ne_of_lt hq_pos).symm, rw [ennreal.rpow_mul, one_div, - ←@ennreal.mul_rpow_of_nonneg _ _ q⁻¹ (by simp [hq_pos.le])], + ←ennreal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ q⁻¹)], refine ennreal.rpow_le_rpow _ (by simp [hq_pos.le]), rwa lintegral_const at h_le, end @@ -774,7 +774,7 @@ calc (∫⁻ a, ↑(nnnorm ((f + g) a)) ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ a, (((λ a, (nnnorm (f a) : ℝ≥0∞)) + (λ a, (nnnorm (g a) : ℝ≥0∞))) a) ^ q ∂μ) ^ (1 / q) : begin - refine @ennreal.rpow_le_rpow _ _ (1/q) _ (by simp [le_trans zero_le_one hq1]), + refine ennreal.rpow_le_rpow _ (by simp [le_trans zero_le_one hq1] : 0 ≤ 1 / q), refine lintegral_mono (λ a, ennreal.rpow_le_rpow _ (le_trans zero_le_one hq1)), simp [←ennreal.coe_add, nnnorm_add_le], end @@ -828,18 +828,18 @@ calc (∫⁻ a, ↑(nnnorm ((f + g) a)) ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ a, (((λ a, (nnnorm (f a) : ℝ≥0∞)) + (λ a, (nnnorm (g a) : ℝ≥0∞))) a) ^ q ∂μ) ^ (1 / q) : begin - refine @ennreal.rpow_le_rpow _ _ (1/q) _ (by simp [hq_pos.le]), + refine ennreal.rpow_le_rpow _ (by simp [hq_pos.le] : 0 ≤ 1 / q), refine lintegral_mono (λ a, ennreal.rpow_le_rpow _ hq_pos.le), simp [←ennreal.coe_add, nnnorm_add_le], end ... ≤ (∫⁻ a, (nnnorm (f a) : ℝ≥0∞) ^ q + (nnnorm (g a) : ℝ≥0∞) ^ q ∂μ) ^ (1 / q) : begin - refine @ennreal.rpow_le_rpow _ _ (1/q) (lintegral_mono (λ a, _)) (by simp [hq_pos.le]), + refine ennreal.rpow_le_rpow (lintegral_mono (λ a, _)) (by simp [hq_pos.le] : 0 ≤ 1 / q), exact ennreal.rpow_add_le_add_rpow _ _ hq_pos hq1, end ... < ∞ : begin - refine @ennreal.rpow_lt_top_of_nonneg _ (1/q) (by simp [hq_pos.le]) _, + refine ennreal.rpow_lt_top_of_nonneg (by simp [hq_pos.le] : 0 ≤ 1 / q) _, rw [lintegral_add' (hf.ennnorm.pow_const q) (hg.ennnorm.pow_const q), ennreal.add_ne_top, ←lt_top_iff_ne_top, ←lt_top_iff_ne_top], @@ -883,21 +883,20 @@ section normed_space variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] -lemma snorm'_const_smul {f : α → F} (c : 𝕜) (hq0_lt : 0 < q) : +lemma snorm'_const_smul {f : α → F} (c : 𝕜) (hq_pos : 0 < q) : snorm' (c • f) q μ = (nnnorm c : ℝ≥0∞) * snorm' f q μ := begin rw snorm', simp_rw [pi.smul_apply, nnnorm_smul, ennreal.coe_mul, - ennreal.mul_rpow_of_nonneg _ _ (le_of_lt hq0_lt)], + ennreal.mul_rpow_of_nonneg _ _ hq_pos.le], suffices h_integral : ∫⁻ a, ↑(nnnorm c) ^ q * ↑(nnnorm (f a)) ^ q ∂μ = (nnnorm c : ℝ≥0∞)^q * ∫⁻ a, (nnnorm (f a)) ^ q ∂μ, { apply_fun (λ x, x ^ (1/q)) at h_integral, - rw [h_integral, @ennreal.mul_rpow_of_nonneg _ _ (1/q) (by simp [le_of_lt hq0_lt])], + rw [h_integral, ennreal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ 1 / q)], congr, - simp_rw [←ennreal.rpow_mul, one_div, mul_inv_cancel (ne_of_lt hq0_lt).symm, - ennreal.rpow_one], }, + simp_rw [←ennreal.rpow_mul, one_div, mul_inv_cancel hq_pos.ne.symm, ennreal.rpow_one], }, rw lintegral_const_mul', - rw ennreal.coe_rpow_of_nonneg _ hq0_lt.le, + rw ennreal.coe_rpow_of_nonneg _ hq_pos.le, exact ennreal.coe_ne_top, end @@ -1712,7 +1711,7 @@ lemma snorm'_lim_le_liminf_snorm' {E} [measurable_space E] snorm' f_lim p μ ≤ at_top.liminf (λ n, snorm' (f n) p μ) := begin rw snorm'_lim_eq_lintegral_liminf hp_pos.le h_lim, - rw [←@ennreal.le_rpow_one_div_iff _ _ (1/p) (by simp [hp_pos]), one_div_one_div], + rw [←ennreal.le_rpow_one_div_iff (by simp [hp_pos] : 0 < 1 / p), one_div_one_div], refine (lintegral_liminf_le' (λ m, ((hf m).ennnorm.pow_const _))).trans_eq _, have h_pow_liminf : at_top.liminf (λ n, snorm' (f n) p μ) ^ p = at_top.liminf (λ n, (snorm' (f n) p μ) ^ p), @@ -1904,7 +1903,7 @@ private lemma lintegral_rpow_tsum_coe_nnnorm_sub_le_tsum {f : ℕ → α → E} begin have hp_pos : 0 < p := zero_lt_one.trans_le hp1, suffices h_pow : ∫⁻ a, (∑' i, nnnorm (f (i + 1) a - f i a) : ℝ≥0∞)^p ∂μ ≤ (∑' i, B i) ^ p, - by rwa [←@ennreal.le_rpow_one_div_iff _ _ (1/p) (by simp [hp_pos]), one_div_one_div], + by rwa [←ennreal.le_rpow_one_div_iff (by simp [hp_pos] : 0 < 1 / p), one_div_one_div], have h_tsum_1 : ∀ g : ℕ → ℝ≥0∞, ∑' i, g i = at_top.liminf (λ n, ∑ i in finset.range (n + 1), g i), by { intro g, rw [ennreal.tsum_eq_liminf_sum_nat, ← liminf_nat_add _ 1], }, @@ -1936,13 +1935,13 @@ begin { have h_tsum_lt_top : (∑' i, B i) ^ p < ∞, from ennreal.rpow_lt_top_of_nonneg hp_pos.le (lt_top_iff_ne_top.mp hB), refine lt_of_le_of_lt _ h_tsum_lt_top, - rwa [←@ennreal.le_rpow_one_div_iff _ _ (1/p) (by simp [hp_pos]), one_div_one_div] at h, }, + rwa [←ennreal.le_rpow_one_div_iff (by simp [hp_pos] : 0 < 1 / p), one_div_one_div] at h, }, have rpow_ae_lt_top : ∀ᵐ x ∂μ, (∑' i, nnnorm (f (i + 1) x - f i x) : ℝ≥0∞)^p < ∞, { refine ae_lt_top' (ae_measurable.pow_const _ _) h_integral, exact ae_measurable.ennreal_tsum (λ n, ((hf (n+1)).sub (hf n)).ennnorm), }, refine rpow_ae_lt_top.mono (λ x hx, _), rwa [←ennreal.lt_rpow_one_div_iff hp_pos, - @ennreal.top_rpow_of_pos (1/p) (by simp [hp_pos])] at hx, + ennreal.top_rpow_of_pos (by simp [hp_pos] : 0 < 1 / p)] at hx, end lemma ae_tendsto_of_cauchy_snorm' [complete_space E] {f : ℕ → α → E} {p : ℝ} @@ -2188,7 +2187,7 @@ ae_eq_fun.coe_fn_mk f _ lemma to_Lp_norm_le [nondiscrete_normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] [fact (1 ≤ p)] : - ∥@to_Lp _ E _ p μ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ := + ∥(to_Lp p μ 𝕜 : (α →ᵇ E) →L[𝕜] (Lp E p μ))∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ := linear_map.mk_continuous_norm_le _ ((measure_univ_nnreal μ) ^ (p.to_real)⁻¹).coe_nonneg _ end bounded_continuous_function @@ -2245,13 +2244,14 @@ rfl variables [nondiscrete_normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] lemma to_Lp_norm_eq_to_Lp_norm_coe : - ∥@to_Lp _ E _ p μ _ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥ - = ∥@bounded_continuous_function.to_Lp _ E _ p μ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥ := + ∥(to_Lp p μ 𝕜 : C(α, E) →L[𝕜] (Lp E p μ))∥ + = ∥(bounded_continuous_function.to_Lp p μ 𝕜 : (α →ᵇ E) →L[𝕜] (Lp E p μ))∥ := continuous_linear_map.op_norm_comp_linear_isometry_equiv _ _ /-- Bound for the operator norm of `continuous_map.to_Lp`. -/ lemma to_Lp_norm_le : - ∥@to_Lp _ E _ p μ _ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ := + ∥(to_Lp p μ 𝕜 : C(α, E) →L[𝕜] (Lp E p μ))∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ := by { rw to_Lp_norm_eq_to_Lp_norm_coe, exact bounded_continuous_function.to_Lp_norm_le μ } end continuous_map +--(to_Lp p μ 𝕜 : (α →ᵇ E) →L[𝕜] (Lp E p μ)) diff --git a/src/measure_theory/prod_group.lean b/src/measure_theory/prod_group.lean index 7da164947ee9d..7f553a4158b93 100644 --- a/src/measure_theory/prod_group.lean +++ b/src/measure_theory/prod_group.lean @@ -42,11 +42,12 @@ namespace measure_theory open measure variables {G : Type*} [topological_space G] [measurable_space G] [second_countable_topology G] - [borel_space G] [group G] [topological_group G] +variables [borel_space G] [group G] [topological_group G] variables {μ ν : measure G} [sigma_finite ν] [sigma_finite μ] /-- This condition is part of the definition of a measurable group in [Halmos, §59]. There, the map in this lemma is called `S`. -/ +@[to_additive map_prod_sum_eq] lemma map_prod_mul_eq (hν : is_mul_left_invariant ν) : map (λ z : G × G, (z.1, z.1 * z.2)) (μ.prod ν) = μ.prod ν := begin @@ -60,6 +61,7 @@ end /-- The function we are mapping along is `SR` in [Halmos, §59], where `S` is the map in `map_prod_mul_eq` and `R` is `prod.swap`. -/ +@[to_additive map_prod_add_eq_swap] lemma map_prod_mul_eq_swap (hμ : is_mul_left_invariant μ) : map (λ z : G × G, (z.2, z.2 * z.1)) (μ.prod ν) = ν.prod μ := begin @@ -70,6 +72,7 @@ end /-- The function we are mapping along is `S⁻¹` in [Halmos, §59], where `S` is the map in `map_prod_mul_eq`. -/ +@[to_additive map_prod_neg_add_eq] lemma map_prod_inv_mul_eq (hν : is_mul_left_invariant ν) : map (λ z : G × G, (z.1, z.1⁻¹ * z.2)) (μ.prod ν) = μ.prod ν := (homeomorph.shear_mul_right G).to_measurable_equiv.map_apply_eq_iff_map_symm_apply_eq.mp $ @@ -77,6 +80,7 @@ lemma map_prod_inv_mul_eq (hν : is_mul_left_invariant ν) : /-- The function we are mapping along is `S⁻¹R` in [Halmos, §59], where `S` is the map in `map_prod_mul_eq` and `R` is `prod.swap`. -/ +@[to_additive map_prod_neg_add_eq_swap] lemma map_prod_inv_mul_eq_swap (hμ : is_mul_left_invariant μ) : map (λ z : G × G, (z.2, z.2⁻¹ * z.1)) (μ.prod ν) = ν.prod μ := begin @@ -88,6 +92,7 @@ end /-- The function we are mapping along is `S⁻¹RSR` in [Halmos, §59], where `S` is the map in `map_prod_mul_eq` and `R` is `prod.swap`. -/ +@[to_additive map_prod_add_neg_eq] lemma map_prod_mul_inv_eq (hμ : is_mul_left_invariant μ) (hν : is_mul_left_invariant ν) : map (λ z : G × G, (z.2 * z.1, z.1⁻¹)) (μ.prod ν) = μ.prod ν := begin @@ -100,6 +105,7 @@ begin map_prod_inv_mul_eq_swap hν] end +@[to_additive] lemma measure_null_of_measure_inv_null (hμ : is_mul_left_invariant μ) {E : set G} (hE : measurable_set E) (h2E : μ ((λ x, x⁻¹) ⁻¹' E) = 0) : μ E = 0 := begin @@ -112,6 +118,7 @@ begin convert lintegral_zero, ext1 x, refine measure_mono_null (inter_subset_right _ _) h2E end +@[to_additive] lemma measure_inv_null (hμ : is_mul_left_invariant μ) {E : set G} (hE : measurable_set E) : μ ((λ x, x⁻¹) ⁻¹' E) = 0 ↔ μ E = 0 := begin @@ -122,6 +129,7 @@ begin exact set.inv_inv end +@[to_additive] lemma measurable_measure_mul_right {E : set G} (hE : measurable_set E) : measurable (λ x, μ ((λ y, y * x) ⁻¹' E)) := begin @@ -132,6 +140,7 @@ begin exact measurable_const.prod_mk (measurable_fst.mul measurable_snd) (measurable_set.univ.prod hE) end +@[to_additive] lemma lintegral_lintegral_mul_inv (hμ : is_mul_left_invariant μ) (hν : is_mul_left_invariant ν) (f : G → G → ℝ≥0∞) (hf : ae_measurable (uncurry f) (μ.prod ν)) : ∫⁻ x, ∫⁻ y, f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ x, ∫⁻ y, f x y ∂ν ∂μ := @@ -146,6 +155,7 @@ begin exact lintegral_map' (hf.mono' (map_prod_mul_inv_eq hμ hν).absolutely_continuous) h, end +@[to_additive] lemma measure_mul_right_null (hμ : is_mul_left_invariant μ) {E : set G} (hE : measurable_set E) (y : G) : μ ((λ x, x * y) ⁻¹' E) = 0 ↔ μ E = 0 := begin @@ -154,6 +164,7 @@ begin convert iff.rfl using 3, ext x, simp, end +@[to_additive] lemma measure_mul_right_ne_zero (hμ : is_mul_left_invariant μ) {E : set G} (hE : measurable_set E) (h2E : μ E ≠ 0) (y : G) : μ ((λ x, x * y) ⁻¹' E) ≠ 0 := (not_iff_not_of_iff (measure_mul_right_null hμ hE y)).mpr h2E @@ -167,6 +178,7 @@ lemma measure_mul_right_ne_zero (hμ : is_mul_left_invariant μ) {E : set G} (hE inequality. For this reason, we use a compact `E` instead of a measurable `E` as in [Halmos], and additionally assume that `ν` is a regular measure (we only need that it is finite on compact sets). -/ +@[to_additive] lemma measure_lintegral_div_measure [t2_space G] (hμ : is_mul_left_invariant μ) (hν : is_mul_left_invariant ν) [regular ν] {E : set G} (hE : is_compact E) (h2E : ν E ≠ 0) (f : G → ℝ≥0∞) (hf : measurable f) : @@ -186,7 +198,7 @@ begin λ x, measurable_const.indicator (measurable_mul_const _ Em), have : ∀ x y, E.indicator (λ (z : G), (1 : ℝ≥0∞)) (y * x) = ((λ z, z * x) ⁻¹' E).indicator (λ (b : G), 1) y, - { intros x y, symmetry, convert indicator_comp_right (λ y, y * x), ext1 z, simp }, + { intros x y, symmetry, convert indicator_comp_right (λ y, y * x), ext1 z, refl }, have h3E : ∀ y, ν ((λ x, x * y) ⁻¹' E) ≠ ∞ := λ y, ennreal.lt_top_iff_ne_top.mp (regular.lt_top_of_is_compact $ (homeomorph.mul_right _).compact_preimage.mpr hE), @@ -198,6 +210,7 @@ end /-- This is roughly the uniqueness (up to a scalar) of left invariant Borel measures on a second countable locally compact group. The uniqueness of Haar measure is proven from this in `measure_theory.measure.haar_measure_unique` -/ +@[to_additive] lemma measure_mul_measure_eq [t2_space G] (hμ : is_mul_left_invariant μ) (hν : is_mul_left_invariant ν) [regular ν] {E F : set G} (hE : is_compact E) (hF : measurable_set F) (h2E : ν E ≠ 0) : μ E * ν F = ν E * μ F := diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean index 6ead35469fbc5..3413057de13ab 100644 --- a/src/topology/algebra/group.lean +++ b/src/topology/algebra/group.lean @@ -636,7 +636,8 @@ end /-- Every locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis. -/ -@[priority 100] instance separable_locally_compact_group.sigma_compact_space +@[priority 100, to_additive separable_locally_compact_add_group.sigma_compact_space] +instance separable_locally_compact_group.sigma_compact_space [separable_space G] [locally_compact_space G] : sigma_compact_space G := begin obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G),