feat(analysis/convolution): weaken typeclass assumptions (#17452)

Remove some finite-dimensionality or propertness assumptions, by noticing that if a compactly supported function is nonzero then the space has to be finite-dimensional.

src/analysis/convolution.lean

@@ -420,10 +420,10 @@ lemma convolution_smul [smul_comm_class ℝ 𝕜 F]
   {y : 𝕜} : f ⋆[L, μ] (y • g) = y • (f ⋆[L, μ] g) :=
 by { ext, simp only [pi.smul_apply, convolution_def, ← integral_smul, (L _).map_smul] }
 
-lemma zero_convolution : 0 ⋆[L, μ] g = 0 :=
+@[simp] lemma zero_convolution : 0 ⋆[L, μ] g = 0 :=
 by { ext, simp_rw [convolution_def, pi.zero_apply, L.map_zero₂, integral_zero] }
 
-lemma convolution_zero : f ⋆[L, μ] 0 = 0 :=
+@[simp] lemma convolution_zero : f ⋆[L, μ] 0 = 0 :=
 by { ext, simp_rw [convolution_def, pi.zero_apply, (L _).map_zero, integral_zero] }
 
 lemma convolution_exists_at.distrib_add {x : G} (hfg : convolution_exists_at f g x L μ)
@@ -582,6 +582,19 @@ lemma convolution_mul_swap [normed_space ℝ 𝕜] [complete_space 𝕜] {f : G
   (f ⋆[mul 𝕜 𝕜, μ] g) x = ∫ t, f (x - t) * g t ∂μ :=
 convolution_eq_swap _
 
+/-- The convolution of two even functions is also even. -/
+lemma convolution_neg_of_neg_eq (h1 : ∀ᵐ x ∂μ, f (-x) = f x) (h2 : ∀ᵐ x ∂μ, g (-x) = g x) :
+  (f ⋆[L, μ] g) (-x) = (f ⋆[L, μ] g) x :=
+calc ∫ (t : G), (L (f t)) (g (-x - t)) ∂μ
+    = ∫ (t : G), (L (f (-t))) (g (x + t)) ∂μ :
+  begin
+    apply integral_congr_ae,
+    filter_upwards [h1, (eventually_add_left_iff μ x).2 h2] with t ht h't,
+    simp_rw [ht, ← h't, neg_add'],
+  end
+... = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ :
+  by { rw ← integral_neg_eq_self, simp only [neg_neg, ← sub_eq_add_neg] }
+
 end measurable
 
 variables [topological_space G]
@@ -933,20 +946,23 @@ end
 
 end assoc
 
-variables [normed_add_comm_group G] [borel_space G]
-variables [second_countable_topology G] [sigma_compact_space G]
+variables [normed_add_comm_group G] [borel_space G] [normed_space 𝕜 G]
 
 lemma convolution_precompR_apply {g : G → E'' →L[𝕜] E'}
   (hf : locally_integrable f μ) (hcg : has_compact_support g) (hg : continuous g)
   (x₀ : G) (x : E'') : (f ⋆[L.precompR E'', μ] g) x₀ x = (f ⋆[L, μ] (λ a, g a x)) x₀  :=
 begin
+  rcases hcg.eq_zero_or_finite_dimensional 𝕜 hg with rfl|fin_dim,
+  { simp only [convolution, pi.zero_apply, integral_const, smul_zero, zero_apply,
+      _root_.map_zero] },
+  resetI,
+  haveI : proper_space G, from finite_dimensional.proper_is_R_or_C 𝕜 G,
   have := hcg.convolution_exists_right (L.precompR E'' : _) hf hg x₀,
   simp_rw [convolution_def, continuous_linear_map.integral_apply this],
   refl,
 end
 
 variables [sigma_finite μ] [is_add_left_invariant μ]
-variables [normed_space 𝕜 G] [proper_space G]
 
 /-- Compute the total derivative of `f ⋆ g` if `g` is `C^1` with compact support and `f` is locally
 integrable. To write down the total derivative as a convolution, we use
@@ -955,6 +971,12 @@ lemma has_compact_support.has_fderiv_at_convolution_right
   (hcg : has_compact_support g) (hf : locally_integrable f μ) (hg : cont_diff 𝕜 1 g) (x₀ : G) :
   has_fderiv_at (f ⋆[L, μ] g) ((f ⋆[L.precompR G, μ] fderiv 𝕜 g) x₀) x₀ :=
 begin
+  rcases hcg.eq_zero_or_finite_dimensional 𝕜 hg.continuous with rfl|fin_dim,
+  { have : fderiv 𝕜 (0 : G → E') = 0, from fderiv_const (0 : E'),
+    simp only [this, convolution_zero, pi.zero_apply],
+    exact has_fderiv_at_const (0 : F) x₀ },
+  resetI,
+  haveI : proper_space G, from finite_dimensional.proper_is_R_or_C 𝕜 G,
   set L' := L.precompR G,
   have h1 : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (λ t, L (f t) (g (x - t))) μ :=
   eventually_of_forall
@@ -988,10 +1010,14 @@ begin
   exact hcf.has_fderiv_at_convolution_right L.flip hg hf x₀,
 end
 
-lemma has_compact_support.cont_diff_convolution_right [finite_dimensional 𝕜 G]
+lemma has_compact_support.cont_diff_convolution_right
   (hcg : has_compact_support g) (hf : locally_integrable f μ) (hg : cont_diff 𝕜 n g) :
   cont_diff 𝕜 n (f ⋆[L, μ] g) :=
 begin
+  rcases hcg.eq_zero_or_finite_dimensional 𝕜 hg.continuous with rfl|fin_dim,
+  { simp only [convolution_zero], exact cont_diff_zero_fun, },
+  resetI,
+  haveI : proper_space G, from finite_dimensional.proper_is_R_or_C 𝕜 G,
   induction n using enat.nat_induction with n ih ih generalizing g,
   { rw [cont_diff_zero] at hg ⊢,
     exact hcg.continuous_convolution_right L hf hg },
@@ -1011,7 +1037,7 @@ begin
   { rw [cont_diff_top] at hg ⊢, exact λ n, ih n hcg (hg n) }
 end
 
-lemma has_compact_support.cont_diff_convolution_left [finite_dimensional 𝕜 G] [is_neg_invariant μ]
+lemma has_compact_support.cont_diff_convolution_left [is_neg_invariant μ]
   (hcf : has_compact_support f) (hf : cont_diff 𝕜 n f) (hg : locally_integrable g μ) :
   cont_diff 𝕜 n (f ⋆[L, μ] g) :=
 by { rw [← convolution_flip], exact hcf.cont_diff_convolution_right L.flip hg hf }

src/analysis/normed_space/finite_dimension.lean

@@ -511,6 +511,27 @@ begin
   simpa using h.image this,
 end
 
+/-- If a function has compact multiplicative support, then either the function is trivial or the
+space if finite-dimensional. -/
+@[to_additive "If a function has compact support, then either the function is trivial or the
+space if finite-dimensional."]
+lemma has_compact_mul_support.eq_one_or_finite_dimensional {X : Type*}
+  [topological_space X] [has_one X] [t2_space X]
+  {f : E → X} (hf : has_compact_mul_support f) (h'f : continuous f) :
+  f = 1 ∨ finite_dimensional 𝕜 E :=
+begin
+  by_cases h : ∀ x, f x = 1, { apply or.inl, ext x, exact h x },
+  apply or.inr,
+  push_neg at h,
+  obtain ⟨x, hx⟩ : ∃ x, f x ≠ 1, from h,
+  have : function.mul_support f ∈ 𝓝 x, from h'f.is_open_mul_support.mem_nhds hx,
+  obtain ⟨r, rpos, hr⟩ : ∃ (r : ℝ) (hi : 0 < r), metric.closed_ball x r ⊆ function.mul_support f,
+    from metric.nhds_basis_closed_ball.mem_iff.1 this,
+  have : is_compact (metric.closed_ball x r),
+    from is_compact_of_is_closed_subset hf metric.is_closed_ball (hr.trans (subset_mul_tsupport _)),
+  exact finite_dimensional_of_is_compact_closed_ball 𝕜 rpos this,
+end
+
 end riesz
 
 /-- An injective linear map with finite-dimensional domain is a closed embedding. -/

src/measure_theory/group/measure.lean

@@ -159,6 +159,23 @@ begin
   { rw map_mul_right_eq_self ν h, apply_instance },
 end
 
+@[to_additive]
+lemma is_mul_left_invariant_map {H : Type*}
+  [measurable_space H] [has_mul H] [has_measurable_mul H]
+  [is_mul_left_invariant μ]
+  (f : G →ₙ* H) (hf : measurable f) (h_surj : surjective f) :
+  is_mul_left_invariant (measure.map f μ) :=
+begin
+  refine ⟨λ h, _⟩,
+  rw map_map (measurable_const_mul _) hf,
+  obtain ⟨g, rfl⟩ := h_surj h,
+  conv_rhs { rw ← map_mul_left_eq_self μ g },
+  rw map_map hf (measurable_const_mul _),
+  congr' 2,
+  ext y,
+  simp only [comp_app, map_mul],
+end
+
 end has_measurable_mul
 
 end mul
@@ -211,6 +228,21 @@ lemma map_div_right_ae (μ : measure G) [is_mul_right_invariant μ] (x : G) :
   filter.map (λ t, t / x) μ.ae = μ.ae :=
 ((measurable_equiv.div_right x).map_ae μ).trans $ congr_arg ae $ map_div_right_eq_self μ x
 
+@[to_additive]
+lemma eventually_mul_left_iff (μ : measure G) [is_mul_left_invariant μ] (t : G) {p : G → Prop} :
+  (∀ᵐ x ∂μ, p (t * x)) ↔ ∀ᵐ x ∂μ, p x :=
+by { conv_rhs { rw [filter.eventually, ← map_mul_left_ae μ t] }, refl }
+
+@[to_additive]
+lemma eventually_mul_right_iff (μ : measure G) [is_mul_right_invariant μ] (t : G) {p : G → Prop} :
+  (∀ᵐ x ∂μ, p (x * t)) ↔ ∀ᵐ x ∂μ, p x :=
+by { conv_rhs { rw [filter.eventually, ← map_mul_right_ae μ t] }, refl }
+
+@[to_additive]
+lemma eventually_div_right_iff (μ : measure G) [is_mul_right_invariant μ] (t : G) {p : G → Prop} :
+  (∀ᵐ x ∂μ, p (x / t)) ↔ ∀ᵐ x ∂μ, p x :=
+by { conv_rhs { rw [filter.eventually, ← map_div_right_ae μ t] }, refl }
+
 end group
 
 namespace measure
@@ -523,17 +555,7 @@ lemma is_haar_measure_map [borel_space G] [topological_group G] {H : Type*} [gro
   (f : G →* H) (hf : continuous f) (h_surj : surjective f)
   (h_prop : tendsto f (cocompact G) (cocompact H)) :
   is_haar_measure (measure.map f μ) :=
-{ to_is_mul_left_invariant := begin
-    constructor,
-    assume h,
-    rw map_map (continuous_mul_left h).measurable hf.measurable,
-    obtain ⟨g, rfl⟩ := h_surj h,
-    conv_rhs { rw ← map_mul_left_eq_self μ g },
-    rw map_map hf.measurable (continuous_mul_left _).measurable,
-    congr' 2,
-    ext y,
-    simp only [comp_app, map_mul],
-  end,
+{ to_is_mul_left_invariant := is_mul_left_invariant_map f.to_mul_hom hf.measurable h_surj,
   lt_top_of_is_compact := begin
     assume K hK,
     rw map_apply hf.measurable hK.measurable_set,

src/topology/separation.lean

@@ -315,6 +315,11 @@ is_closed_singleton.is_open_compl
 lemma is_open_ne [t1_space α] {x : α} : is_open {y | y ≠ x} :=
 is_open_compl_singleton
 
+@[to_additive]
+lemma continuous.is_open_mul_support [t1_space α] [has_one α] [topological_space β]
+  {f : β → α} (hf : continuous f) : is_open (mul_support f) :=
+is_open_ne.preimage hf
+
 lemma ne.nhds_within_compl_singleton [t1_space α] {x y : α} (h : x ≠ y) :
   𝓝[{y}ᶜ] x = 𝓝 x :=
 is_open_ne.nhds_within_eq h