wip

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -385,9 +385,11 @@ theorem dist_one_right (a : E) : dist a 1 = ‖a‖ := by rw [dist_eq_norm_div,
 theorem inseparable_one_iff_norm {a : E} : Inseparable a 1 ↔ ‖a‖ = 0 := by
   rw [Metric.inseparable_iff, dist_one_right]
 
+@[to_additive]
+lemma dist_one_left (a : E) : dist (1 : E) a = ‖a‖ := by rw [dist_comm, dist_one_right]
+
 @[to_additive (attr := simp)]
-theorem dist_one_left : dist (1 : E) = norm :=
-  funext fun a => by rw [dist_comm, dist_one_right]
+lemma dist_one : dist (1 : E) = norm := funext dist_one_left
 
 @[to_additive]
 theorem norm_div_rev (a b : E) : ‖a / b‖ = ‖b / a‖ := by

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -159,7 +159,7 @@ end NNNorm
 
 @[to_additive lipschitzWith_one_norm]
 theorem lipschitzWith_one_norm' : LipschitzWith 1 (norm : E → ℝ) := by
-  simpa only [dist_one_left] using LipschitzWith.dist_right (1 : E)
+  simpa using LipschitzWith.dist_right (1 : E)
 
 @[to_additive lipschitzWith_one_nnnorm]
 theorem lipschitzWith_one_nnnorm' : LipschitzWith 1 (NNNorm.nnnorm : E → ℝ≥0) :=

Mathlib/Geometry/Group/Marking.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Analysis.Normed.Group.Basic
+import Mathlib.Analysis.Normed.Group.Quotient
 import Mathlib.GroupTheory.FreeGroup.Reduce
 
 /-!
@@ -17,7 +17,7 @@ This file defines group markings and induces a norm on marked groups.
   homomorphism `FreeGroup S →* G`.
 * `MarkedGroup`: If `m : GroupMarking G S`, then `MarkedGroup m` is a type synonym for `G`
   endowed with the metric coming from `m`.
-* `MarkedGroup.instNormedGroup`: A marked group is normed by its marking.
+* `MarkedGroup.instNormedGroup`: A marked group is normed by the word metric of the marking.
 -/
 
 open Function List Nat
@@ -117,6 +117,11 @@ lemma toMarkedGroup_smul (g : G) (x : α) [SMul G α] :
 @[to_additive (attr := simp)]
 lemma ofMarkedGroup_smul (g : MarkedGroup m) (x : α) [SMul G α] : ofMarkedGroup g • x = g • x := rfl
 
+/-- A marked group is equivalent to a quotient of the free group by a normal subgroup. -/
+@[simps! apply]
+noncomputable def quotientEquivMarkedGroup : FreeGroup S ⧸ m.toMonoidHom.ker ≃* MarkedGroup m :=
+  QuotientGroup.quotientKerEquivOfSurjective _ m.coe_surjective
+
 @[to_additive]
 private lemma mul_aux [DecidableEq S] (x : MarkedGroup m) :
     ∃ (n : _) (l : FreeGroup S), toMarkedGroup (m l) = x ∧ l.toWord.length ≤ n := by
@@ -141,42 +146,21 @@ private lemma find_mul_aux [DecidableEq S] (x : MarkedGroup m)
     (Nat.le_find_iff _ _).2 fun k hk ⟨l, hl, hlk⟩ => (Nat.lt_find_iff _ _).1 hk _ hlk ⟨l, hl, rfl⟩
 
 @[to_additive]
-noncomputable instance : NormedGroup (MarkedGroup m) :=
-  GroupNorm.toNormedGroup
-    { toFun := fun x => by classical exact (Nat.find (mul_aux x)).cast
-      map_one' := by
-        classical
-        exact cast_eq_zero.2 <| (find_eq_zero <| mul_aux _).2 ⟨1, by simp_rw [map_one], le_rfl⟩
-      mul_le' := fun x y => by
-        classical
-        dsimp
-        norm_cast
-        obtain ⟨a, rfl, ha⟩ := Nat.find_spec (mul_aux x)
-        obtain ⟨b, rfl, hb⟩ := Nat.find_spec (mul_aux y)
-        refine find_le ⟨a * b, by simp, (a.toWord_mul_sublist _).length_le.trans ?_⟩
-        rw [length_append]
-        gcongr
-      inv' := by
-        classical
-        suffices ∀ {x : MarkedGroup m}, Nat.find (mul_aux x⁻¹) ≤ Nat.find (mul_aux x) by
-          dsimp
-          refine fun _ => congr_arg Nat.cast (this.antisymm ?_)
-          convert this
-          simp_rw [inv_inv]
-        rintro x
-        refine find_mono fun nI => ?_
-        rintro ⟨l, hl, h⟩
-        exact ⟨l⁻¹, by simp [hl], h.trans_eq' <| by simp⟩
-      eq_one_of_map_eq_zero' := fun x hx => by
-        classical
-        obtain ⟨l, rfl, hl⟩ := (find_eq_zero <| mul_aux _).1 (cast_eq_zero.1 hx)
-        rw [le_zero_iff, length_eq_zero, ← FreeGroup.toWord_one] at hl
-        rw [FreeGroup.toWord_injective hl, map_one, map_one] }
+noncomputable instance : NormedGroup (MarkedGroup m) where
+  norm x := ‖quotientEquivMarkedGroup.symm x‖
 
 namespace MarkedGroup
 
-@[to_additive]
-lemma norm_def [DecidableEq S] (x : MarkedGroup m)
+@[to_additive add_norm_def]
+private lemma norm_def [DecidableEq S] (x : MarkedGroup m)
+    [DecidablePred fun n ↦ ∃ l, toMarkedGroup (m l) = x ∧ l.toWord.length = n] :
+    ‖x‖ = Nat.find (mul_aux' x) := by
+  convert congr_arg Nat.cast (find_mul_aux _)
+  classical
+  infer_instance
+
+@[to_additive add_norm_def]
+lemma norm_le_iff [DecidableEq S] (x : MarkedGroup m)
     [DecidablePred fun n ↦ ∃ l, toMarkedGroup (m l) = x ∧ l.toWord.length = n] :
     ‖x‖ = Nat.find (mul_aux' x) := by
   convert congr_arg Nat.cast (find_mul_aux _)

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -180,6 +180,10 @@ theorem isClosed_setOf_map_smul {N : Type*} [Monoid N] (α β) [MulAction M α]
   exact isClosed_iInter fun c => isClosed_iInter fun x =>
     isClosed_eq (continuous_apply _) ((continuous_apply _).const_smul _)
 
+@[to_additive]
+instance Submonoid.continuousConstSMul {S : Submonoid M} : ContinuousConstSMul S α :=
+  IsInducing.id.continuousConstSMul Subtype.val rfl
+
 end Monoid
 
 section Group
@@ -191,6 +195,10 @@ theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G)
     Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
   ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul c⁻¹, fun h => h.const_smul _⟩
 
+@[to_additive]
+instance Subgroup.continuousConstSMul {S : Subgroup G} : ContinuousConstSMul S α :=
+  IsInducing.id.continuousConstSMul Subtype.val rfl
+
 variable [TopologicalSpace β] {f : β → α} {b : β} {s : Set β}
 
 @[to_additive]

Mathlib/Topology/Algebra/Group/Quotient.lean

@@ -41,9 +41,8 @@ alias quotientMap_mk := isQuotientMap_mk
 theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
   continuous_quot_mk
 
-section ContinuousMul
-
-variable [ContinuousMul G] {N : Subgroup G}
+section ContinuousMulConst
+variable [ContinuousConstSMul Gᵐᵒᵖ G] {N : Subgroup G}
 
 @[to_additive]
 theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul
@@ -61,21 +60,27 @@ theorem dense_image_mk {s : Set G} :
     Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G)) := by
   rw [← dense_preimage_mk, preimage_image_mk_eq_mul]
 
-@[to_additive]
-instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where
-  continuous_smul := by
-    rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
-    exact continuous_mk.comp continuous_mul
-
-@[to_additive]
-instance instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance
-
 /-- A quotient of a locally compact group is locally compact. -/
 @[to_additive]
 instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) :
     LocallyCompactSpace (G ⧸ N) :=
   QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace
 
+end ContinuousMulConst
+
+section ContinuousMul
+
+variable [ContinuousConstSMul Gᵐᵒᵖ G] {N : Subgroup G}
+
+-- @[to_additive]
+-- instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where
+--   continuous_smul := by
+--     rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
+--     exact continuous_mk.comp continuous_mul
+
+-- @[to_additive]
+-- instance instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance
+
 @[to_additive (attr := deprecated "No deprecation message was provided." (since := "2024-10-05"))]
 theorem continuous_smul₁ (x : G ⧸ N) : Continuous fun g : G => g • x :=
   continuous_id.smul continuous_const

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

@@ -471,10 +471,13 @@ theorem infDist_le_dist_of_mem (h : y ∈ s) : infDist x s ≤ dist x y := by
 theorem infDist_le_infDist_of_subset (h : s ⊆ t) (hs : s.Nonempty) : infDist x t ≤ infDist x s :=
   ENNReal.toReal_mono (infEdist_ne_top hs) (infEdist_anti h)
 
+lemma le_infDist {r : ℝ} (hs : s.Nonempty) : r ≤ infDist x s ↔ ∀ ⦃y⦄, y ∈ s → r ≤ dist x y := by
+  simp_rw [infDist, ← ENNReal.ofReal_le_iff_le_toReal (infEdist_ne_top hs), le_infEdist,
+    ENNReal.ofReal_le_iff_le_toReal (edist_ne_top _ _), ← dist_edist]
+
 /-- The minimal distance to a set `s` is `< r` iff there exists a point in `s` at distance `< r`. -/
 theorem infDist_lt_iff {r : ℝ} (hs : s.Nonempty) : infDist x s < r ↔ ∃ y ∈ s, dist x y < r := by
-  simp_rw [infDist, ← ENNReal.lt_ofReal_iff_toReal_lt (infEdist_ne_top hs), infEdist_lt_iff,
-    ENNReal.lt_ofReal_iff_toReal_lt (edist_ne_top _ _), ← dist_edist]
+  simp [← not_le, le_infDist hs]
 
 /-- The minimal distance from `x` to `s` is bounded by the distance from `y` to `s`, modulo
 the distance between `x` and `y`. -/