feat(measure_theory/integral): integral composed with smul (#17455)

src/analysis/box_integral/integrability.lean

@@ -171,7 +171,8 @@ lemma has_box_integral (f : simple_func (ι → ℝ) E) (μ : measure (ι → 
   has_integral.{u v v} I l f μ.to_box_additive.to_smul (f.integral (μ.restrict I)) :=
 begin
   induction f using measure_theory.simple_func.induction with y s hs f g hd hfi hgi,
-  { simpa [function.const, measure.restrict_apply hs]
+  { simpa only [measure.restrict_apply hs, const_zero, integral_piecewise_zero, integral_const,
+      measure.restrict_apply, measurable_set.univ, set.univ_inter]
       using box_integral.has_integral_indicator_const l hl hs I y μ },
   { borelize E, haveI := fact.mk (I.measure_coe_lt_top μ),
     rw integral_add,

src/measure_theory/function/locally_integrable.lean

@@ -56,6 +56,28 @@ begin
     exact ⟨K, nhds_within_le_nhds hK, h2K⟩ }
 end
 
+lemma locally_integrable_const [is_locally_finite_measure μ] (c : E) :
+  locally_integrable (λ x, c) μ :=
+λ K hK, by simp only [integrable_on_const, hK.measure_lt_top, or_true]
+
+lemma locally_integrable.indicator (hf : locally_integrable f μ)
+  {s : set X} (hs : measurable_set s) : locally_integrable (s.indicator f) μ :=
+λ K hK, (hf hK).indicator hs
+
+theorem locally_integrable_map_homeomorph [borel_space X] [borel_space Y]
+  (e : X ≃ₜ Y) {f : Y → E} {μ : measure X} :
+  locally_integrable f (measure.map e μ) ↔ locally_integrable (f ∘ e) μ :=
+begin
+  refine ⟨λ h k hk, _, λ h k hk, _⟩,
+  { have : is_compact (e.symm ⁻¹' k), from (homeomorph.is_compact_preimage _).2 hk,
+    convert (integrable_on_map_equiv e.to_measurable_equiv).1 (h this) using 1,
+    simp only [←preimage_comp, homeomorph.to_measurable_equiv_coe, homeomorph.symm_comp_self,
+      preimage_id_eq, id.def] },
+  { apply (integrable_on_map_equiv e.to_measurable_equiv).2,
+    have : is_compact (e ⁻¹' k), from (homeomorph.is_compact_preimage _).2 hk,
+    exact h this }
+end
+
 section real
 variables [opens_measurable_space X] {A K : set X} {g g' : X → ℝ}
 

src/measure_theory/group/measure.lean

@@ -26,8 +26,8 @@ We also give analogues of all these notions in the additive world.
 
 noncomputable theory
 
-open_locale ennreal pointwise big_operators
-open has_inv set function measure_theory.measure
+open_locale ennreal pointwise big_operators topological_space
+open has_inv set function measure_theory.measure filter
 
 variables {G : Type*} [measurable_space G]
 
@@ -213,6 +213,15 @@ calc μ ((λ h, h * g) ⁻¹' A) = map (λ h, h * g) μ A :
   ((measurable_equiv.mul_right g).map_apply A).symm
 ... = μ A : by rw map_mul_right_eq_self μ g
 
+@[simp, to_additive]
+lemma measure_smul (μ : measure G) [is_mul_left_invariant μ] (g : G) (A : set G) :
+  μ (g • A) = μ A :=
+begin
+  convert measure_preimage_mul μ (g⁻¹) A,
+  ext x,
+  simp only [mem_smul_set_iff_inv_smul_mem, smul_eq_mul, mem_preimage]
+end
+
 @[to_additive]
 lemma map_mul_left_ae (μ : measure G) [is_mul_left_invariant μ] (x : G) :
   filter.map (λ h, x * h) μ.ae = μ.ae :=
@@ -460,6 +469,59 @@ lemma measure_lt_top_of_is_compact_of_is_mul_left_invariant'
 measure_lt_top_of_is_compact_of_is_mul_left_invariant (interior U) is_open_interior hU
   ((measure_mono (interior_subset)).trans_lt (lt_top_iff_ne_top.2 h)).ne hK
 
+/-- In a noncompact locally compact group, a left-invariant measure which is positive
+on open sets has infinite mass. -/
+@[simp, to_additive "In a noncompact locally compact additive group, a left-invariant measure which
+is positive on open sets has infinite mass."]
+lemma measure_univ_of_is_mul_left_invariant [locally_compact_space G] [noncompact_space G]
+  (μ : measure G) [is_open_pos_measure μ] [μ.is_mul_left_invariant] :
+  μ univ = ∞ :=
+begin
+  /- Consider a closed compact set `K` with nonempty interior. For any compact set `L`, one may
+  find `g = g (L)` such that `L` is disjoint from `g • K`. Iterating this, one finds
+  infinitely many translates of `K` which are disjoint from each other. As they all have the
+  same positive mass, it follows that the space has infinite measure. -/
+  obtain ⟨K, hK, Kclosed, Kint⟩ : ∃ (K : set G), is_compact K ∧ is_closed K ∧ (1 : G) ∈ interior K,
+  { rcases local_is_compact_is_closed_nhds_of_group (is_open_univ.mem_nhds (mem_univ (1 : G)))
+      with ⟨K, hK⟩,
+    exact ⟨K, hK.1, hK.2.1, hK.2.2.2⟩, },
+  have K_pos : 0 < μ K, from measure_pos_of_nonempty_interior _ ⟨_, Kint⟩,
+  have A : ∀ (L : set G), is_compact L → ∃ (g : G), disjoint L (g • K),
+    from λ L hL, exists_disjoint_smul_of_is_compact hL hK,
+  choose! g hg using A,
+  set L : ℕ → set G := λ n, (λ T, T ∪ (g T • K))^[n] K with hL,
+  have Lcompact : ∀ n, is_compact (L n),
+  { assume n,
+    induction n with n IH,
+    { exact hK },
+    { simp_rw [hL, iterate_succ'],
+      apply is_compact.union IH (hK.smul (g (L n))) } },
+  have Lclosed : ∀ n, is_closed (L n),
+  { assume n,
+    induction n with n IH,
+    { exact Kclosed },
+    { simp_rw [hL, iterate_succ'],
+      apply is_closed.union IH (Kclosed.smul (g (L n))) } },
+  have M : ∀ n, μ (L n) = (n + 1 : ℕ) * μ K,
+  { assume n,
+    induction n with n IH,
+    { simp only [L, one_mul, algebra_map.coe_one, iterate_zero, id.def] },
+    { calc μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) :
+        begin
+          simp_rw [hL, iterate_succ'],
+          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurable_set
+        end
+      ... = ((n + 1) + 1 : ℕ) * μ K :
+        by simp only [IH, measure_smul, add_mul, nat.cast_add, algebra_map.coe_one, one_mul] } },
+  have N : tendsto (λ n, μ (L n)) at_top (𝓝 (∞ * μ K)),
+  { simp_rw [M],
+    apply ennreal.tendsto.mul_const _ (or.inl ennreal.top_ne_zero),
+    exact ennreal.tendsto_nat_nhds_top.comp (tendsto_add_at_top_nat _) },
+  simp only [ennreal.top_mul, K_pos.ne', if_false] at N,
+  apply top_le_iff.1,
+  exact le_of_tendsto' N (λ n, measure_mono (subset_univ _)),
+end
+
 end topological_group
 
 section comm_group
@@ -543,8 +605,6 @@ lemma is_haar_measure_of_is_compact_nonempty_interior [topological_group G] [bor
     λ L hL, measure_lt_top_of_is_compact_of_is_mul_left_invariant' h'K h' hL,
   to_is_open_pos_measure := is_open_pos_measure_of_mul_left_invariant_of_compact K hK h }
 
-open filter
-
 /-- The image of a Haar measure under a continuous surjective proper group homomorphism is again
 a Haar measure. See also `mul_equiv.is_haar_measure_map`. -/
 @[to_additive "The image of an additive Haar measure under a continuous surjective proper additive
@@ -594,8 +654,6 @@ instance {G : Type*} [group G] [topological_space G] {mG : measurable_space G}
   [has_measurable_mul G] [has_measurable_mul H] :
   is_haar_measure (μ.prod ν) := {}
 
-open_locale topological_space
-
 /-- If the neutral element of a group is not isolated, then a Haar measure on this group has
 no atoms.
 

src/measure_theory/integral/integrable_on.lean

@@ -209,13 +209,17 @@ lemma integrable_indicator_iff (hs : measurable_set s) :
 by simp [integrable_on, integrable, has_finite_integral, nnnorm_indicator_eq_indicator_nnnorm,
   ennreal.coe_indicator, lintegral_indicator _ hs, ae_strongly_measurable_indicator_iff hs]
 
-lemma integrable_on.indicator (h : integrable_on f s μ) (hs : measurable_set s) :
+lemma integrable_on.integrable_indicator (h : integrable_on f s μ) (hs : measurable_set s) :
   integrable (indicator s f) μ :=
 (integrable_indicator_iff hs).2 h
 
 lemma integrable.indicator (h : integrable f μ) (hs : measurable_set s) :
   integrable (indicator s f) μ :=
-h.integrable_on.indicator hs
+h.integrable_on.integrable_indicator hs
+
+lemma integrable_on.indicator (h : integrable_on f s μ) (ht : measurable_set t) :
+  integrable_on (indicator t f) s μ :=
+integrable.indicator h ht
 
 lemma integrable_indicator_const_Lp {E} [normed_add_comm_group E]
   {p : ℝ≥0∞} {s : set α} (hs : measurable_set s) (hμs : μ s ≠ ∞) (c : E) :

src/measure_theory/integral/set_integral.lean

@@ -135,7 +135,7 @@ begin
   { rwa [integral_undef, integral_undef],
     rwa integrable_indicator_iff hs },
   calc ∫ x, indicator s f x ∂μ = ∫ x in s, indicator s f x ∂μ + ∫ x in sᶜ, indicator s f x ∂μ :
-    (integral_add_compl hs (hfi.indicator hs)).symm
+    (integral_add_compl hs (hfi.integrable_indicator hs)).symm
   ... = ∫ x in s, f x ∂μ + ∫ x in sᶜ, 0 ∂μ :
     congr_arg2 (+) (integral_congr_ae (indicator_ae_eq_restrict hs))
       (integral_congr_ae (indicator_ae_eq_restrict_compl hs))
@@ -168,7 +168,7 @@ lemma integral_piecewise [decidable_pred (∈ s)] (hs : measurable_set s)
   {f g : α → E} (hf : integrable_on f s μ) (hg : integrable_on g sᶜ μ) :
   ∫ x, s.piecewise f g x ∂μ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, g x ∂μ :=
 by rw [← set.indicator_add_compl_eq_piecewise,
-  integral_add' (hf.indicator hs) (hg.indicator hs.compl),
+  integral_add' (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl),
   integral_indicator hs, integral_indicator hs.compl]
 
 lemma tendsto_set_integral_of_monotone {ι : Type*} [countable ι] [semilattice_sup ι]
@@ -839,6 +839,15 @@ L.to_continuous_linear_map.integral_comp_comm' L.antilipschitz _
 
 end linear_isometry
 
+namespace continuous_linear_equiv
+
+variables [complete_space F] [normed_space ℝ F] [complete_space E] [normed_space ℝ E]
+
+lemma integral_comp_comm (L : E ≃L[𝕜] F) (φ : α → E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
+L.to_continuous_linear_map.integral_comp_comm' L.antilipschitz _
+
+end continuous_linear_equiv
+
 variables [complete_space E] [normed_space ℝ E] [complete_space F] [normed_space ℝ F]
 
 @[norm_cast] lemma integral_of_real {f : α → ℝ} : ∫ a, (f a : 𝕜) ∂μ = ↑∫ a, f a ∂μ :=

src/measure_theory/measure/haar_lebesgue.lean

@@ -324,6 +324,7 @@ equal to `μ s` times the absolute value of the determinant of `f`. -/
 
 variables {E : Type*} [normed_add_comm_group E] [measurable_space E] [normed_space ℝ E]
   [finite_dimensional ℝ E] [borel_space E] (μ : measure E) [is_add_haar_measure μ]
+  {F : Type*} [normed_add_comm_group F] [normed_space ℝ F] [complete_space F]
 
 lemma map_add_haar_smul {r : ℝ} (hr : r ≠ 0) :
   measure.map ((•) r) μ = ennreal.of_real (abs (r ^ (finrank ℝ E))⁻¹) • μ :=
@@ -369,6 +370,51 @@ calc μ (affine_map.homothety x r '' s) = μ ((λ y, y + x) '' (r • ((λ y, y
 ... = ennreal.of_real (abs (r ^ (finrank ℝ E))) * μ s :
   by simp only [image_add_right, measure_preimage_add_right, add_haar_smul]
 
+/-- The integral of `f (R • x)` with respect to an additive Haar measure is a multiple of the
+integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
+thanks to the convention that a non-integrable function has integral zero. -/
+lemma integral_comp_smul (f : E → F) (R : ℝ) :
+  ∫ x, f (R • x) ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ x, f x ∂μ :=
+begin
+  rcases eq_or_ne R 0 with rfl|hR,
+  { simp only [zero_smul, integral_const],
+    rcases nat.eq_zero_or_pos (finrank ℝ E) with hE|hE,
+    { haveI : subsingleton E, from finrank_zero_iff.1 hE,
+      have : f = (λ x, f 0), { ext x, rw subsingleton.elim x 0 },
+      conv_rhs { rw this },
+      simp only [hE, pow_zero, inv_one, abs_one, one_smul, integral_const] },
+    { haveI : nontrivial E, from finrank_pos_iff.1 hE,
+      simp only [zero_pow hE, measure_univ_of_is_add_left_invariant, ennreal.top_to_real, zero_smul,
+        inv_zero, abs_zero]} },
+  { calc ∫ x, f (R • x) ∂μ = ∫ y, f y ∂(measure.map (λ x, R • x) μ) :
+      (integral_map_equiv (homeomorph.smul (is_unit_iff_ne_zero.2 hR).unit)
+        .to_measurable_equiv f).symm
+    ... = |(R ^ finrank ℝ E)⁻¹| • ∫ x, f x ∂μ :
+      by simp only [map_add_haar_smul μ hR, integral_smul_measure, ennreal.to_real_of_real,
+                    abs_nonneg] }
+end
+
+/-- The integral of `f (R • x)` with respect to an additive Haar measure is a multiple of the
+integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
+thanks to the convention that a non-integrable function has integral zero. -/
+lemma integral_comp_smul_of_nonneg (f : E → F) (R : ℝ) {hR : 0 ≤ R} :
+  ∫ x, f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ x, f x ∂μ :=
+by rw [integral_comp_smul μ f R, abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR _))]
+
+/-- The integral of `f (R⁻¹ • x)` with respect to an additive Haar measure is a multiple of the
+integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
+thanks to the convention that a non-integrable function has integral zero. -/
+lemma integral_comp_inv_smul (f : E → F) (R : ℝ) :
+  ∫ x, f (R⁻¹ • x) ∂μ = |(R ^ finrank ℝ E)| • ∫ x, f x ∂μ :=
+by rw [integral_comp_smul μ f (R⁻¹), inv_pow, inv_inv]
+
+/-- The integral of `f (R⁻¹ • x)` with respect to an additive Haar measure is a multiple of the
+integral of `f`. The formula we give works even when `f` is not integrable or `R = 0`
+thanks to the convention that a non-integrable function has integral zero. -/
+lemma integral_comp_inv_smul_of_nonneg (f : E → F) {R : ℝ} (hR : 0 ≤ R) :
+  ∫ x, f (R⁻¹ • x) ∂μ = R ^ finrank ℝ E • ∫ x, f x ∂μ :=
+by rw [integral_comp_inv_smul μ f R, abs_of_nonneg ((pow_nonneg hR _))]
+
 /-! 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. -/
 

src/probability/martingale/borel_cantelli.lean

@@ -321,7 +321,8 @@ end
 lemma integrable_process (μ : measure Ω) [is_finite_measure μ]
   (hs : ∀ n, measurable_set[ℱ n] (s n)) (n : ℕ) :
   integrable (process s n) μ :=
-integrable_finset_sum' _ $ λ k hk, integrable_on.indicator (integrable_const 1) $ ℱ.le _ _ $ hs _
+integrable_finset_sum' _ $ λ k hk,
+  integrable_on.integrable_indicator (integrable_const 1) $ ℱ.le _ _ $ hs _
 
 end borel_cantelli
 

src/topology/algebra/const_mul_action.lean

@@ -128,6 +128,7 @@ instance {ι : Type*} {γ : ι → Type*} [∀ i, topological_space (γ i)] [Π
   [∀ i, has_continuous_const_smul M (γ i)] : has_continuous_const_smul M (Π i, γ i) :=
 ⟨λ _, continuous_pi $ λ i, (continuous_apply i).const_smul _⟩
 
+@[to_additive]
 lemma is_compact.smul {α β} [has_smul α β] [topological_space β]
   [has_continuous_const_smul α β] (a : α) {s : set β}
   (hs : is_compact s) : is_compact (a • s) := hs.image (continuous_id'.const_smul a)

src/topology/algebra/group.lean

@@ -1209,6 +1209,49 @@ begin
   exact mem_interior_iff_mem_nhds.1 hy
 end
 
+/-- Given two compact sets in a noncompact topological group, there is a translate of the second
+one that is disjoint from the first one. -/
+@[to_additive "Given two compact sets in a noncompact additive topological group, there is a
+translate of the second one that is disjoint from the first one."]
+lemma exists_disjoint_smul_of_is_compact [noncompact_space G] {K L : set G}
+  (hK : is_compact K) (hL : is_compact L) : ∃ (g : G), disjoint K (g • L) :=
+begin
+  have A : ¬ (K * L⁻¹ = univ), from (hK.mul hL.inv).ne_univ,
+  obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹,
+  { contrapose! A, exact eq_univ_iff_forall.2 A },
+  refine ⟨g, _⟩,
+  apply disjoint_left.2 (λ a ha h'a, hg _),
+  rcases h'a with ⟨b, bL, rfl⟩,
+  refine ⟨g * b, b⁻¹, ha, by simpa only [set.mem_inv, inv_inv] using bL, _⟩,
+  simp only [smul_eq_mul, mul_inv_cancel_right]
+end
+
+/-- In a locally compact group, any neighborhood of the identity contains a compact closed
+neighborhood of the identity, even without separation assumptions on the space. -/
+@[to_additive "In a locally compact additive group, any neighborhood of the identity contains a
+compact closed neighborhood of the identity, even without separation assumptions on the space."]
+lemma local_is_compact_is_closed_nhds_of_group [locally_compact_space G]
+  {U : set G} (hU : U ∈ 𝓝 (1 : G)) :
+  ∃ (K : set G), is_compact K ∧ is_closed K ∧ K ⊆ U ∧ (1 : G) ∈ interior K :=
+begin
+  obtain ⟨L, Lint, LU, Lcomp⟩ : ∃ (L : set G) (H : L ∈ 𝓝 (1 : G)), L ⊆ U ∧ is_compact L,
+    from local_compact_nhds hU,
+  obtain ⟨V, Vnhds, hV⟩ : ∃ V ∈ 𝓝 (1 : G), ∀ (v ∈ V) (w ∈ V), v * w ∈ L,
+  { have : ((λ p : G × G, p.1 * p.2) ⁻¹' L) ∈ 𝓝 ((1, 1) : G × G),
+    { refine continuous_at_fst.mul continuous_at_snd _,
+      simpa only [mul_one] using Lint },
+    simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] },
+  have VL : closure V ⊆ L, from calc
+    closure V = {(1 : G)} * closure V : by simp only [singleton_mul, one_mul, image_id']
+    ... ⊆ interior V * closure V : mul_subset_mul_right
+      (by simpa only [singleton_subset_iff] using mem_interior_iff_mem_nhds.2 Vnhds)
+    ... = interior V * V : is_open_interior.mul_closure _
+    ... ⊆ V * V : mul_subset_mul_right interior_subset
+    ... ⊆ L : by { rintros x ⟨y, z, yv, zv, rfl⟩, exact hV _ yv _ zv },
+  exact ⟨closure V, is_compact_of_is_closed_subset Lcomp is_closed_closure VL, is_closed_closure,
+    VL.trans LU, interior_mono subset_closure (mem_interior_iff_mem_nhds.2 Vnhds)⟩,
+end
+
 end
 
 section

src/topology/algebra/monoid.lean

@@ -453,7 +453,8 @@ end
 multiplication by constants.
 
 Notably, this instances applies when `R = A`, or when `[algebra R A]` is available. -/
-@[priority 100]
+@[priority 100, to_additive  "If `R` acts on `A` via `A`, then continuous addition implies
+continuous affine addition by constants."]
 instance is_scalar_tower.has_continuous_const_smul {R A : Type*} [monoid A] [has_smul R A]
   [is_scalar_tower R A A] [topological_space A] [has_continuous_mul A] :
   has_continuous_const_smul R A :=

src/topology/instances/ennreal.lean

@@ -166,6 +166,9 @@ tendsto_nhds_top $ λ n, mem_at_top_sets.2
 by rw [tendsto_nhds_top_iff_nnreal, at_top_basis_Ioi.tendsto_right_iff];
   [simp, apply_instance, apply_instance]
 
+lemma tendsto_of_real_at_top : tendsto ennreal.of_real at_top (𝓝 ∞) :=
+tendsto_coe_nhds_top.2 tendsto_real_to_nnreal_at_top
+
 lemma nhds_zero : 𝓝 (0 : ℝ≥0∞) = ⨅a ≠ 0, 𝓟 (Iio a) :=
 nhds_bot_order.trans $ by simp [bot_lt_iff_ne_bot, Iio]
 

src/topology/instances/nnreal.lean

@@ -99,10 +99,18 @@ lemma comap_coe_at_top : comap (coe : ℝ≥0 → ℝ) at_top = at_top :=
   tendsto (λ a, (m a : ℝ)) f at_top ↔ tendsto m f at_top :=
 tendsto_Ici_at_top.symm
 
-lemma tendsto_real_to_nnreal {f : filter α} {m : α → ℝ} {x : ℝ} (h : tendsto m f (𝓝 x)) :
+lemma _root_.tendsto_real_to_nnreal {f : filter α} {m : α → ℝ} {x : ℝ} (h : tendsto m f (𝓝 x)) :
   tendsto (λa, real.to_nnreal (m a)) f (𝓝 (real.to_nnreal x)) :=
 (continuous_real_to_nnreal.tendsto _).comp h
 
+lemma _root_.tendsto_real_to_nnreal_at_top : tendsto real.to_nnreal at_top at_top :=
+begin
+  rw ← tendsto_coe_at_top,
+  apply tendsto_id.congr' _,
+  filter_upwards [Ici_mem_at_top (0 : ℝ)] with x hx,
+  simp only [max_eq_left (set.mem_Ici.1 hx), id.def, real.coe_to_nnreal'],
+end
+
 lemma nhds_zero : 𝓝 (0 : ℝ≥0) = ⨅a ≠ 0, 𝓟 (Iio a) :=
 nhds_bot_order.trans $ by simp [bot_lt_iff_ne_bot]