feat(topology): preliminaries for Haar measure (#3194)

Define group operations on sets
Define compacts, in a similar way to opens
Prove some "separation" properties for topological groups
Rename `continuous.comap` to `opens.comap` (so that we can have comaps for other kinds of sets in topological spaces)
Rename `inf_val` to `inf_def` (unused)
Move some definitions from `topology.opens` to `topology.compacts`

Author: fpvandoorn

src/data/finset/lattice.lean

@@ -77,6 +77,13 @@ lemma comp_sup_eq_sup_comp_of_is_total [is_total α (≤)] {γ : Type} [semilatt
   (g : α → γ) (mono_g : monotone g) (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f) :=
 comp_sup_eq_sup_comp g mono_g.map_sup bot
 
+/-- Computating `sup` in a subtype (closed under `sup`) is the same as computing it in `α`. -/
+lemma sup_coe {P : α → Prop}
+  {Pbot : P ⊥} {Psup : ∀{{x y}}, P x → P y → P (x ⊔ y)}
+  (t : finset β) (f : β → {x : α // P x}) :
+  (@sup _ _ (subtype.semilattice_sup_bot Pbot Psup) t f : α) = t.sup (λ x, f x) :=
+by { classical, rw [comp_sup_eq_sup_comp coe]; intros; refl }
+
 theorem subset_range_sup_succ (s : finset ℕ) : s ⊆ range (s.sup id).succ :=
 λ n hn, mem_range.2 $ nat.lt_succ_of_le $ le_sup hn
 
@@ -99,7 +106,7 @@ def inf (s : finset β) (f : β → α) : α := s.fold (⊓) ⊤ f
 
 variables {s s₁ s₂ : finset β} {f : β → α}
 
-lemma inf_val : s.inf f = (s.1.map f).inf := rfl
+lemma inf_def : s.inf f = (s.1.map f).inf := rfl
 
 @[simp] lemma inf_empty : (∅ : finset β).inf f = ⊤ :=
 fold_empty
@@ -143,6 +150,13 @@ lemma comp_inf_eq_inf_comp_of_is_total [h : is_total α (≤)] {γ : Type} [semi
   (g : α → γ) (mono_g : monotone g) (top : g ⊤ = ⊤) : g (s.inf f) = s.inf (g ∘ f) :=
 comp_inf_eq_inf_comp g mono_g.map_inf top
 
+/-- Computating `inf` in a subtype (closed under `inf`) is the same as computing it in `α`. -/
+lemma inf_coe {P : α → Prop}
+  {Ptop : P ⊤} {Pinf : ∀{{x y}}, P x → P y → P (x ⊓ y)}
+  (t : finset β) (f : β → {x : α // P x}) :
+  (@inf _ _ (subtype.semilattice_inf_top Ptop Pinf) t f : α) = t.inf (λ x, f x) :=
+by { classical, rw [comp_inf_eq_inf_comp coe]; intros; refl }
+
 end inf
 
 lemma inf_eq_infi [complete_lattice β] (s : finset α) (f : α → β) : s.inf f = (⨅a∈s, f a) :=

src/data/real/ennreal.lean

@@ -197,6 +197,9 @@ by simp [(≠), mul_eq_top] {contextual := tt}
 lemma mul_lt_top {a b : ennreal}  : a < ⊤ → b < ⊤ → a * b < ⊤ :=
 by simpa only [ennreal.lt_top_iff_ne_top] using mul_ne_top
 
+@[simp] lemma mul_pos {a b : ennreal} : 0 < a * b ↔ 0 < a ∧ 0 < b :=
+by simp only [zero_lt_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
+
 lemma pow_eq_top : ∀ n:ℕ, a^n=∞ → a=∞
 | 0 := by simp
 | (n+1) := λ o, (mul_eq_top.1 o).elim (λ h, pow_eq_top n h.2) and.left
@@ -753,6 +756,12 @@ inv_zero ▸ inv_eq_inv
 
 lemma inv_ne_top : a⁻¹ ≠ ∞ ↔ a ≠ 0 := by simp
 
+@[simp] lemma inv_lt_top {x : ennreal} : x⁻¹ < ⊤ ↔ 0 < x :=
+by { simp only [lt_top_iff_ne_top, inv_ne_top, zero_lt_iff_ne_zero] }
+
+lemma div_lt_top {x y : ennreal} (h1 : x < ⊤) (h2 : 0 < y) : x / y < ⊤ :=
+mul_lt_top h1 (inv_lt_top.mpr h2)
+
 @[simp] lemma inv_eq_zero : a⁻¹ = 0 ↔ a = ∞ :=
 inv_top ▸ inv_eq_inv
 
@@ -1163,6 +1172,23 @@ finset.induction_on s (by simp) $ assume a s ha ih,
       assume a ha, (hk _ $ finset.mem_insert_of_mem ha).right⟩,
   by simp [ha, ih.symm, infi_add_infi this]
 
+
+lemma infi_mul {ι} [nonempty ι] {f : ι → ennreal} {x : ennreal} (h : x ≠ ⊤) :
+  infi f * x = ⨅i, f i * x :=
+begin
+  by_cases h2 : x = 0, simp only [h2, mul_zero, infi_const],
+  refine le_antisymm
+    (le_infi $ λ i, mul_right_mono $ infi_le _ _)
+    ((div_le_iff_le_mul (or.inl h2) $ or.inl h).mp $ le_infi $
+      λ i, (div_le_iff_le_mul (or.inl h2) $ or.inl h).mpr $ infi_le _ _)
+end
+
+lemma mul_infi {ι} [nonempty ι] {f : ι → ennreal} {x : ennreal} (h : x ≠ ⊤) :
+  x * infi f = ⨅i, x * f i :=
+by { rw [mul_comm, infi_mul h], simp only [mul_comm], assumption }
+
+/-! `supr_mul`, `mul_supr` and variants are in `topology.instances.ennreal`. -/
+
 end infi
 
 section supr

src/order/bounded_lattice.lean

@@ -774,6 +774,13 @@ protected def semilattice_inf_bot [semilattice_inf_bot α] {P : α → Prop}
   bot_le := λ x, @bot_le α _ x,
   ..subtype.semilattice_inf Pinf }
 
+/-- A subtype forms a `⊓`-`⊤`-semilattice if `⊤` and `⊓` preserve the property. -/
+protected def semilattice_inf_top [semilattice_inf_top α] {P : α → Prop}
+  (Ptop : P ⊤) (Pinf : ∀{{x y}}, P x → P y → P (x ⊓ y)) : semilattice_inf_top {x : α // P x} :=
+{ top := ⟨⊤, Ptop⟩,
+  le_top := λ x, @le_top α _ x,
+  ..subtype.semilattice_inf Pinf }
+
 /-- A subtype forms a lattice if `⊔` and `⊓` preserve the property. -/
 protected def lattice [lattice α] {P : α → Prop}
   (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y)) :

src/topology/algebra/group.lean

@@ -402,6 +402,66 @@ lemma topological_group.t2_space [t1_space α] : t2_space α := regular_space.t2
 
 end
 
+section
+
+/-! Some results about an open set containing the product of two sets in a topological group. -/
+
+variables [topological_space α] [group α] [topological_group α]
+/-- Given a open neighborhood `U` of `1` there is a open neighborhood `V` of `1`
+  such that `VV ⊆ U`. -/
+@[to_additive "Given a open neighborhood `U` of `0` there is a open neighborhood `V` of `0`
+  such that `V + V ⊆ U`."]
+lemma one_open_separated_mul {U : set α} (h1U : is_open U) (h2U : (1 : α) ∈ U) :
+  ∃ V : set α, is_open V ∧ (1 : α) ∈ V ∧ V * V ⊆ U :=
+begin
+  rcases exists_nhds_square (continuous_mul U h1U) (by simp only [mem_preimage, one_mul, h2U] :
+    ((1 : α), (1 : α)) ∈ (λ p : α × α, p.1 * p.2) ⁻¹' U) with ⟨V, h1V, h2V, h3V⟩,
+  refine ⟨V, h1V, h2V, _⟩,
+  rwa [← image_subset_iff, image_mul_prod] at h3V
+end
+
+/-- Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `1`
+  such that `KV ⊆ U`. -/
+@[to_additive "Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `0`
+  such that `K + V ⊆ U`."]
+lemma compact_open_separated_mul {K U : set α} (hK : compact K) (hU : is_open U) (hKU : K ⊆ U) :
+  ∃ V : set α, is_open V ∧ (1 : α) ∈ V ∧ K * V ⊆ U :=
+begin
+  let W : α → set α := λ x, (λ y, x * y) ⁻¹' U,
+  have h1W : ∀ x, is_open (W x) := λ x, continuous_mul_left x U hU,
+  have h2W : ∀ x ∈ K, (1 : α) ∈ W x := λ x hx, by simp only [mem_preimage, mul_one, hKU hx],
+  choose V hV using λ x : K, one_open_separated_mul (h1W x) (h2W x.1 x.2),
+  let X : K → set α := λ x, (λ y, (x : α)⁻¹ * y) ⁻¹' (V x),
+  cases hK.elim_finite_subcover X (λ x, continuous_mul_left x⁻¹ (V x) (hV x).1) _ with t ht, swap,
+  { intros x hx, rw [mem_Union], use ⟨x, hx⟩, rw [mem_preimage], convert (hV _).2.1,
+    simp only [mul_left_inv, subtype.coe_mk] },
+  refine ⟨⋂ x ∈ t, V x, is_open_bInter (finite_mem_finset _) (λ x hx, (hV x).1), _, _⟩,
+  { simp only [mem_Inter], intros x hx, exact (hV x).2.1 },
+  rintro _ ⟨x, y, hx, hy, rfl⟩, simp only [mem_Inter] at hy,
+  have := ht hx, simp only [mem_Union, mem_preimage] at this, rcases this with ⟨z, h1z, h2z⟩,
+  have : (z : α)⁻¹ * x * y ∈ W z := (hV z).2.2 (mul_mem_mul h2z (hy z h1z)),
+  rw [mem_preimage] at this, convert this using 1, simp only [mul_assoc, mul_inv_cancel_left]
+end
+
+/-- A compact set is covered by finitely many left multiplicative translates of a set
+  with non-empty interior. -/
+@[to_additive "A compact set is covered by finitely many left additive translates of a set
+  with non-empty interior."]
+lemma compact_covered_by_mul_left_translates {K V : set α} (hK : compact K)
+  (hV : (interior V).nonempty) : ∃ t : finset α, K ⊆ ⋃ g ∈ t, (λ h, g * h) ⁻¹' V :=
+begin
+  cases hV with g₀ hg₀,
+  rcases compact.elim_finite_subcover hK (λ x : α, interior $ (λ h, x * h) ⁻¹' V) _ _ with ⟨t, ht⟩,
+  { refine ⟨t, subset.trans ht _⟩,
+    apply Union_subset_Union, intro g, apply Union_subset_Union, intro hg, apply interior_subset },
+  { intro g, apply is_open_interior },
+  { intros g hg, rw [mem_Union], use g₀ * g⁻¹,
+    apply preimage_interior_subset_interior_preimage, exact continuous_const.mul continuous_id,
+    rwa [mem_preimage, inv_mul_cancel_right] }
+end
+
+end
+
 section
 variables [topological_space α] [comm_group α] [topological_group α]
 

src/topology/algebra/infinite_sum.lean

@@ -339,6 +339,10 @@ tsum_eq_has_sum $ has_sum_sum_of_ne_finset_zero hf
 lemma tsum_fintype [fintype β] (f : β → α) : (∑'b, f b) = ∑ b, f b :=
 tsum_eq_has_sum $ has_sum_fintype f
 
+@[simp] lemma tsum_subtype_eq_sum {f : β → α} {s : finset β} :
+  (∑'x : {x // x ∈ s}, f x) = ∑ x in s, f x :=
+by { rw [tsum_fintype], conv_rhs { rw ← finset.sum_attach }, refl }
+
 lemma tsum_eq_single {f : β → α} (b : β) (hf : ∀b' ≠ b, f b' = 0)  :
   (∑'b, f b) = f b :=
 tsum_eq_has_sum $ has_sum_single b hf

src/topology/basic.lean

@@ -822,6 +822,10 @@ open_locale topological_space
   of every open set is open. -/
 def continuous (f : α → β) := ∀s, is_open s → is_open (f ⁻¹' s)
 
+lemma is_open.preimage {f : α → β} (hf : continuous f) {s : set β} (h : is_open s) :
+  is_open (f ⁻¹' s) :=
+hf s h
+
 /-- A function between topological spaces is continuous at a point `x₀`
 if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
 def continuous_at (f : α → β) (x : α) := tendsto f (𝓝 x) (𝓝 (f x))
@@ -891,6 +895,10 @@ lemma continuous_iff_is_closed {f : α → β} :
 ⟨assume hf s hs, hf sᶜ hs,
   assume hf s, by rw [←is_closed_compl_iff, ←is_closed_compl_iff]; exact hf _⟩
 
+lemma is_closed.preimage {f : α → β} (hf : continuous f) {s : set β} (h : is_closed s) :
+  is_closed (f ⁻¹' s) :=
+continuous_iff_is_closed.mp hf s h
+
 lemma continuous_at_iff_ultrafilter {f : α → β} (x) : continuous_at f x ↔
   ∀ g, is_ultrafilter g → g ≤ 𝓝 x → g.map f ≤ 𝓝 (f x) :=
 tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))

src/topology/compacts.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import topology.homeomorph
+/-!
+# Compact sets
+
+## Summary
+
+We define the subtype of compact sets in a topological space.
+
+## Main Definitions
+
+- `closeds α` is the type of closed subsets of a topological space `α`.
+- `compacts α` is the type of compact subsets of a topological space `α`.
+- `nonempty_compacts α` is the type of non-empty compact subsets.
+- `positive_compacts α` is the type of compact subsets with non-empty interior.
+-/
+open set
+
+
+variables (α : Type*) {β : Type*} [topological_space α] [topological_space β]
+namespace topological_space
+
+/-- The type of closed subsets of a topological space. -/
+def closeds := {s : set α // is_closed s}
+
+/-- The compact sets of a topological space. See also `nonempty_compacts`. -/
+def compacts : Type* := { s : set α // compact s }
+
+/-- The type of non-empty compact subsets of a topological space. The
+non-emptiness will be useful in metric spaces, as we will be able to put
+a distance (and not merely an edistance) on this space. -/
+def nonempty_compacts := {s : set α // s.nonempty ∧ compact s}
+
+/-- The compact sets with nonempty interior of a topological space. See also `compacts` and
+  `nonempty_compacts`. -/
+@[nolint has_inhabited_instance]
+def positive_compacts: Type* := { s : set α // compact s ∧ (interior s).nonempty  }
+
+variables {α}
+
+namespace compacts
+
+instance : semilattice_sup_bot (compacts α) :=
+subtype.semilattice_sup_bot compact_empty (λ K₁ K₂, compact.union)
+
+instance [t2_space α]: semilattice_inf_bot (compacts α) :=
+subtype.semilattice_inf_bot compact_empty (λ K₁ K₂, compact.inter)
+
+instance [t2_space α] : lattice (compacts α) :=
+subtype.lattice (λ K₁ K₂, compact.union) (λ K₁ K₂, compact.inter)
+
+@[simp] lemma bot_val : (⊥ : compacts α).1 = ∅ := rfl
+
+@[simp] lemma sup_val {K₁ K₂ : compacts α} : (K₁ ⊔ K₂).1 = K₁.1 ∪ K₂.1 := rfl
+
+@[ext] protected lemma ext {K₁ K₂ : compacts α} (h : K₁.1 = K₂.1) : K₁ = K₂ :=
+subtype.eq h
+
+@[simp] lemma finset_sup_val {β} {K : β → compacts α} {s : finset β} :
+  (s.sup K).1 = s.sup (λ x, (K x).1) :=
+finset.sup_coe _ _
+
+instance : inhabited (compacts α) := ⟨⊥⟩
+
+/-- The image of a compact set under a continuous function. -/
+protected def map (f : α → β) (hf : continuous f) (K : compacts α) : compacts β :=
+⟨f '' K.1, K.2.image hf⟩
+
+@[simp] lemma map_val {f : α → β} (hf : continuous f) (K : compacts α) :
+  (K.map f hf).1 = f '' K.1 := rfl
+
+/-- A homeomorphism induces an equivalence on compact sets, by taking the image. -/
+@[simp] protected def equiv (f : α ≃ₜ β) : compacts α ≃ compacts β :=
+{ to_fun := compacts.map f f.continuous,
+  inv_fun := compacts.map _ f.symm.continuous,
+  left_inv := by { intro K, ext1, simp only [map_val, ← image_comp, f.symm_comp_self, image_id] },
+  right_inv := by { intro K, ext1,
+    simp only [map_val, ← image_comp, f.self_comp_symm, image_id] } }
+
+/-- The image of a compact set under a homeomorphism can also be expressed as a preimage. -/
+lemma equiv_to_fun_val (f : α ≃ₜ β) (K : compacts α) :
+  (compacts.equiv f K).1 = f.symm ⁻¹' K.1 :=
+congr_fun (image_eq_preimage_of_inverse f.left_inv f.right_inv) K.1
+
+end compacts
+
+section nonempty_compacts
+open topological_space set
+variable {α}
+
+instance nonempty_compacts.to_compact_space {p : nonempty_compacts α} : compact_space p.val :=
+⟨compact_iff_compact_univ.1 p.property.2⟩
+
+instance nonempty_compacts.to_nonempty {p : nonempty_compacts α} : nonempty p.val :=
+p.property.1.to_subtype
+
+/-- Associate to a nonempty compact subset the corresponding closed subset -/
+def nonempty_compacts.to_closeds [t2_space α] : nonempty_compacts α → closeds α :=
+set.inclusion $ λ s hs, hs.2.is_closed
+
+end nonempty_compacts
+
+end topological_space

src/topology/constructions.lean

@@ -242,6 +242,16 @@ begin
       ⟨u, ⟨u, subset.refl u, uo, au⟩, v, ⟨v, subset.refl v, vo, bv⟩, h⟩⟩)
 end
 
+/-- Given an open neighborhood `s` of `(x, x)`, then `(x, x)` has a square open neighborhood
+  that is a subset of `s`. -/
+lemma exists_nhds_square {s : set (α × α)} (hs : is_open s) {x : α} (hx : (x, x) ∈ s) :
+  ∃U, is_open U ∧ x ∈ U ∧ set.prod U U ⊆ s :=
+begin
+  rcases is_open_prod_iff.mp hs x x hx with ⟨u, v, hu, hv, h1x, h2x, h2s⟩,
+  refine ⟨u ∩ v, is_open_inter hu hv, ⟨h1x, h2x⟩, subset.trans _ h2s⟩,
+  simp only [prod_subset_prod_iff, inter_subset_left, true_or, inter_subset_right, and_self],
+end
+
 /-- The first projection in a product of topological spaces sends open sets to open sets. -/
 lemma is_open_map_fst : is_open_map (@prod.fst α β) :=
 begin

src/topology/homeomorph.lean

@@ -103,6 +103,12 @@ begin
   exact continuous_iff_is_closed.1 (h.symm.continuous) _
 end
 
+@[simp] lemma is_open_preimage (h : α ≃ₜ β) {s : set β} : is_open (h ⁻¹' s) ↔ is_open s :=
+begin
+  refine ⟨λ hs, _, h.continuous_to_fun s⟩,
+  rw [← (image_preimage_eq h.to_equiv.surjective : _ = s)], exact h.is_open_map _ hs
+end
+
 /-- If an bijective map `e : α ≃ β` is continuous and open, then it is a homeomorphism. -/
 def homeomorph_of_continuous_open (e : α ≃ β) (h₁ : continuous e) (h₂ : is_open_map e) :
   α ≃ₜ β :=

src/topology/instances/ennreal.lean

@@ -534,6 +534,9 @@ tsum_add ennreal.summable ennreal.summable
 protected lemma tsum_le_tsum (h : ∀a, f a ≤ g a) : (∑'a, f a) ≤ (∑'a, g a) :=
 tsum_le_tsum h ennreal.summable ennreal.summable
 
+protected lemma sum_le_tsum {f : α → ennreal} (s : finset α) : s.sum f ≤ tsum f :=
+sum_le_tsum s (λ x hx, zero_le _) ennreal.summable
+
 protected lemma tsum_eq_supr_nat {f : ℕ → ennreal} :
   (∑'i:ℕ, f i) = (⨆i:ℕ, ∑ a in finset.range i, f a) :=
 ennreal.tsum_eq_supr_sum' _ finset.exists_nat_subset_range