feat(topology/continuous_function): some lemmas spun off from #18392 (#…

…18465)

A few miscellaneous lemmas about continuous functions needed for my Poisson summation project. Companion mathlib4 PR (blank for now) at [#2369](leanprover-community/mathlib4#2369).

src/topology/algebra/monoid.lean

@@ -7,6 +7,7 @@ import algebra.big_operators.finprod
 import order.filter.pointwise
 import topology.algebra.mul_action
 import algebra.big_operators.pi
+import topology.continuous_function.basic
 
 /-!
 # Theory of topological monoids
@@ -688,3 +689,23 @@ by { rw ← Inf_range, exact has_continuous_mul_Inf (set.forall_range_iff.mpr h'
 by { rw inf_eq_infi, refine has_continuous_mul_infi (λ b, _), cases b; assumption }
 
 end lattice_ops
+
+namespace continuous_map
+
+variables [has_mul X] [has_continuous_mul X]
+
+/-- The continuous map `λ y, y * x` -/
+@[to_additive "The continuous map `λ y, y + x"]
+protected def mul_right (x : X) : C(X, X) := mk _ (continuous_mul_right x)
+
+@[to_additive, simp]
+lemma coe_mul_right (x : X) : ⇑(continuous_map.mul_right x) = λ y, y * x := rfl
+
+/-- The continuous map `λ y, x * y` -/
+@[to_additive "The continuous map `λ y, x + y"]
+protected def mul_left (x : X) : C(X, X) := mk _ (continuous_mul_left x)
+
+@[to_additive, simp]
+lemma coe_mul_left (x : X) : ⇑(continuous_map.mul_left x) = λ y, x * y := rfl
+
+end continuous_map

src/topology/continuous_function/algebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Nicolò Cavalleri
 -/
 import algebra.algebra.pi
+import algebra.periodic
 import algebra.algebra.subalgebra.basic
 import algebra.star.star_alg_hom
 import tactic.field_simp
@@ -45,38 +46,54 @@ namespace continuous_map
 variables {α : Type*} {β : Type*} {γ : Type*}
 variables [topological_space α] [topological_space β] [topological_space γ]
 
+/- ### "mul" and "add" -/
+
 @[to_additive]
 instance has_mul [has_mul β] [has_continuous_mul β] : has_mul C(α, β) :=
 ⟨λ f g, ⟨f * g, continuous_mul.comp (f.continuous.prod_mk g.continuous : _)⟩⟩
 
 @[simp, norm_cast, to_additive]
 lemma coe_mul [has_mul β] [has_continuous_mul β] (f g : C(α, β)) : ⇑(f * g) = f * g := rfl
 
+@[simp, to_additive]
+lemma mul_apply [has_mul β] [has_continuous_mul β] (f g : C(α, β)) (x : α) :
+  (f * g) x = f x * g x := rfl
+
 @[simp, to_additive] lemma mul_comp [has_mul γ] [has_continuous_mul γ]
   (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
   (f₁ * f₂).comp g = f₁.comp g * f₂.comp g :=
 rfl
 
-@[to_additive]
-instance [has_one β] : has_one C(α, β) := ⟨const α 1⟩
+/- ### "one" -/
 
-@[simp, norm_cast, to_additive]
-lemma coe_one [has_one β]  : ⇑(1 : C(α, β)) = 1 := rfl
+@[to_additive] instance [has_one β] : has_one C(α, β) := ⟨const α 1⟩
+
+@[simp, norm_cast, to_additive] lemma coe_one [has_one β]  : ⇑(1 : C(α, β)) = 1 := rfl
+
+@[simp, to_additive] lemma one_apply [has_one β] (x : α) : (1 : C(α, β)) x = 1 := rfl
 
 @[simp, to_additive] lemma one_comp [has_one γ] (g : C(α, β)) : (1 : C(β, γ)).comp g = 1 := rfl
 
-instance [has_nat_cast β] : has_nat_cast C(α, β) :=
-⟨λ n, continuous_map.const _ n⟩
+/- ### "nat_cast" -/
 
-@[simp, norm_cast]
-lemma coe_nat_cast [has_nat_cast β] (n : ℕ) : ((n : C(α, β)) : α → β) = n := rfl
+instance [has_nat_cast β] : has_nat_cast C(α, β) := ⟨λ n, continuous_map.const _ n⟩
+
+@[simp, norm_cast] lemma coe_nat_cast [has_nat_cast β] (n : ℕ) : ((n : C(α, β)) : α → β) = n := rfl
+
+@[simp] lemma nat_cast_apply [has_nat_cast β] (n : ℕ) (x : α) : (n : C(α, β)) x = n := rfl
+
+/- ### "int_cast" -/
 
 instance [has_int_cast β] : has_int_cast C(α, β) :=
 ⟨λ n, continuous_map.const _ n⟩
 
 @[simp, norm_cast]
 lemma coe_int_cast [has_int_cast β] (n : ℤ) : ((n : C(α, β)) : α → β) = n := rfl
 
+@[simp] lemma int_cast_apply [has_int_cast β] (n : ℤ) (x : α) : (n : C(α, β)) x = n := rfl
+
+/- ### "nsmul" and "pow" -/
+
 instance has_nsmul [add_monoid β] [has_continuous_add β] : has_smul ℕ C(α, β) :=
 ⟨λ n f, ⟨n • f, f.continuous.nsmul n⟩⟩
 
@@ -88,8 +105,14 @@ instance has_pow [monoid β] [has_continuous_mul β] : has_pow C(α, β) ℕ :=
 lemma coe_pow [monoid β] [has_continuous_mul β] (f : C(α, β)) (n : ℕ) :
   ⇑(f ^ n) = f ^ n := rfl
 
--- don't make `coe_nsmul` simp as the linter complains it's redundant WRT `coe_smul`
-attribute [simp] coe_pow
+@[to_additive] lemma pow_apply [monoid β] [has_continuous_mul β]
+  (f : C(α, β)) (n : ℕ) (x : α) :
+  (f ^ n) x = f x ^ n :=
+rfl
+
+-- don't make auto-generated `coe_nsmul` and `nsmul_apply` simp, as the linter complains they're
+-- redundant WRT `coe_smul`
+attribute [simp] coe_pow pow_apply
 
 @[to_additive] lemma pow_comp [monoid γ] [has_continuous_mul γ]
   (f : C(β, γ)) (n : ℕ) (g : C(α, β)) :
@@ -99,6 +122,8 @@ rfl
 -- don't make `nsmul_comp` simp as the linter complains it's redundant WRT `smul_comp`
 attribute [simp] pow_comp
 
+/- ### "inv" and "neg" -/
+
 @[to_additive]
 instance [group β] [topological_group β] : has_inv C(α, β) :=
 { inv := λ f, ⟨f⁻¹, f.continuous.inv⟩ }
@@ -108,10 +133,16 @@ lemma coe_inv [group β] [topological_group β] (f : C(α, β)) :
   ⇑(f⁻¹) = f⁻¹ :=
 rfl
 
+@[simp, to_additive] lemma inv_apply [group β] [topological_group β] (f : C(α, β)) (x : α) :
+  f⁻¹ x = (f x)⁻¹ :=
+rfl
+
 @[simp, to_additive] lemma inv_comp [group γ] [topological_group γ] (f : C(β, γ)) (g : C(α, β)) :
   (f⁻¹).comp g = (f.comp g)⁻¹ :=
 rfl
 
+/- ### "div" and "sub" -/
+
 @[to_additive]
 instance [has_div β] [has_continuous_div β] : has_div C(α, β) :=
 { div := λ f g, ⟨f / g, f.continuous.div' g.continuous⟩ }
@@ -120,11 +151,17 @@ instance [has_div β] [has_continuous_div β] : has_div C(α, β) :=
 lemma coe_div [has_div β] [has_continuous_div β] (f g : C(α, β)) : ⇑(f / g) = f / g :=
 rfl
 
+@[simp, to_additive] lemma div_apply [has_div β] [has_continuous_div β] (f g : C(α, β)) (x : α) :
+  (f / g) x = f x / g x :=
+rfl
+
 @[simp, to_additive] lemma div_comp [has_div γ] [has_continuous_div γ]
   (f g : C(β, γ)) (h : C(α, β)) :
   (f / g).comp h = (f.comp h) / (g.comp h) :=
 rfl
 
+/- ### "zpow" and "zsmul" -/
+
 instance has_zsmul [add_group β] [topological_add_group β] : has_smul ℤ C(α, β) :=
 { smul := λ z f, ⟨z • f, f.continuous.zsmul z⟩ }
 
@@ -138,8 +175,14 @@ lemma coe_zpow [group β] [topological_group β] (f : C(α, β)) (z : ℤ) :
   ⇑(f ^ z) = f ^ z :=
 rfl
 
--- don't make `coe_zsmul` simp as the linter complains it's redundant WRT `coe_smul`
-attribute [simp] coe_zpow
+@[to_additive] lemma zpow_apply [group β] [topological_group β]
+  (f : C(α, β)) (z : ℤ) (x : α) :
+  (f ^ z) x = f x ^ z :=
+rfl
+
+-- don't make auto-generated `coe_zsmul` and `zsmul_apply` simp as the linter complains they're
+-- redundant WRT `coe_smul`
+attribute [simp] coe_zpow zpow_apply
 
 @[to_additive]
 lemma zpow_comp [group γ] [topological_group γ] (f : C(β, γ)) (z : ℤ) (g : C(α, β)) :
@@ -881,6 +924,30 @@ lemma comp_star_alg_hom'_comp (g : C(Y, Z)) (f : C(X, Y)) :
   comp_star_alg_hom' 𝕜 A (g.comp f) = (comp_star_alg_hom' 𝕜 A f).comp (comp_star_alg_hom' 𝕜 A g) :=
 star_alg_hom.ext $ λ _, continuous_map.ext $ λ _, rfl
 
+section periodicity
+
+/-! ### Summing translates of a function -/
+
+/-- Summing the translates of `f` by `ℤ • p` gives a map which is periodic with period `p`.
+(This is true without any convergence conditions, since if the sum doesn't converge it is taken to
+be the zero map, which is periodic.) -/
+lemma periodic_tsum_comp_add_zsmul [locally_compact_space X] [add_comm_group X]
+  [topological_add_group X] [add_comm_monoid Y] [has_continuous_add Y] [t2_space Y]
+  (f : C(X, Y)) (p : X) :
+  function.periodic ⇑(∑' (n : ℤ), f.comp (continuous_map.add_right (n • p))) p :=
+begin
+  intro x,
+  by_cases h : summable (λ n : ℤ, f.comp (continuous_map.add_right (n • p))),
+  { convert congr_arg (λ f : C(X, Y), f x) ((equiv.add_right (1 : ℤ)).tsum_eq _) using 1,
+    simp_rw [←tsum_apply h, ←tsum_apply ((equiv.add_right (1 : ℤ)).summable_iff.mpr h),
+      equiv.coe_add_right, comp_apply, coe_add_right, add_one_zsmul, add_comm (_ • p) p,
+      ←add_assoc] },
+  { rw tsum_eq_zero_of_not_summable h,
+    simp only [coe_zero, pi.zero_apply] }
+end
+
+end periodicity
+
 end continuous_map
 
 namespace homeomorph

src/topology/continuous_function/basic.lean

@@ -224,7 +224,13 @@ def restrict (f : C(α, β)) : C(s, β) := ⟨f ∘ coe⟩
 
 @[simp] lemma coe_restrict (f : C(α, β)) : ⇑(f.restrict s) = f ∘ coe := rfl
 
-/-- The restriction of a continuous map onto the preimage of a set. -/
+@[simp] lemma restrict_apply (f : C(α, β)) (s : set α) (x : s) : f.restrict s x = f x := rfl
+
+@[simp] lemma restrict_apply_mk (f : C(α, β)) (s : set α) (x : α) (hx : x ∈ s) :
+  f.restrict s ⟨x, hx⟩ = f x :=
+rfl
+
+/-- The restriction of a continuous map to the preimage of a set. -/
 @[simps]
 def restrict_preimage (f : C(α, β)) (s : set β) : C(f ⁻¹' s, s) :=
 ⟨s.restrict_preimage f, continuous_iff_continuous_at.mpr $ λ x, f.2.continuous_at.restrict_preimage⟩

src/topology/continuous_function/bounded.lean

@@ -308,11 +308,17 @@ begin
 end
 
 /-- Composition of a bounded continuous function and a continuous function. -/
-@[simps { fully_applied := ff }]
 def comp_continuous {δ : Type*} [topological_space δ] (f : α →ᵇ β) (g : C(δ, α)) : δ →ᵇ β :=
 { to_continuous_map := f.1.comp g,
   map_bounded' := f.map_bounded'.imp (λ C hC x y, hC _ _) }
 
+@[simp] lemma coe_comp_continuous {δ : Type*} [topological_space δ] (f : α →ᵇ β) (g : C(δ, α)) :
+  coe_fn (f.comp_continuous g) = f ∘ g := rfl
+
+@[simp] lemma comp_continuous_apply {δ : Type*} [topological_space δ]
+  (f : α →ᵇ β) (g : C(δ, α)) (x : δ) : f.comp_continuous g x = f (g x) :=
+rfl
+
 lemma lipschitz_comp_continuous {δ : Type*} [topological_space δ] (g : C(δ, α)) :
   lipschitz_with 1 (λ f : α →ᵇ β, f.comp_continuous g) :=
 lipschitz_with.mk_one $ λ f₁ f₂, (dist_le dist_nonneg).2 $ λ x, dist_coe_le_dist (g x)
@@ -322,10 +328,13 @@ lemma continuous_comp_continuous {δ : Type*} [topological_space δ] (g : C(δ,
 (lipschitz_comp_continuous g).continuous
 
 /-- Restrict a bounded continuous function to a set. -/
-@[simps apply { fully_applied := ff }]
 def restrict (f : α →ᵇ β) (s : set α) : s →ᵇ β :=
 f.comp_continuous $ (continuous_map.id _).restrict s
 
+@[simp] lemma coe_restrict (f : α →ᵇ β) (s : set α) : coe_fn (f.restrict s) = f ∘ coe := rfl
+
+@[simp] lemma restrict_apply (f : α →ᵇ β) (s : set α) (x : s) : f.restrict s x = f x := rfl
+
 /-- Composition (in the target) of a bounded continuous function with a Lipschitz map again
 gives a bounded continuous function -/
 def comp (G : β → γ) {C : ℝ≥0} (H : lipschitz_with C G)

src/topology/continuous_function/compact.lean

@@ -206,6 +206,11 @@ le_trans (neg_le_neg (f.norm_coe_le_norm x)) (neg_le.mp (neg_le_abs_self (f x)))
 lemma norm_eq_supr_norm : ‖f‖ = ⨆ x : α, ‖f x‖ :=
 (mk_of_compact f).norm_eq_supr_norm
 
+lemma norm_restrict_mono_set {X : Type*} [topological_space X]
+  (f : C(X, E)) {K L : topological_space.compacts X} (hKL : K ≤ L) :
+  ‖f.restrict K‖ ≤ ‖f.restrict L‖ :=
+(norm_le _ (norm_nonneg _)).mpr (λ x, norm_coe_le_norm (f.restrict L) $ set.inclusion hKL x)
+
 end
 
 section
@@ -409,7 +414,12 @@ map_continuous (comp_right_continuous_map A f)
 
 end comp_right
 
-section weierstrass
+section local_normal_convergence
+/-! ### Local normal convergence
+
+A sum of continuous functions (on a locally compact space) is "locally normally convergent" if the
+sum of its sup-norms on any compact subset is summable. This implies convergence in the topology
+of `C(X, E)` (i.e. locally uniform convergence). -/
 
 open topological_space
 
@@ -427,8 +437,7 @@ begin
   simpa only [has_sum, A] using summable_of_summable_norm (hF K)
 end
 
-end weierstrass
-
+end local_normal_convergence
 
 /-!
 ### Star structures