Merge remote-tracking branch 'origin/master' into nolint-param

src/analysis/ODE/gronwall.lean

@@ -188,7 +188,7 @@ theorem dist_le_of_approx_trajectories_ODE {v : ℝ → E → E}
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwall_bound δ K (εf + εg) (t - a) :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,
-dist_le_of_approx_trajectories_ODE_of_mem_set (λ t x y hx hy, hv t x y) hf hf' f_bound hfs
+dist_le_of_approx_trajectories_ODE_of_mem_set (λ t x y hx hy, (hv t).dist_le x y) hf hf' f_bound hfs
   hg hg' g_bound (λ t ht, trivial) ha
 
 /-- If `f` and `g` are two exact solutions of the same ODE, then the distance between them
@@ -234,7 +234,7 @@ theorem dist_le_of_trajectories_ODE {v : ℝ → E → E}
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,
-dist_le_of_trajectories_ODE_of_mem_set (λ t x y hx hy, hv t x y) hf hf' hfs
+dist_le_of_trajectories_ODE_of_mem_set (λ t x y hx hy, (hv t).dist_le x y) hf hf' hfs
   hg hg' (λ t ht, trivial) ha
 
 /-- There exists only one solution of an ODE \(\dot x=v(t, x)\) in a set `s ⊆ ℝ × E` with
@@ -270,5 +270,5 @@ theorem ODE_solution_unique {v : ℝ → E → E}
   (ha : f a = g a) :
   ∀ t ∈ Icc a b, f t = g t :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,
-ODE_solution_unique_of_mem_set (λ t x y hx hy, hv t x y)
+ODE_solution_unique_of_mem_set (λ t x y hx hy, (hv t).dist_le x y)
   hf hf' hfs hg hg' (λ t ht, trivial) ha

src/analysis/normed_space/finite_dimension.lean

@@ -252,7 +252,7 @@ begin
     have B : e (e.symm y) = y := linear_equiv.apply_symm_apply _ _,
     conv_lhs { rw [← A, ← B] },
     change dist (f (e.symm x)) (f (e.symm y)) ≤ ∥f∥ * dist (e.symm x) (e.symm y),
-    exact f.lipschitz _ _ }
+    exact f.lipschitz.dist_le _ _ }
 end
 
 end proper_field

src/analysis/normed_space/operator_norm.lean

@@ -37,15 +37,15 @@ variables [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E
 
 lemma linear_map.lipschitz_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   lipschitz_with (nnreal.of_real C) f :=
-lipschitz_with.of_dist_le $ λ x y, by simpa [dist_eq_norm] using h (x - y)
+lipschitz_with.of_dist_le' $ λ x y, by simpa [dist_eq_norm] using h (x - y)
 
 lemma linear_map.uniform_continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   uniform_continuous f :=
-(f.lipschitz_of_bound C h).to_uniform_continuous
+(f.lipschitz_of_bound C h).uniform_continuous
 
 lemma linear_map.continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   continuous f :=
-(f.lipschitz_of_bound C h).to_continuous
+(f.lipschitz_of_bound C h).continuous
 
 /-- Construct a continuous linear map from a linear map and a bound on this linear map.
 The fact that the norm of the continuous linear map is then controlled is given in
@@ -304,11 +304,12 @@ lemma op_norm_comp_le : ∥comp h f∥ ≤ ∥h∥ * ∥f∥ :=
 
 /-- continuous linear maps are Lipschitz continuous. -/
 theorem lipschitz : lipschitz_with ⟨∥f∥, op_norm_nonneg f⟩ f :=
-λ x y, by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }
+lipschitz_with.of_dist_le $ λ x y,
+  by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }
 
 /-- A continuous linear map is automatically uniformly continuous. -/
 protected theorem uniform_continuous : uniform_continuous f :=
-f.lipschitz.to_uniform_continuous
+f.lipschitz.uniform_continuous
 
 variable {f}
 /-- A continuous linear map is an isometry if and only if it preserves the norm. -/

src/data/real/ennreal.lean

@@ -741,6 +741,17 @@ lemma div_le_iff_le_mul (hb0 : b ≠ 0) (hbt : b ≠ ⊤) : a / b ≤ c ↔ a 
 suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹, by simpa [div_def],
 (le_div_iff_mul_le (inv_ne_zero.2 hbt) (inv_ne_top.2 hb0)).symm
 
+lemma div_le_of_le_mul (h : a ≤ b * c) : a / c ≤ b :=
+begin
+  by_cases h0 : c = 0,
+  { have : a = 0, by simpa [h0] using h, simp [*] },
+  by_cases hinf : c = ⊤, by simp [hinf],
+  exact (div_le_iff_le_mul h0 hinf).2 h
+end
+
+lemma mul_lt_of_lt_div (h : a < b / c) : a * c < b :=
+by { contrapose! h, exact ennreal.div_le_of_le_mul h }
+
 lemma inv_le_iff_le_mul : (b = ⊤ → a ≠ 0) → (a = ⊤ → b ≠ 0) → (a⁻¹ ≤ b ↔ 1 ≤ a * b) :=
 begin
   cases a; cases b; simp [none_eq_top, some_eq_coe, mul_top, top_mul] {contextual := tt},

src/topology/bounded_continuous_function.lean

@@ -184,30 +184,30 @@ end
 gives a bounded continuous function -/
 def comp (G : β → γ) {C : nnreal} (H : lipschitz_with C G)
   (f : α →ᵇ β) : α →ᵇ γ :=
-⟨λx, G (f x), H.to_continuous.comp f.2.1,
+⟨λx, G (f x), H.continuous.comp f.2.1,
   let ⟨D, hD⟩ := f.2.2 in
   ⟨max C 0 * D, λ x y, calc
-    dist (G (f x)) (G (f y)) ≤ C * dist (f x) (f y) : H _ _
+    dist (G (f x)) (G (f y)) ≤ C * dist (f x) (f y) : H.dist_le _ _
     ... ≤ max C 0 * dist (f x) (f y) : mul_le_mul_of_nonneg_right (le_max_left C 0) dist_nonneg
     ... ≤ max C 0 * D : mul_le_mul_of_nonneg_left (hD _ _) (le_max_right C 0)⟩⟩
 
 /-- The composition operator (in the target) with a Lipschitz map is Lipschitz -/
 lemma lipschitz_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
   lipschitz_with C (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
-λ f g,
+lipschitz_with.of_dist_le $ λ f g,
 (dist_le (mul_nonneg C.2 dist_nonneg)).2 $ λ x,
-calc dist (G (f x)) (G (g x)) ≤ C * dist (f x) (g x) : H _ _
+calc dist (G (f x)) (G (g x)) ≤ C * dist (f x) (g x) : H.dist_le _ _
   ... ≤ C * dist f g : mul_le_mul_of_nonneg_left (dist_coe_le_dist _) C.2
 
 /-- The composition operator (in the target) with a Lipschitz map is uniformly continuous -/
 lemma uniform_continuous_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
   uniform_continuous (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
-(lipschitz_comp H).to_uniform_continuous
+(lipschitz_comp H).uniform_continuous
 
 /-- The composition operator (in the target) with a Lipschitz map is continuous -/
 lemma continuous_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
   continuous (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
-(lipschitz_comp H).to_continuous
+(lipschitz_comp H).continuous
 
 /-- Restriction (in the target) of a bounded continuous function taking values in a subset -/
 def cod_restrict (s : set β) (f : α →ᵇ β) (H : ∀x, f x ∈ s) : α →ᵇ s :=

src/topology/metric_space/closeds.lean

@@ -417,7 +417,7 @@ lemma nonempty_compacts.dist_eq {x y : nonempty_compacts α} :
 
 lemma lipschitz_inf_dist_set (x : α) :
   lipschitz_with 1 (λ s : nonempty_compacts α, inf_dist x s.val) :=
-lipschitz_with.one_of_le_add $ assume s t,
+lipschitz_with.of_le_add $ assume s t,
 by { rw dist_comm,
   exact inf_dist_le_inf_dist_add_Hausdorff_dist (edist_ne_top t s) }
 
@@ -428,7 +428,7 @@ lemma lipschitz_inf_dist :
 
 lemma uniform_continuous_inf_dist_Hausdorff_dist :
   uniform_continuous (λp : α × (nonempty_compacts α), inf_dist p.1 (p.2).val) :=
-lipschitz_inf_dist.to_uniform_continuous
+lipschitz_inf_dist.uniform_continuous
 
 end --section
 end metric --namespace

src/topology/metric_space/contracting.lean

@@ -34,7 +34,7 @@ begin
 end
 
 /-- A map is said to be `contracting_with K`, if `K < 1` and `f` is `lipschitz_with K`. -/
-def contracting_with [metric_space α] (K : ℝ≥0) (f : α → α) :=
+def contracting_with [emetric_space α] (K : ℝ≥0) (f : α → α) :=
 (K < 1) ∧ lipschitz_with K f
 
 namespace contracting_with
@@ -45,14 +45,17 @@ include hf
 
 lemma to_lipschitz_with : lipschitz_with K f := hf.2
 
+lemma dist_le (x y : α) : dist (f x) (f y) ≤ K * dist x y :=
+hf.to_lipschitz_with.dist_le x y
+
 lemma one_sub_K_pos : (0:ℝ) < 1 - K := sub_pos_of_lt hf.1
 
 lemma dist_inequality (x y) : dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - K) :=
 suffices dist x y ≤ dist x (f x) + dist y (f y) + K * dist x y,
   by rwa [le_div_iff hf.one_sub_K_pos, mul_comm, sub_mul, one_mul, sub_le_iff_le_add],
 calc dist x y ≤ dist x (f x) + dist y (f y) + dist (f x) (f y) : dist_triangle4_right _ _ _ _
           ... ≤ dist x (f x) + dist y (f y) + K * dist x y :
-  add_le_add_left (hf.to_lipschitz_with _ _) _
+  add_le_add_left (hf.dist_le _ _) _
 
 lemma dist_le_of_fixed_point (x) {y} (hy : f y = y) :
   dist x y ≤ (dist x (f x)) / (1 - K) :=
@@ -69,7 +72,7 @@ have cauchy_seq (λ n, f^[n] x₀),
 from cauchy_seq_of_le_geometric K (dist x₀ (f x₀)) hf.1 $
   hf.to_lipschitz_with.dist_iterate_succ_le_geometric x₀,
 let ⟨x, hx⟩ := cauchy_seq_tendsto_of_complete this in
-⟨x, fixed_point_of_tendsto_iterate (hf.to_lipschitz_with.to_continuous.tendsto x) ⟨x₀, hx⟩⟩
+⟨x, fixed_point_of_tendsto_iterate (hf.to_lipschitz_with.continuous.tendsto x) ⟨x₀, hx⟩⟩
 
 /-- Let `f` be a contracting map with constant `K`; let `g` be another map uniformly
 `C`-close to `f`. If `x` and `y` are their fixed points, then `dist x y ≤ C / (1 - K)`. -/

src/topology/metric_space/gromov_hausdorff.lean

@@ -494,11 +494,11 @@ end
 
 lemma to_GH_space_lipschitz :
   lipschitz_with 1 (nonempty_compacts.to_GH_space : nonempty_compacts α → GH_space) :=
-lipschitz_with.one_mk GH_dist_le_nonempty_compacts_dist
+lipschitz_with.mk_one GH_dist_le_nonempty_compacts_dist
 
 lemma to_GH_space_continuous :
   continuous (nonempty_compacts.to_GH_space : nonempty_compacts α → GH_space) :=
-to_GH_space_lipschitz.to_continuous
+to_GH_space_lipschitz.continuous
 
 end nonempty_compacts
 

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -161,6 +161,7 @@ calc
 private lemma candidates_lipschitz (fA : f ∈ candidates α β) :
   lipschitz_with (2 * max_var α β) f :=
 begin
+  apply lipschitz_with.of_dist_le,
   rintros ⟨x, y⟩ ⟨z, t⟩,
   rw real.dist_eq,
   apply abs_le_of_le_of_neg_le,
@@ -172,7 +173,7 @@ end
 
 /-- candidates give rise to elements of bounded_continuous_functions -/
 def candidates_b_of_candidates (f : prod_space_fun α β) (fA : f ∈ candidates α β) : Cb α β :=
-bounded_continuous_function.mk_of_compact f (candidates_lipschitz fA).to_continuous
+bounded_continuous_function.mk_of_compact f (candidates_lipschitz fA).continuous
 
 lemma candidates_b_of_candidates_mem (f : prod_space_fun α β) (fA : f ∈ candidates α β) :
   candidates_b_of_candidates f fA ∈ candidates_b α β := fA
@@ -244,7 +245,7 @@ begin
         tendsto_const_nhds.mul tendsto_id,
       simpa using this },
     { assume x y f hf,
-      exact candidates_lipschitz hf _ _ } }
+      exact (candidates_lipschitz hf).dist_le _ _ } }
 end
 
 /-- We will then choose the candidate minimizing the Hausdorff distance. Except that we are not
@@ -390,7 +391,7 @@ max_le (le_trans (HD_lipschitz_aux1 f g) (add_le_add_right (le_max_left _ _) _))
 
 /-- Conclude that HD, being Lipschitz, is continuous -/
 private lemma HD_continuous : continuous (HD : Cb α β → ℝ) :=
-lipschitz_with.to_continuous (lipschitz_with.one_of_le_add HD_lipschitz_aux3)
+lipschitz_with.continuous (lipschitz_with.of_le_add HD_lipschitz_aux3)
 
 end constructions --section
 

src/topology/metric_space/hausdorff_distance.lean

@@ -458,12 +458,12 @@ variable (s)
 
 /-- The minimal distance to a set is Lipschitz in point with constant 1 -/
 lemma lipschitz_inf_dist_pt : lipschitz_with 1 (λx, inf_dist x s) :=
-lipschitz_with.one_of_le_add $ λ x y, inf_dist_le_inf_dist_add_dist
+lipschitz_with.of_le_add $ λ x y, inf_dist_le_inf_dist_add_dist
 
 /-- The minimal distance to a set is uniformly continuous in point -/
 lemma uniform_continuous_inf_dist_pt :
   uniform_continuous (λx, inf_dist x s) :=
-(lipschitz_inf_dist_pt s).to_uniform_continuous
+(lipschitz_inf_dist_pt s).uniform_continuous
 
 /-- The minimal distance to a set is continuous in point -/
 lemma continuous_inf_dist_pt : continuous (λx, inf_dist x s) :=