feat(topology/algebra,geometry/manifold): continuity and smoothness of locally finite products of functions (#7128)

Author: urkud

src/geometry/manifold/algebra/monoid.lean

@@ -173,3 +173,54 @@ instance : inhabited (smooth_monoid_morphism I I' G G') := ⟨1⟩
 instance : has_coe_to_fun (smooth_monoid_morphism I I' G G') := ⟨_, λ a, a.to_fun⟩
 
 end monoid
+
+section comm_monoid
+
+open_locale big_operators
+
+variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
+{H : Type*} [topological_space H]
+{E : Type*} [normed_group E] [normed_space 𝕜 E] {I : model_with_corners 𝕜 E H}
+{G : Type*} [comm_monoid G] [topological_space G] [charted_space H G] [has_smooth_mul I G]
+{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
+{H' : Type*} [topological_space H'] {I' : model_with_corners 𝕜 E' H'}
+{M : Type*} [topological_space M] [charted_space H' M]
+
+@[to_additive]
+lemma smooth_finset_prod' {ι} {s : finset ι} {f : ι → M → G} (h : ∀ i ∈ s, smooth I' I (f i)) :
+  smooth I' I (∏ i in s, f i) :=
+finset.prod_induction _ _ (λ f g hf hg, hf.mul hg)
+  (@smooth_const _ _ _ _ _ _ _ I' _ _ _ _ _ _ _ _ I _ _ _ 1) h
+
+@[to_additive]
+lemma smooth_finset_prod {ι} {s : finset ι} {f : ι → M → G} (h : ∀ i ∈ s, smooth I' I (f i)) :
+  smooth I' I (λ x, ∏ i in s, f i x) :=
+by { simp only [← finset.prod_apply], exact smooth_finset_prod' h }
+
+open function filter
+
+@[to_additive]
+lemma smooth_finprod {ι} {f : ι → M → G} (h : ∀ i, smooth I' I (f i))
+  (hfin : locally_finite (λ i, mul_support (f i))) :
+  smooth I' I (λ x, ∏ᶠ i, f i x) :=
+begin
+  intro x,
+  rcases hfin x with ⟨U, hxU, hUf⟩,
+  have : smooth_at I' I (λ x, ∏ i in hUf.to_finset, f i x) x,
+    from smooth_finset_prod (λ i hi, h i) x,
+  refine this.congr_of_eventually_eq (mem_sets_of_superset hxU $ λ y hy, _),
+  refine finprod_eq_prod_of_mul_support_subset _ (λ i hi, _),
+  rw [hUf.coe_to_finset],
+  exact ⟨y, hi, hy⟩
+end
+
+@[to_additive]
+lemma smooth_finprod_cond {ι} {f : ι → M → G} {p : ι → Prop} (hc : ∀ i, p i → smooth I' I (f i))
+  (hf : locally_finite (λ i, mul_support (f i))) :
+  smooth I' I (λ x, ∏ᶠ i (hi : p i), f i x) :=
+begin
+  simp only [← finprod_subtype_eq_finprod_cond],
+  exact smooth_finprod (λ i, hc i i.2) (hf.comp_injective subtype.coe_injective)
+end
+
+end comm_monoid

src/topology/algebra/monoid.lean

@@ -7,6 +7,7 @@ import topology.continuous_on
 import group_theory.submonoid.operations
 import algebra.group.prod
 import algebra.pointwise
+import algebra.big_operators.finprod
 
 /-!
 # Theory of topological monoids
@@ -19,17 +20,17 @@ the definitions.
 open classical set filter topological_space
 open_locale classical topological_space big_operators
 
-variables {α β M N : Type*}
+variables {ι α X M N : Type*} [topological_space X]
 
 /-- Basic hypothesis to talk about a topological additive monoid or a topological additive
-semigroup. A topological additive monoid over `α`, for example, is obtained by requiring both the
-instances `add_monoid α` and `has_continuous_add α`. -/
+semigroup. A topological additive monoid over `M`, for example, is obtained by requiring both the
+instances `add_monoid M` and `has_continuous_add M`. -/
 class has_continuous_add (M : Type*) [topological_space M] [has_add M] : Prop :=
 (continuous_add : continuous (λ p : M × M, p.1 + p.2))
 
 /-- Basic hypothesis to talk about a topological monoid or a topological semigroup.
-A topological monoid over `α`, for example, is obtained by requiring both the instances `monoid α`
-and `has_continuous_mul α`. -/
+A topological monoid over `M`, for example, is obtained by requiring both the instances `monoid M`
+and `has_continuous_mul M`. -/
 @[to_additive]
 class has_continuous_mul (M : Type*) [topological_space M] [has_mul M] : Prop :=
 (continuous_mul : continuous (λ p : M × M, p.1 * p.2))
@@ -43,8 +44,7 @@ lemma continuous_mul : continuous (λp:M×M, p.1 * p.2) :=
 has_continuous_mul.continuous_mul
 
 @[continuity, to_additive]
-lemma continuous.mul [topological_space α] {f : α → M} {g : α → M}
-  (hf : continuous f) (hg : continuous g) :
+lemma continuous.mul {f g : X → M} (hf : continuous f) (hg : continuous g) :
   continuous (λx, f x * g x) :=
 continuous_mul.comp (hf.prod_mk hg : _)
 
@@ -60,8 +60,8 @@ lemma continuous_mul_right (a : M) : continuous (λ b:M, b * a) :=
 continuous_id.mul continuous_const
 
 @[to_additive]
-lemma continuous_on.mul [topological_space α] {f : α → M} {g : α → M} {s : set α}
-  (hf : continuous_on f s) (hg : continuous_on g s) :
+lemma continuous_on.mul {f g : X → M} {s : set X} (hf : continuous_on f s)
+  (hg : continuous_on g s) :
   continuous_on (λx, f x * g x) s :=
 (continuous_mul.comp_continuous_on (hf.prod hg) : _)
 
@@ -70,7 +70,7 @@ lemma tendsto_mul {a b : M} : tendsto (λp:M×M, p.fst * p.snd) (𝓝 (a, b)) (
 continuous_iff_continuous_at.mp has_continuous_mul.continuous_mul (a, b)
 
 @[to_additive]
-lemma filter.tendsto.mul {f : α → M} {g : α → M} {x : filter α} {a b : M}
+lemma filter.tendsto.mul {f g : α → M} {x : filter α} {a b : M}
   (hf : tendsto f x (𝓝 a)) (hg : tendsto g x (𝓝 b)) :
   tendsto (λx, f x * g x) x (𝓝 (a * b)) :=
 tendsto_mul.comp (hf.prod_mk_nhds hg)
@@ -86,14 +86,13 @@ lemma filter.tendsto.mul_const (b : M) {c : M} {f : α → M} {l : filter α}
 h.mul tendsto_const_nhds
 
 @[to_additive]
-lemma continuous_at.mul [topological_space α] {f : α → M} {g : α → M} {x : α}
-  (hf : continuous_at f x) (hg : continuous_at g x) :
+lemma continuous_at.mul {f g : X → M} {x : X} (hf : continuous_at f x) (hg : continuous_at g x) :
   continuous_at (λx, f x * g x) x :=
 hf.mul hg
 
 @[to_additive]
-lemma continuous_within_at.mul [topological_space α] {f : α → M} {g : α → M} {s : set α} {x : α}
-  (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
+lemma continuous_within_at.mul {f g : X → M} {s : set X} {x : X} (hf : continuous_within_at f s x)
+  (hg : continuous_within_at g s x) :
   continuous_within_at (λx, f x * g x) s x :=
 hf.mul hg
 
@@ -103,8 +102,8 @@ instance [topological_space N] [has_mul N] [has_continuous_mul N] : has_continuo
  ((continuous_snd.comp continuous_fst).mul (continuous_snd.comp continuous_snd))⟩
 
 @[to_additive]
-instance pi.has_continuous_mul {C : β → Type*} [∀ b, topological_space (C b)]
-  [∀ b, has_mul (C b)] [∀ b, has_continuous_mul (C b)] : has_continuous_mul (Π b, C b) :=
+instance pi.has_continuous_mul {C : ι → Type*} [∀ i, topological_space (C i)]
+  [∀ i, has_mul (C i)] [∀ i, has_continuous_mul (C i)] : has_continuous_mul (Π i, C i) :=
 { continuous_mul := continuous_pi (λ i, continuous.mul
     ((continuous_apply i).comp continuous_fst) ((continuous_apply i).comp continuous_snd)) }
 
@@ -243,8 +242,8 @@ begin
 end
 
 @[to_additive]
-lemma tendsto_list_prod {f : β → α → M} {x : filter α} {a : β → M} :
-  ∀l:list β, (∀c∈l, tendsto (f c) x (𝓝 (a c))) →
+lemma tendsto_list_prod {f : ι → α → M} {x : filter α} {a : ι → M} :
+  ∀ l:list ι, (∀i∈l, tendsto (f i) x (𝓝 (a i))) →
     tendsto (λb, (l.map (λc, f c b)).prod) x (𝓝 ((l.map a).prod))
 | []       _ := by simp [tendsto_const_nhds]
 | (f :: l) h :=
@@ -255,9 +254,9 @@ lemma tendsto_list_prod {f : β → α → M} {x : filter α} {a : β → M} :
   end
 
 @[to_additive]
-lemma continuous_list_prod [topological_space α] {f : β → α → M} (l : list β)
-  (h : ∀c∈l, continuous (f c)) :
-  continuous (λa, (l.map (λc, f c a)).prod) :=
+lemma continuous_list_prod {f : ι → X → M} (l : list ι)
+  (h : ∀i∈l, continuous (f i)) :
+  continuous (λa, (l.map (λi, f i a)).prod) :=
 continuous_iff_continuous_at.2 $ assume x, tendsto_list_prod l $ assume c hc,
   continuous_iff_continuous_at.1 (h c hc) x
 
@@ -268,7 +267,7 @@ lemma continuous_pow : ∀ n : ℕ, continuous (λ a : M, a ^ n)
 | (k+1) := by { simp only [pow_succ], exact continuous_id.mul (continuous_pow _) }
 
 @[continuity]
-lemma continuous.pow {f : α → M} [topological_space α] (h : continuous f) (n : ℕ) :
+lemma continuous.pow {f : X → M} (h : continuous f) (n : ℕ) :
   continuous (λ b, (f b) ^ n) :=
 continuous.comp (continuous_pow n) h
 
@@ -338,31 +337,55 @@ mem_nhds_sets oS S.one_mem
 variable [has_continuous_mul M]
 
 @[to_additive]
-lemma tendsto_multiset_prod {f : β → α → M} {x : filter α} {a : β → M} (s : multiset β) :
-  (∀c∈s, tendsto (f c) x (𝓝 (a c))) →
+lemma tendsto_multiset_prod {f : ι → α → M} {x : filter α} {a : ι → M} (s : multiset ι) :
+  (∀ i ∈ s, tendsto (f i) x (𝓝 (a i))) →
     tendsto (λb, (s.map (λc, f c b)).prod) x (𝓝 ((s.map a).prod)) :=
-by { rcases s with ⟨l⟩, simp, exact tendsto_list_prod l }
+by { rcases s with ⟨l⟩, simpa using tendsto_list_prod l }
 
 @[to_additive]
-lemma tendsto_finset_prod {f : β → α → M} {x : filter α} {a : β → M} (s : finset β) :
-  (∀c∈s, tendsto (f c) x (𝓝 (a c))) → tendsto (λb, ∏ c in s, f c b) x (𝓝 (∏ c in s, a c)) :=
+lemma tendsto_finset_prod {f : ι → α → M} {x : filter α} {a : ι → M} (s : finset ι) :
+  (∀ i ∈ s, tendsto (f i) x (𝓝 (a i))) → tendsto (λb, ∏ c in s, f c b) x (𝓝 (∏ c in s, a c)) :=
 tendsto_multiset_prod _
 
 @[to_additive, continuity]
-lemma continuous_multiset_prod [topological_space α] {f : β → α → M} (s : multiset β) :
-  (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).prod) :=
-by { rcases s with ⟨l⟩, simp, exact continuous_list_prod l }
+lemma continuous_multiset_prod {f : ι → X → M} (s : multiset ι) :
+  (∀i ∈ s, continuous (f i)) → continuous (λ a, (s.map (λ i, f i a)).prod) :=
+by { rcases s with ⟨l⟩, simpa using continuous_list_prod l }
 
 attribute [continuity] continuous_multiset_sum
 
 @[continuity, to_additive]
-lemma continuous_finset_prod [topological_space α] {f : β → α → M} (s : finset β) :
-  (∀c∈s, continuous (f c)) → continuous (λa, ∏ c in s, f c a) :=
+lemma continuous_finset_prod {f : ι → X → M} (s : finset ι) :
+  (∀ i ∈ s, continuous (f i)) → continuous (λa, ∏ i in s, f i a) :=
 continuous_multiset_prod _
 
 -- should `to_additive` be doing this?
 attribute [continuity] continuous_finset_sum
 
+open function
+
+@[to_additive] lemma continuous_finprod {f : ι → X → M} (hc : ∀ i, continuous (f i))
+  (hf : locally_finite (λ i, mul_support (f i))) :
+  continuous (λ x, ∏ᶠ i, f i x) :=
+begin
+  refine continuous_iff_continuous_at.2 (λ x, _),
+  rcases hf x with ⟨U, hxU, hUf⟩,
+  have : continuous_at (λ x, ∏ i in hUf.to_finset, f i x) x,
+    from tendsto_finset_prod _ (λ i hi, (hc i).continuous_at),
+  refine this.congr (mem_sets_of_superset hxU $ λ y hy, _),
+  refine (finprod_eq_prod_of_mul_support_subset _ (λ i hi, _)).symm,
+  rw [hUf.coe_to_finset],
+  exact ⟨y, hi, hy⟩
+end
+
+@[to_additive] lemma continuous_finprod_cond {f : ι → X → M} {p : ι → Prop}
+  (hc : ∀ i, p i → continuous (f i)) (hf : locally_finite (λ i, mul_support (f i))) :
+  continuous (λ x, ∏ᶠ i (hi : p i), f i x) :=
+begin
+  simp only [← finprod_subtype_eq_finprod_cond],
+  exact continuous_finprod (λ i, hc i i.2) (hf.comp_injective subtype.coe_injective)
+end
+
 end
 
 instance additive.has_continuous_add {M} [h : topological_space M] [has_mul M]

src/topology/continuous_function/basic.lean

@@ -36,9 +36,14 @@ instance : has_coe_to_fun (C(α, β)) := ⟨_, continuous_map.to_fun⟩
 
 variables {α β} {f g : continuous_map α β}
 
-protected lemma continuous (f : C(α, β)) : continuous f := f.continuous_to_fun
+@[continuity] protected lemma continuous (f : C(α, β)) : continuous f := f.continuous_to_fun
 
-@[continuity] lemma coe_continuous : continuous (f : α → β) := f.continuous_to_fun
+protected lemma continuous_at (f : C(α, β)) (x : α) : continuous_at f x :=
+f.continuous.continuous_at
+
+protected lemma continuous_within_at (f : C(α, β)) (s : set α) (x : α) :
+  continuous_within_at f s x :=
+f.continuous.continuous_within_at
 
 @[ext] theorem ext (H : ∀ x, f x = g x) : f = g :=
 by cases f; cases g; congr'; exact funext H