feat(topology/instances/real): a continuous periodic function has com…

…pact range (and is hence bounded) (#7968)

A few more facts about periodic functions, namely:
- If a function `f` is `periodic` with positive period `p`,
  then for all `x` there exists `y` such that `y` is an element of `[0, p)` and `f x = f y`
- A continuous, periodic function has compact range
- A continuous, periodic function is bounded

src/algebra/periodic.lean

@@ -5,6 +5,7 @@ Authors: Benjamin Davidson
 -/
 import data.int.parity
 import algebra.module.opposites
+import algebra.archimedean
 
 /-!
 # Periodicity
@@ -240,6 +241,14 @@ lemma periodic.int_mul_eq [ring α]
   f (n * c) = f 0 :=
 (h.int_mul n).eq
 
+/-- If a function `f` is `periodic` with positive period `c`, then for all `x` there exists some
+  `y ∈ Ico 0 c` such that `f x = f y`. -/
+lemma periodic.exists_mem_Ico [linear_ordered_add_comm_group α] [archimedean α]
+  (h : periodic f c) (hc : 0 < c) (x) :
+  ∃ y ∈ set.Ico 0 c, f x = f y :=
+let ⟨n, H⟩ := linear_ordered_add_comm_group.exists_int_smul_near_of_pos' hc x in
+⟨x - n • c, H, (h.sub_gsmul_eq n).symm⟩
+
 lemma periodic_with_period_zero [add_zero_class α]
   (f : α → β) :
   periodic f 0 :=

src/data/set/basic.lean

@@ -1642,18 +1642,21 @@ by { ext, simp }
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
 (surjective_quot_mk r).range_eq
 
-@[simp] theorem image_univ {ι : Type*} {f : ι → β} : f '' univ = range f :=
+@[simp] theorem image_univ {f : α → β} : f '' univ = range f :=
 by { ext, simp [image, range] }
 
-theorem image_subset_range {ι : Type*} (f : ι → β) (s : set ι) : f '' s ⊆ range f :=
+theorem image_subset_range (f : α → β) (s) : f '' s ⊆ range f :=
 by rw ← image_univ; exact image_subset _ (subset_univ _)
 
+theorem mem_range_of_mem_image (f : α → β) (s) {x : β} (h : x ∈ f '' s) : x ∈ range f :=
+mem_of_mem_of_subset h $ image_subset_range f s
+
 theorem range_comp (g : α → β) (f : ι → α) : range (g ∘ f) = g '' range f :=
 subset.antisymm
   (forall_range_iff.mpr $ assume i, mem_image_of_mem g (mem_range_self _))
   (ball_image_iff.mpr $ forall_range_iff.mpr mem_range_self)
 
-theorem range_subset_iff {s : set α} : range f ⊆ s ↔ ∀ y, f y ∈ s :=
+theorem range_subset_iff : range f ⊆ s ↔ ∀ y, f y ∈ s :=
 forall_range_iff
 
 lemma range_comp_subset_range (f : α → β) (g : β → γ) : range (g ∘ f) ⊆ range g :=

src/topology/instances/real.lean

@@ -8,6 +8,8 @@ import topology.algebra.uniform_group
 import topology.algebra.ring
 import ring_theory.subring
 import group_theory.archimedean
+import algebra.periodic
+
 /-!
 # Topological properties of ℝ
 -/
@@ -281,6 +283,41 @@ eq_Icc_of_connected_compact ⟨(nonempty_Icc.2 hab).image f, is_preconnected_Icc
 
 end
 
+section periodic
+
+namespace function
+
+lemma periodic.compact_of_continuous' [topological_space α] {f : ℝ → α} {c : ℝ}
+  (hp : periodic f c) (hc : 0 < c) (hf : continuous f) :
+  is_compact (range f) :=
+begin
+  convert is_compact_Icc.image hf,
+  ext x,
+  refine ⟨_, mem_range_of_mem_image f (Icc 0 c)⟩,
+  rintros ⟨y, h1⟩,
+  obtain ⟨z, hz, h2⟩ := hp.exists_mem_Ico hc y,
+  exact ⟨z, mem_Icc_of_Ico hz, h2.symm.trans h1⟩,
+end
+
+/-- A continuous, periodic function has compact range. -/
+lemma periodic.compact_of_continuous [topological_space α] {f : ℝ → α} {c : ℝ}
+  (hp : periodic f c) (hc : c ≠ 0) (hf : continuous f) :
+  is_compact (range f) :=
+begin
+  cases lt_or_gt_of_ne hc with hneg hpos,
+  exacts [hp.neg.compact_of_continuous' (neg_pos.mpr hneg) hf, hp.compact_of_continuous' hpos hf],
+end
+
+/-- A continuous, periodic function is bounded. -/
+lemma periodic.bounded_of_continuous [pseudo_metric_space α] {f : ℝ → α} {c : ℝ}
+  (hp : periodic f c) (hc : c ≠ 0) (hf : continuous f) :
+  bounded (range f) :=
+(hp.compact_of_continuous hc hf).bounded
+
+end function
+
+end periodic
+
 section subgroups
 
 /-- Given a nontrivial subgroup `G ⊆ ℝ`, if `G ∩ ℝ_{>0}` has no minimum then `G` is dense. -/