feat(*): add various results split out from proof of Gallagher's theorem (#17985)

ocfnash · ocfnash · commit 5cc2dfdd3e92 · 2022-12-21T14:13:50.000Z
This is a collection of tiny results that are not really related but I'm bundling them together in an effort to aid review.
diff --git a/src/analysis/normed/field/basic.lean b/src/analysis/normed/field/basic.lean
@@ -693,6 +693,8 @@ instance : normed_comm_ring ℤ :=
 
 lemma int.norm_eq_abs (n : ℤ) : ‖n‖ = |n| := rfl
 
+@[simp] lemma int.norm_coe_nat (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [int.norm_eq_abs]
+
 lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ‖n‖₊ :=
 nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ)
                = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast]
@@ -724,36 +726,17 @@ instance : densely_normed_field ℚ :=
 by rw [← rat.norm_cast_real, ← int.norm_cast_real]; congr' 1; norm_cast
 
 -- Now that we've installed the norm on `ℤ`,
--- we can state some lemmas about `nsmul` and `zsmul`.
+-- we can state some lemmas about `zsmul`.
 section
-variables [seminormed_add_comm_group α]
-
-lemma norm_nsmul_le (n : ℕ) (a : α) : ‖n • a‖ ≤ n * ‖a‖ :=
-begin
-  induction n with n ih,
-  { simp only [norm_zero, nat.cast_zero, zero_mul, zero_smul] },
-  simp only [nat.succ_eq_add_one, add_smul, add_mul, one_mul, nat.cast_add,
-    nat.cast_one, one_nsmul],
-  exact norm_add_le_of_le ih le_rfl
-end
-
-lemma norm_zsmul_le (n : ℤ) (a : α) : ‖n • a‖ ≤ ‖n‖ * ‖a‖ :=
-begin
-  induction n with n n,
-  { simp only [int.of_nat_eq_coe, coe_nat_zsmul],
-    convert norm_nsmul_le n a,
-    exact nat.abs_cast n },
-  { simp only [int.neg_succ_of_nat_coe, neg_smul, norm_neg, coe_nat_zsmul],
-    convert norm_nsmul_le n.succ a,
-    exact nat.abs_cast n.succ, }
-end
+variables [seminormed_comm_group α]
 
-lemma nnnorm_nsmul_le (n : ℕ) (a : α) : ‖n • a‖₊ ≤ n * ‖a‖₊ :=
-by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_nat_cast]
-  using norm_nsmul_le n a
+@[to_additive norm_zsmul_le]
+lemma norm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a^n‖ ≤ ‖n‖ * ‖a‖ :=
+by rcases n.eq_coe_or_neg with ⟨n, rfl | rfl⟩; simpa using norm_pow_le_mul_norm n a
 
-lemma nnnorm_zsmul_le (n : ℤ) (a : α) : ‖n • a‖₊ ≤ ‖n‖₊ * ‖a‖₊ :=
-by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul] using norm_zsmul_le n a
+@[to_additive nnnorm_zsmul_le]
+lemma nnnorm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a^n‖₊ ≤ ‖n‖₊ * ‖a‖₊ :=
+by simpa only [← nnreal.coe_le_coe, nnreal.coe_mul] using norm_zpow_le_mul_norm n a
 
 end
 
diff --git a/src/analysis/normed/group/basic.lean b/src/analysis/normed/group/basic.lean
@@ -1061,6 +1061,42 @@ by { ext c,
   ((*) b) ⁻¹' sphere a r = sphere (a / b) r :=
 by { ext c, simp only [set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm] }
 
+@[to_additive norm_nsmul_le] lemma norm_pow_le_mul_norm (n : ℕ) (a : E) : ‖a^n‖ ≤ n * ‖a‖ :=
+begin
+  induction n with n ih, { simp, },
+  simpa only [pow_succ', nat.cast_succ, add_mul, one_mul] using norm_mul_le_of_le ih le_rfl,
+end
+
+@[to_additive nnnorm_nsmul_le] lemma nnnorm_pow_le_mul_norm (n : ℕ) (a : E) : ‖a^n‖₊ ≤ n * ‖a‖₊ :=
+by simpa only [← nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_nat_cast]
+  using norm_pow_le_mul_norm n a
+
+@[to_additive] lemma pow_mem_closed_ball {n : ℕ} (h : a ∈ closed_ball b r) :
+  a^n ∈ closed_ball (b^n) (n • r) :=
+begin
+  simp only [mem_closed_ball, dist_eq_norm_div, ← div_pow] at h ⊢,
+  refine (norm_pow_le_mul_norm n (a / b)).trans _,
+  simpa only [nsmul_eq_mul] using mul_le_mul_of_nonneg_left h n.cast_nonneg,
+end
+
+@[to_additive] lemma pow_mem_ball {n : ℕ} (hn : 0 < n) (h : a ∈ ball b r) :
+  a^n ∈ ball (b^n) (n • r) :=
+begin
+  simp only [mem_ball, dist_eq_norm_div, ← div_pow] at h ⊢,
+  refine lt_of_le_of_lt (norm_pow_le_mul_norm n (a / b)) _,
+  replace hn : 0 < (n : ℝ), { norm_cast, assumption, },
+  rw nsmul_eq_mul,
+  nlinarith,
+end
+
+@[simp, to_additive] lemma mul_mem_closed_ball_mul_iff {c : E} :
+  a * c ∈ closed_ball (b * c) r ↔ a ∈ closed_ball b r :=
+by simp only [mem_closed_ball, dist_eq_norm_div, mul_div_mul_right_eq_div]
+
+@[simp, to_additive] lemma mul_mem_ball_mul_iff {c : E} :
+  a * c ∈ ball (b * c) r ↔ a ∈ ball b r :=
+by simp only [mem_ball, dist_eq_norm_div, mul_div_mul_right_eq_div]
+
 namespace isometric
 
 /-- Multiplication `y ↦ x * y` as an `isometry`. -/
diff --git a/src/analysis/normed_space/int.lean b/src/analysis/normed_space/int.lean
@@ -31,8 +31,6 @@ by rw [← coe_nnnorm, int.nnnorm_coe_units, nnreal.coe_one]
 
 @[simp] lemma nnnorm_coe_nat (n : ℕ) : ‖(n : ℤ)‖₊ = n := real.nnnorm_coe_nat _
 
-@[simp] lemma norm_coe_nat (n : ℕ) : ‖(n : ℤ)‖ = n := real.norm_coe_nat _
-
 @[simp] lemma to_nat_add_to_nat_neg_eq_nnnorm (n : ℤ) : ↑(n.to_nat) + ↑((-n).to_nat) = ‖n‖₊ :=
 by rw [← nat.cast_add, to_nat_add_to_nat_neg_eq_nat_abs, nnreal.coe_nat_abs]
 
diff --git a/src/data/nat/totient.lean b/src/data/nat/totient.lean
@@ -36,6 +36,17 @@ by simp [totient]
 
 lemma totient_eq_card_coprime (n : ℕ) : φ n = ((range n).filter n.coprime).card := rfl
 
+/-- A characterisation of `nat.totient` that avoids `finset`. -/
+lemma totient_eq_card_lt_and_coprime (n : ℕ) : φ n = nat.card {m | m < n ∧ n.coprime m} :=
+begin
+  let e : {m | m < n ∧ n.coprime m} ≃ finset.filter n.coprime (finset.range n) :=
+  { to_fun  := λ m, ⟨m, by simpa only [finset.mem_filter, finset.mem_range] using m.property⟩,
+    inv_fun := λ m, ⟨m, by simpa only [finset.mem_filter, finset.mem_range] using m.property⟩,
+    left_inv  := λ m, by simp only [subtype.coe_mk, subtype.coe_eta],
+    right_inv := λ m, by simp only [subtype.coe_mk, subtype.coe_eta] },
+  rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, fintype.card_coe],
+end
+
 lemma totient_le (n : ℕ) : φ n ≤ n :=
 ((range n).card_filter_le _).trans_eq (card_range n)
 
diff --git a/src/measure_theory/covering/liminf_limsup.lean b/src/measure_theory/covering/liminf_limsup.lean
@@ -163,7 +163,7 @@ begin
   cases le_or_lt 1 M with hM' hM',
   { apply has_subset.subset.eventually_le,
     change _ ≤ _,
-    refine mono_blimsup' (hMr.mono $ λ i hi, cthickening_mono _ (s i)),
+    refine mono_blimsup' (hMr.mono $ λ i hi hp, cthickening_mono _ (s i)),
     exact (le_mul_of_one_le_left (hRp i) hM').trans hi, },
   { simp only [← @cthickening_closure _ _ _ (s _)],
     have hs : ∀ i, is_closed (closure (s i)) := λ i, is_closed_closure,
diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean
@@ -1458,18 +1458,36 @@ instance : boolean_algebra (subtype (measurable_set : set α → Prop)) :=
   .. measurable_set.subtype.bounded_order,
   .. measurable_set.subtype.distrib_lattice }
 
+@[measurability] lemma measurable_set_blimsup {s : ℕ → set α} {p : ℕ → Prop}
+  (h : ∀ n, p n → measurable_set (s n)) :
+  measurable_set $ filter.blimsup s filter.at_top p :=
+begin
+  simp only [filter.blimsup_eq_infi_bsupr_of_nat, supr_eq_Union, infi_eq_Inter],
+  exact measurable_set.Inter
+    (λ n, measurable_set.Union (λ m, measurable_set.Union $ λ hm, h m hm.1)),
+end
+
+@[measurability] lemma measurable_set_bliminf {s : ℕ → set α} {p : ℕ → Prop}
+  (h : ∀ n, p n → measurable_set (s n)) :
+  measurable_set $ filter.bliminf s filter.at_top p :=
+begin
+  simp only [filter.bliminf_eq_supr_binfi_of_nat, infi_eq_Inter, supr_eq_Union],
+  exact measurable_set.Union
+    (λ n, measurable_set.Inter (λ m, measurable_set.Inter $ λ hm, h m hm.1)),
+end
+
 @[measurability] lemma measurable_set_limsup {s : ℕ → set α} (hs : ∀ n, measurable_set $ s n) :
   measurable_set $ filter.limsup s filter.at_top :=
 begin
-  simp only [filter.limsup_eq_infi_supr_of_nat', supr_eq_Union, infi_eq_Inter],
-  exact measurable_set.Inter (λ n, measurable_set.Union $ λ m, hs $ m + n),
+  convert measurable_set_blimsup (λ n h, hs n : ∀ n, true → measurable_set (s n)),
+  simp,
 end
 
 @[measurability] lemma measurable_set_liminf {s : ℕ → set α} (hs : ∀ n, measurable_set $ s n) :
   measurable_set $ filter.liminf s filter.at_top :=
 begin
-  simp only [filter.liminf_eq_supr_infi_of_nat', supr_eq_Union, infi_eq_Inter],
-  exact measurable_set.Union (λ n, measurable_set.Inter $ λ m, hs $ m + n),
+  convert measurable_set_bliminf (λ n h, hs n : ∀ n, true → measurable_set (s n)),
+  simp,
 end
 
 end measurable_set
diff --git a/src/measure_theory/measure/measure_space_def.lean b/src/measure_theory/measure/measure_space_def.lean
@@ -406,6 +406,38 @@ lemma ae_eq_set_union {s' t' : set α} (h : s =ᵐ[μ] t) (h' : s' =ᵐ[μ] t')
   (s ∪ s' : set α) =ᵐ[μ] (t ∪ t' : set α) :=
 h.union h'
 
+lemma union_ae_eq_univ_of_ae_eq_univ_left (h : s =ᵐ[μ] univ) :
+  (s ∪ t : set α) =ᵐ[μ] univ :=
+by { convert ae_eq_set_union h (ae_eq_refl t), rw univ_union, }
+
+lemma union_ae_eq_univ_of_ae_eq_univ_right (h : t =ᵐ[μ] univ) :
+  (s ∪ t : set α) =ᵐ[μ] univ :=
+by { convert ae_eq_set_union (ae_eq_refl s) h, rw union_univ, }
+
+lemma union_ae_eq_right_of_ae_eq_empty (h : s =ᵐ[μ] (∅ : set α)) :
+  (s ∪ t : set α) =ᵐ[μ] t :=
+by { convert ae_eq_set_union h (ae_eq_refl t), rw empty_union, }
+
+lemma union_ae_eq_left_of_ae_eq_empty (h : t =ᵐ[μ] (∅ : set α)) :
+  (s ∪ t : set α) =ᵐ[μ] s :=
+by { convert ae_eq_set_union (ae_eq_refl s) h, rw union_empty, }
+
+lemma inter_ae_eq_right_of_ae_eq_univ (h : s =ᵐ[μ] univ) :
+  (s ∩ t : set α) =ᵐ[μ] t :=
+by { convert ae_eq_set_inter h (ae_eq_refl t), rw univ_inter, }
+
+lemma inter_ae_eq_left_of_ae_eq_univ (h : t =ᵐ[μ] univ) :
+  (s ∩ t : set α) =ᵐ[μ] s :=
+by { convert ae_eq_set_inter (ae_eq_refl s) h, rw inter_univ, }
+
+lemma inter_ae_eq_empty_of_ae_eq_empty_left (h : s =ᵐ[μ] (∅ : set α)) :
+  (s ∩ t : set α) =ᵐ[μ] (∅ : set α) :=
+by { convert ae_eq_set_inter h (ae_eq_refl t), rw empty_inter, }
+
+lemma inter_ae_eq_empty_of_ae_eq_empty_right (h : t =ᵐ[μ] (∅ : set α)) :
+  (s ∩ t : set α) =ᵐ[μ] (∅ : set α) :=
+by { convert ae_eq_set_inter (ae_eq_refl s) h, rw inter_empty, }
+
 @[to_additive]
 lemma _root_.set.mul_indicator_ae_eq_one {M : Type*} [has_one M] {f : α → M} {s : set α}
   (h : s.mul_indicator f =ᵐ[μ] 1) : μ (s ∩ function.mul_support f) = 0 :=
diff --git a/src/order/hom/complete_lattice.lean b/src/order/hom/complete_lattice.lean
@@ -583,7 +583,9 @@ end complete_lattice_hom
 
 namespace complete_lattice_hom
 
-/-- `set.preimage` as a complete lattice homomorphism. -/
+/-- `set.preimage` as a complete lattice homomorphism.
+
+See also `Sup_hom.set_image`. -/
 def set_preimage (f : α → β) : complete_lattice_hom (set β) (set α) :=
 { to_fun := preimage f,
   map_Sup' := λ s, preimage_sUnion.trans $ by simp only [set.Sup_eq_sUnion, set.sUnion_image],
@@ -597,3 +599,30 @@ lemma set_preimage_comp (g : β → γ) (f : α → β) :
   set_preimage (g ∘ f) = (set_preimage f).comp (set_preimage g) := rfl
 
 end complete_lattice_hom
+
+lemma set.image_Sup {f : α → β} (s : set (set α)) :
+  f '' Sup s = Sup (image f '' s) :=
+begin
+  ext b,
+  simp only [Sup_eq_sUnion, mem_image, mem_sUnion, exists_prop, sUnion_image, mem_Union],
+  split,
+  { rintros ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩, exact ⟨t, ht₁, a, ht₂, rfl⟩, },
+  { rintros ⟨t, ht₁, a, ht₂, rfl⟩, exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩, },
+end
+
+/-- Using `set.image`, a function between types yields a `Sup_hom` between their lattices of
+subsets.
+
+See also `complete_lattice_hom.set_preimage`. -/
+@[simps] def Sup_hom.set_image (f : α → β) : Sup_hom (set α) (set β) :=
+{ to_fun := image f,
+  map_Sup' := set.image_Sup }
+
+/-- An equivalence of types yields an order isomorphism between their lattices of subsets. -/
+@[simps] def equiv.to_order_iso_set (e : α ≃ β) : set α ≃o set β :=
+{ to_fun  := image e,
+  inv_fun := image e.symm,
+  left_inv  := λ s, by simp only [← image_comp, equiv.symm_comp_self, id.def, image_id'],
+  right_inv := λ s, by simp only [← image_comp, equiv.self_comp_symm, id.def, image_id'],
+  map_rel_iff' :=
+    λ s t, ⟨λ h, by simpa using @monotone_image _ _ e.symm _ _ h, λ h, monotone_image h⟩ }
diff --git a/src/order/liminf_limsup.lean b/src/order/liminf_limsup.lean
@@ -661,19 +661,19 @@ lemma bliminf_antitone (h : ∀ x, p x → q x) :
   bliminf u f q ≤ bliminf u f p :=
 Sup_le_Sup $ λ a ha, ha.mono $ by tauto
 
-lemma mono_blimsup' (h : ∀ᶠ x in f, u x ≤ v x) :
+lemma mono_blimsup' (h : ∀ᶠ x in f, p x → u x ≤ v x) :
   blimsup u f p ≤ blimsup v f p :=
-Inf_le_Inf $ λ a ha, (ha.and h).mono $ λ x hx hx', hx.2.trans (hx.1 hx')
+Inf_le_Inf $ λ a ha, (ha.and h).mono $ λ x hx hx', (hx.2 hx').trans (hx.1 hx')
 
-lemma mono_blimsup (h : ∀ x, u x ≤ v x) :
+lemma mono_blimsup (h : ∀ x, p x → u x ≤ v x) :
   blimsup u f p ≤ blimsup v f p :=
 mono_blimsup' $ eventually_of_forall h
 
-lemma mono_bliminf' (h : ∀ᶠ x in f, u x ≤ v x) :
+lemma mono_bliminf' (h : ∀ᶠ x in f, p x → u x ≤ v x) :
   bliminf u f p ≤ bliminf v f p :=
-Sup_le_Sup $ λ a ha, (ha.and h).mono $ λ x hx hx', (hx.1 hx').trans hx.2
+Sup_le_Sup $ λ a ha, (ha.and h).mono $ λ x hx hx', (hx.1 hx').trans (hx.2 hx')
 
-lemma mono_bliminf (h : ∀ x, u x ≤ v x) :
+lemma mono_bliminf (h : ∀ x, p x → u x ≤ v x) :
   bliminf u f p ≤ bliminf v f p :=
 mono_bliminf' $ eventually_of_forall h
 
@@ -703,6 +703,32 @@ sup_le (blimsup_mono $ by tauto) (blimsup_mono $ by tauto)
   bliminf u f (λ x, p x ∨ q x) ≤ bliminf u f p ⊓ bliminf u f q :=
 @blimsup_sup_le_or αᵒᵈ β _ f p q u
 
+lemma order_iso.apply_blimsup [complete_lattice γ] (e : α ≃o γ) :
+  e (blimsup u f p) = blimsup (e ∘ u) f p :=
+begin
+  simp only [blimsup_eq, map_Inf, function.comp_app],
+  congr,
+  ext c,
+  obtain ⟨a, rfl⟩ := e.surjective c,
+  simp,
+end
+
+lemma order_iso.apply_bliminf [complete_lattice γ] (e : α ≃o γ) :
+  e (bliminf u f p) = bliminf (e ∘ u) f p :=
+@order_iso.apply_blimsup αᵒᵈ β γᵒᵈ _ f p u _ e.dual
+
+lemma Sup_hom.apply_blimsup_le [complete_lattice γ] (g : Sup_hom α γ) :
+  g (blimsup u f p) ≤ blimsup (g ∘ u) f p :=
+begin
+  simp only [blimsup_eq_infi_bsupr],
+  refine ((order_hom_class.mono g).map_infi₂_le _).trans _,
+  simp only [_root_.map_supr],
+end
+
+lemma Inf_hom.le_apply_bliminf [complete_lattice γ] (g : Inf_hom α γ) :
+  bliminf (g ∘ u) f p ≤ g (bliminf u f p) :=
+@Sup_hom.apply_blimsup_le αᵒᵈ β γᵒᵈ _ f p u _ g.dual
+
 end complete_lattice
 
 section complete_distrib_lattice
