From e9a72ca8d70972c18afbfe4df49c287abd8bdab7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 7 Mar 2024 06:34:55 +0000 Subject: [PATCH] chore: Rename monotonicity of `/` lemmas (#10634) The new names and argument orders match the corresponding `*` lemmas, which I already took care of in a previous PR. From LeanAPAP --- .../Computation/Approximations.lean | 2 +- Mathlib/Algebra/Order/Field/Basic.lean | 76 +++++++++++-------- Mathlib/Algebra/Order/Field/Power.lean | 2 +- Mathlib/Algebra/Order/Floor.lean | 2 +- .../Complex/UpperHalfPlane/Metric.lean | 8 +- Mathlib/Analysis/Convex/Strong.lean | 5 +- .../Normed/Group/ControlledClosure.lean | 6 +- Mathlib/Analysis/NormedSpace/AddTorsor.lean | 2 +- Mathlib/Analysis/SpecialFunctions/Arsinh.lean | 2 + Mathlib/Analysis/SpecialFunctions/Exp.lean | 4 +- Mathlib/Analysis/Subadditive.lean | 2 +- Mathlib/Combinatorics/Additive/Behrend.lean | 16 ++-- Mathlib/Combinatorics/Schnirelmann.lean | 9 +-- Mathlib/Combinatorics/SetFamily/LYM.lean | 2 +- .../Combinatorics/SimpleGraph/Density.lean | 4 +- .../SimpleGraph/Regularity/Chunk.lean | 21 +++-- .../SimpleGraph/Regularity/Increment.lean | 7 +- Mathlib/Data/Real/NNReal.lean | 3 +- .../RotationNumber/TranslationNumber.lean | 4 +- .../Integral/DivergenceTheorem.lean | 7 +- Mathlib/Topology/UrysohnsLemma.lean | 4 +- 21 files changed, 96 insertions(+), 92 deletions(-) diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean b/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean index d784a6349a4173..0086dbc7a578de 100644 --- a/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean +++ b/Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean @@ -514,7 +514,7 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) : positivity rw [abs_of_pos this] rwa [this] - suffices 0 < denom ∧ denom ≤ denom' from div_le_div_of_le_left zero_le_one this.left this.right + suffices 0 < denom ∧ denom ≤ denom' from div_le_div_of_nonneg_left zero_le_one this.1 this.2 constructor · have : 0 < pred_conts.b + gp.b * conts.b := nextConts_b_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _ diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index 0bff91471eb237..4437c33fee648b 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -347,31 +347,43 @@ theorem one_le_inv_iff : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1 := @[mono, gcongr] -theorem div_le_div_of_le (hc : 0 ≤ c) (h : a ≤ b) : a / c ≤ b / c := by +lemma div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c := by rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c] - exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 hc) -#align div_le_div_of_le div_le_div_of_le + exact mul_le_mul_of_nonneg_right hab (one_div_nonneg.2 hc) +#align div_le_div_of_le_of_nonneg div_le_div_of_nonneg_right + +@[gcongr] +lemma div_lt_div_of_pos_right (h : a < b) (hc : 0 < c) : a / c < b / c := by + rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c] + exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc) +#align div_lt_div_of_lt div_lt_div_of_pos_right -- Not a `mono` lemma b/c `div_le_div` is strictly more general @[gcongr] -theorem div_le_div_of_le_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c := by +lemma div_le_div_of_nonneg_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c := by rw [div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_left ((inv_le_inv (hc.trans_le h) hc).mpr h) ha -#align div_le_div_of_le_left div_le_div_of_le_left - -@[deprecated div_le_div_of_le] -theorem div_le_div_of_le_of_nonneg (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c := - div_le_div_of_le hc hab -#align div_le_div_of_le_of_nonneg div_le_div_of_le_of_nonneg +#align div_le_div_of_le_left div_le_div_of_nonneg_left @[gcongr] -theorem div_lt_div_of_lt (hc : 0 < c) (h : a < b) : a / c < b / c := by - rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c] - exact mul_lt_mul_of_pos_right h (one_div_pos.2 hc) -#align div_lt_div_of_lt div_lt_div_of_lt +lemma div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / c := by + simpa only [div_eq_mul_inv, mul_lt_mul_left ha, inv_lt_inv (hc.trans h) hc] +#align div_lt_div_of_lt_left div_lt_div_of_pos_left + +-- 2024-02-16 +@[deprecated] alias div_le_div_of_le_of_nonneg := div_le_div_of_nonneg_right +@[deprecated] alias div_lt_div_of_lt := div_lt_div_of_pos_right +@[deprecated] alias div_le_div_of_le_left := div_le_div_of_nonneg_left +@[deprecated] alias div_lt_div_of_lt_left := div_lt_div_of_pos_left + +@[deprecated div_le_div_of_nonneg_right] +lemma div_le_div_of_le (hc : 0 ≤ c) (hab : a ≤ b) : a / c ≤ b / c := + div_le_div_of_nonneg_right hab hc +#align div_le_div_of_le div_le_div_of_le theorem div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b := - ⟨le_imp_le_of_lt_imp_lt <| div_lt_div_of_lt hc, div_le_div_of_le <| hc.le⟩ + ⟨le_imp_le_of_lt_imp_lt fun hab ↦ div_lt_div_of_pos_right hab hc, + fun hab ↦ div_le_div_of_nonneg_right hab hc.le⟩ #align div_le_div_right div_le_div_right theorem div_lt_div_right (hc : 0 < c) : a / c < b / c ↔ a < b := @@ -409,26 +421,21 @@ theorem div_lt_div' (hac : a ≤ c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) : a (div_lt_div_iff (d0.trans hbd) d0).2 (mul_lt_mul' hac hbd d0.le c0) #align div_lt_div' div_lt_div' -@[gcongr] -theorem div_lt_div_of_lt_left (hc : 0 < c) (hb : 0 < b) (h : b < a) : c / a < c / b := - (div_lt_div_left hc (hb.trans h) hb).mpr h -#align div_lt_div_of_lt_left div_lt_div_of_lt_left - /-! ### Relating one division and involving `1` -/ theorem div_le_self (ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a := by - simpa only [div_one] using div_le_div_of_le_left ha zero_lt_one hb + simpa only [div_one] using div_le_div_of_nonneg_left ha zero_lt_one hb #align div_le_self div_le_self theorem div_lt_self (ha : 0 < a) (hb : 1 < b) : a / b < a := by - simpa only [div_one] using div_lt_div_of_lt_left ha zero_lt_one hb + simpa only [div_one] using div_lt_div_of_pos_left ha zero_lt_one hb #align div_lt_self div_lt_self theorem le_div_self (ha : 0 ≤ a) (hb₀ : 0 < b) (hb₁ : b ≤ 1) : a ≤ a / b := by - simpa only [div_one] using div_le_div_of_le_left ha hb₀ hb₁ + simpa only [div_one] using div_le_div_of_nonneg_left ha hb₀ hb₁ #align le_div_self le_div_self theorem one_le_div (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by rw [le_div_iff hb, one_mul] @@ -562,6 +569,11 @@ theorem add_thirds (a : α) : a / 3 + a / 3 + a / 3 = a := by ### Miscellaneous lemmas -/ +@[simp] lemma div_pos_iff_of_pos_left (ha : 0 < a) : 0 < a / b ↔ 0 < b := by + simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos] + +@[simp] lemma div_pos_iff_of_pos_right (hb : 0 < b) : 0 < a / b ↔ 0 < a := by + simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)] theorem mul_le_mul_of_mul_div_le (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c := by rw [← mul_div_assoc] at h @@ -586,10 +598,14 @@ theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff hc₀]⟩ #align exists_pos_lt_mul exists_pos_lt_mul +lemma monotone_div_right_of_nonneg (ha : 0 ≤ a) : Monotone (· / a) := + fun _b _c hbc ↦ div_le_div_of_nonneg_right hbc ha + +lemma strictMono_div_right_of_pos (ha : 0 < a) : StrictMono (· / a) := + fun _b _c hbc ↦ div_lt_div_of_pos_right hbc ha + theorem Monotone.div_const {β : Type*} [Preorder β] {f : β → α} (hf : Monotone f) {c : α} - (hc : 0 ≤ c) : Monotone fun x => f x / c := by - haveI := @LinearOrder.decidableLE α _ - simpa only [div_eq_mul_inv] using (monotone_mul_right_of_nonneg (inv_nonneg.2 hc)).comp hf + (hc : 0 ≤ c) : Monotone fun x => f x / c := (monotone_div_right_of_nonneg hc).comp hf #align monotone.div_const Monotone.div_const theorem StrictMono.div_const {β : Type*} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α} @@ -603,20 +619,20 @@ instance (priority := 100) LinearOrderedSemiField.toDenselyOrdered : DenselyOrde ⟨(a₁ + a₂) / 2, calc a₁ = (a₁ + a₁) / 2 := (add_self_div_two a₁).symm - _ < (a₁ + a₂) / 2 := div_lt_div_of_lt zero_lt_two (add_lt_add_left h _) + _ < (a₁ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_left h _) zero_lt_two , calc - (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := div_lt_div_of_lt zero_lt_two (add_lt_add_right h _) + (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_right h _) zero_lt_two _ = a₂ := add_self_div_two a₂ ⟩ #align linear_ordered_field.to_densely_ordered LinearOrderedSemiField.toDenselyOrdered theorem min_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : min (a / c) (b / c) = min a b / c := - Eq.symm <| Monotone.map_min fun _ _ => div_le_div_of_le hc + (monotone_div_right_of_nonneg hc).map_min.symm #align min_div_div_right min_div_div_right theorem max_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : max (a / c) (b / c) = max a b / c := - Eq.symm <| Monotone.map_max fun _ _ => div_le_div_of_le hc + (monotone_div_right_of_nonneg hc).map_max.symm #align max_div_div_right max_div_div_right theorem one_div_strictAntiOn : StrictAntiOn (fun x : α => 1 / x) (Set.Ioi 0) := diff --git a/Mathlib/Algebra/Order/Field/Power.lean b/Mathlib/Algebra/Order/Field/Power.lean index c1872af5ca5829..54949135a9f290 100644 --- a/Mathlib/Algebra/Order/Field/Power.lean +++ b/Mathlib/Algebra/Order/Field/Power.lean @@ -237,7 +237,7 @@ theorem Nat.cast_le_pow_sub_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ (a ^ n `Nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator. -/ theorem Nat.cast_le_pow_div_sub (H : 1 < a) (n : ℕ) : (n : α) ≤ a ^ n / (a - 1) := (n.cast_le_pow_sub_div_sub H).trans <| - div_le_div_of_le (sub_nonneg.2 H.le) (sub_le_self _ zero_le_one) + div_le_div_of_nonneg_right (sub_le_self _ zero_le_one) (sub_nonneg.2 H.le) #align nat.cast_le_pow_div_sub Nat.cast_le_pow_div_sub end LinearOrderedField diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean index 34f8305b66c10d..0310adb3a3b327 100644 --- a/Mathlib/Algebra/Order/Floor.lean +++ b/Mathlib/Algebra/Order/Floor.lean @@ -542,7 +542,7 @@ theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by refine' (floor_eq_iff _).2 _ · exact div_nonneg ha n.cast_nonneg constructor - · exact cast_div_le.trans (div_le_div_of_le n.cast_nonneg (floor_le ha)) + · exact cast_div_le.trans (div_le_div_of_nonneg_right (floor_le ha) n.cast_nonneg) rw [div_lt_iff, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha] · exact lt_div_mul_add hn · exact cast_pos.2 hn diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean index f3b40a0249970d..a10d4a68ae2f19 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean @@ -245,9 +245,11 @@ theorem dist_log_im_le (z w : ℍ) : dist (log z.im) (log w.im) ≤ dist z w := calc dist (log z.im) (log w.im) = dist (mk ⟨0, z.im⟩ z.im_pos) (mk ⟨0, w.im⟩ w.im_pos) := Eq.symm <| dist_of_re_eq rfl - _ ≤ dist z w := mul_le_mul_of_nonneg_left (arsinh_le_arsinh.2 <| - div_le_div_of_le (mul_nonneg zero_le_two (sqrt_nonneg _)) <| by - simpa [sqrt_sq_eq_abs] using Complex.abs_im_le_abs (z - w)) zero_le_two + _ ≤ dist z w := by + simp_rw [dist_eq] + gcongr + · simpa [sqrt_sq_eq_abs] using Complex.abs_im_le_abs (z - w) + · simp #align upper_half_plane.dist_log_im_le UpperHalfPlane.dist_log_im_le theorem im_le_im_mul_exp_dist (z w : ℍ) : z.im ≤ w.im * Real.exp (dist z w) := by diff --git a/Mathlib/Analysis/Convex/Strong.lean b/Mathlib/Analysis/Convex/Strong.lean index 5b4dadffcf5dfd..f356e6e5cead32 100644 --- a/Mathlib/Analysis/Convex/Strong.lean +++ b/Mathlib/Analysis/Convex/Strong.lean @@ -127,11 +127,10 @@ def StrongConcaveOn (s : Set E) (m : ℝ) : (E → ℝ) → Prop := variable {s : Set E} {f : E → ℝ} {m n : ℝ} nonrec lemma StrongConvexOn.mono (hmn : m ≤ n) (hf : StrongConvexOn s n f) : StrongConvexOn s m f := - hf.mono fun r ↦ mul_le_mul_of_nonneg_right (div_le_div_of_le zero_le_two hmn) <| by positivity + hf.mono fun r ↦ by gcongr nonrec lemma StrongConcaveOn.mono (hmn : m ≤ n) (hf : StrongConcaveOn s n f) : - StrongConcaveOn s m f := - hf.mono fun r ↦ mul_le_mul_of_nonneg_right (div_le_div_of_le zero_le_two hmn) <| by positivity + StrongConcaveOn s m f := hf.mono fun r ↦ by gcongr @[simp] lemma strongConvexOn_zero : StrongConvexOn s 0 f ↔ ConvexOn ℝ s f := by simp [StrongConvexOn, ← Pi.zero_def] diff --git a/Mathlib/Analysis/Normed/Group/ControlledClosure.lean b/Mathlib/Analysis/Normed/Group/ControlledClosure.lean index 7f0dc66a8a1712..32575bf4a3490e 100644 --- a/Mathlib/Analysis/Normed/Group/ControlledClosure.lean +++ b/Mathlib/Analysis/Normed/Group/ControlledClosure.lean @@ -44,11 +44,7 @@ theorem controlled_closure_of_complete {f : NormedAddGroupHom G H} {K : AddSubgr of a sequence `v` of elements of `K` which starts close to `h` and then quickly goes to zero. The sequence `b` below quantifies this. -/ set b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C - have b_pos : ∀ i, 0 < b i := by - intro i - field_simp [b, hC] - exact - div_pos (mul_pos hε (norm_pos_iff.mpr hyp_h)) (mul_pos (by norm_num : (0 : ℝ) < 2 ^ i * 2) hC) + have b_pos (i) : 0 < b i := by field_simp [b, hC, hyp_h] obtain ⟨v : ℕ → H, lim_v : Tendsto (fun n : ℕ => ∑ k in range (n + 1), v k) atTop (𝓝 h), v_in : ∀ n, v n ∈ K, hv₀ : ‖v 0 - h‖ < b 0, hv : ∀ n > 0, ‖v n‖ < b n⟩ := diff --git a/Mathlib/Analysis/NormedSpace/AddTorsor.lean b/Mathlib/Analysis/NormedSpace/AddTorsor.lean index 4d47866a86497d..26116f4d0f5583 100644 --- a/Mathlib/Analysis/NormedSpace/AddTorsor.lean +++ b/Mathlib/Analysis/NormedSpace/AddTorsor.lean @@ -214,7 +214,7 @@ theorem dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) : rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint] try infer_instance rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul] - exact div_le_div_of_le (norm_nonneg _) (norm_add_le _ _) + exact div_le_div_of_nonneg_right (norm_add_le _ _) (norm_nonneg _) #align dist_midpoint_midpoint_le' dist_midpoint_midpoint_le' theorem nndist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) : diff --git a/Mathlib/Analysis/SpecialFunctions/Arsinh.lean b/Mathlib/Analysis/SpecialFunctions/Arsinh.lean index 6dc3283b729657..53cc8682b010b4 100644 --- a/Mathlib/Analysis/SpecialFunctions/Arsinh.lean +++ b/Mathlib/Analysis/SpecialFunctions/Arsinh.lean @@ -148,6 +148,8 @@ theorem arsinh_le_arsinh : arsinh x ≤ arsinh y ↔ x ≤ y := sinhOrderIso.symm.le_iff_le #align real.arsinh_le_arsinh Real.arsinh_le_arsinh +@[gcongr] protected alias ⟨_, GCongr.arsinh_le_arsinh⟩ := arsinh_le_arsinh + @[simp] theorem arsinh_lt_arsinh : arsinh x < arsinh y ↔ x < y := sinhOrderIso.symm.lt_iff_lt diff --git a/Mathlib/Analysis/SpecialFunctions/Exp.lean b/Mathlib/Analysis/SpecialFunctions/Exp.lean index c1f107bda376df..297e89a16b81d5 100644 --- a/Mathlib/Analysis/SpecialFunctions/Exp.lean +++ b/Mathlib/Analysis/SpecialFunctions/Exp.lean @@ -235,9 +235,7 @@ theorem tendsto_exp_div_pow_atTop (n : ℕ) : Tendsto (fun x => exp x / x ^ n) a calc x ^ n ≤ ⌈x⌉₊ ^ n := mod_cast pow_le_pow_left hx₀.le (Nat.le_ceil _) _ _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le - _ ≤ exp (x + 1) / (exp 1 * C) := - (div_le_div_of_le (mul_pos (exp_pos _) hC₀).le - (exp_le_exp.2 <| (Nat.ceil_lt_add_one hx₀.le).le)) + _ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne'] #align real.tendsto_exp_div_pow_at_top Real.tendsto_exp_div_pow_atTop diff --git a/Mathlib/Analysis/Subadditive.lean b/Mathlib/Analysis/Subadditive.lean index 0b6148dabb6552..8f6ae3b927f0a1 100644 --- a/Mathlib/Analysis/Subadditive.lean +++ b/Mathlib/Analysis/Subadditive.lean @@ -78,7 +78,7 @@ theorem eventually_div_lt_of_div_lt {L : ℝ} {n : ℕ} (hn : n ≠ 0) (hL : u n rw [mul_comm] refine lt_of_le_of_lt ?_ hk simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul] - exact div_le_div_of_le (Nat.cast_nonneg _) (h.apply_mul_add_le _ _ _) + exact div_le_div_of_nonneg_right (h.apply_mul_add_le _ _ _) (Nat.cast_nonneg _) #align subadditive.eventually_div_lt_of_div_lt Subadditive.eventually_div_lt_of_div_lt /-- Fekete's lemma: a subadditive sequence which is bounded below converges. -/ diff --git a/Mathlib/Combinatorics/Additive/Behrend.lean b/Mathlib/Combinatorics/Additive/Behrend.lean index 18d8beaa1a3d97..b2def5cb5f790f 100644 --- a/Mathlib/Combinatorics/Additive/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/Behrend.lean @@ -256,7 +256,7 @@ theorem exists_large_sphere (n d : ℕ) : · simp obtain rfl | hd := d.eq_zero_or_pos · simp - refine' (div_le_div_of_le_left _ _ _).trans hk + refine' (div_le_div_of_nonneg_left _ _ _).trans hk · exact cast_nonneg _ · exact cast_add_one_pos _ simp only [← le_sub_iff_add_le', cast_mul, ← mul_sub, cast_pow, cast_sub hd, sub_sq, one_pow, @@ -327,13 +327,11 @@ theorem le_sqrt_log (hN : 4096 ≤ N) : log (2 / (1 - 2 / exp 1)) * (69 / 50) theorem exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : exp (-2 * x) < exp (2 - ⌈x⌉₊) / ⌈x⌉₊ := by have h₁ := ceil_lt_add_one hx.le - have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by - rw [_root_.le_sub_iff_add_le] - apply (add_le_add_left h₁.le _).trans_eq - rw [← add_assoc, sub_add_cancel] - linarith - refine' lt_of_le_of_lt _ (div_lt_div_of_lt_left (exp_pos _) (cast_pos.2 <| ceil_pos.2 hx) h₁) - refine' le_trans _ (div_le_div_of_le (add_nonneg hx.le zero_le_one) (exp_le_exp.2 h₂)) + have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith + calc + _ ≤ exp (1 - x) / (x + 1) := ?_ + _ ≤ exp (2 - ⌈x⌉₊) / (x + 1) := by gcongr + _ < _ := by gcongr rw [le_div_iff (add_pos hx zero_lt_one), ← le_div_iff' (exp_pos _), ← exp_sub, neg_mul, sub_neg_eq_add, two_mul, sub_add_add_cancel, add_comm _ x] exact le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _) @@ -429,7 +427,7 @@ set_option linter.uppercaseLean3 false in theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dValue N := by apply div_lt_floor _ rw [← log_le_log_iff, log_rpow, mul_comm, ← div_eq_mul_inv] - · apply le_trans _ (div_le_div_of_le_left _ _ (ceil_lt_mul _).le) + · apply le_trans _ (div_le_div_of_nonneg_left _ _ (ceil_lt_mul _).le) rw [mul_comm, ← div_div, div_sqrt, le_div_iff] · set_option tactic.skipAssignedInstances false in norm_num; exact le_sqrt_log hN · norm_num1 diff --git a/Mathlib/Combinatorics/Schnirelmann.lean b/Mathlib/Combinatorics/Schnirelmann.lean index b302f50b2a6998..927113d4a9928e 100644 --- a/Mathlib/Combinatorics/Schnirelmann.lean +++ b/Mathlib/Combinatorics/Schnirelmann.lean @@ -93,7 +93,7 @@ lemma schnirelmannDensity_le_of_not_mem {k : ℕ} (hk : k ∉ A) : · simpa using schnirelmannDensity_le_one apply schnirelmannDensity_le_of_le k hk'.ne' rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne'] - apply div_le_div_of_le (Nat.cast_nonneg _) + gcongr rw [← Nat.cast_pred hk', Nat.cast_le] suffices (Ioc 0 k).filter (· ∈ A) ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp) rw [← Ioo_insert_right hk', filter_insert, if_neg hk] @@ -106,8 +106,8 @@ lemma schnirelmannDensity_eq_zero_of_one_not_mem (h : 1 ∉ A) : schnirelmannDen /-- The Schnirelmann density is increasing with the set. -/ lemma schnirelmannDensity_le_of_subset {B : Set ℕ} [DecidablePred (· ∈ B)] (h : A ⊆ B) : schnirelmannDensity A ≤ schnirelmannDensity B := - ciInf_mono ⟨0, fun _ ⟨_, hx⟩ => hx ▸ by positivity⟩ fun _ => div_le_div_of_le (by positivity) <| - Nat.cast_le.2 <| card_le_card <| monotone_filter_right _ h + ciInf_mono ⟨0, fun _ ⟨_, hx⟩ ↦ hx ▸ by positivity⟩ fun _ ↦ by + gcongr; exact monotone_filter_right _ h /-- The Schnirelmann density of `A` is `1` if and only if `A` contains all the positive naturals. -/ lemma schnirelmannDensity_eq_one_iff : schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A := by @@ -196,8 +196,7 @@ lemma schnirelmannDensity_finset (A : Finset ℕ) : schnirelmannDensity A = 0 := have hn : 0 < n := Nat.succ_pos _ use n, hn rw [div_lt_iff (Nat.cast_pos.2 hn), ← div_lt_iff' hε, Nat.cast_add_one] - exact (Nat.lt_floor_add_one _).trans_le' <| div_le_div_of_le hε.le <| Nat.cast_le.2 <| - card_le_card <| by simp [subset_iff] + exact (Nat.lt_floor_add_one _).trans_le' <| by gcongr; simp [subset_iff] /-- The Schnirelmann density of any finite set is `0`. -/ lemma schnirelmannDensity_finite {A : Set ℕ} [DecidablePred (· ∈ A)] (hA : A.Finite) : diff --git a/Mathlib/Combinatorics/SetFamily/LYM.lean b/Mathlib/Combinatorics/SetFamily/LYM.lean index b4c66643f7e19e..eb0b36470c571f 100644 --- a/Mathlib/Combinatorics/SetFamily/LYM.lean +++ b/Mathlib/Combinatorics/SetFamily/LYM.lean @@ -240,7 +240,7 @@ theorem IsAntichain.sperner [Fintype α] {𝒜 : Finset (Finset α)} rw [Iic_eq_Icc, ← Ico_succ_right, bot_eq_zero, Ico_zero_eq_range] refine' (sum_le_sum fun r hr => _).trans (sum_card_slice_div_choose_le_one h𝒜) rw [mem_range] at hr - refine' div_le_div_of_le_left _ _ _ <;> norm_cast + refine' div_le_div_of_nonneg_left _ _ _ <;> norm_cast · exact Nat.zero_le _ · exact choose_pos (Nat.lt_succ_iff.1 hr) · exact choose_le_middle _ _ diff --git a/Mathlib/Combinatorics/SimpleGraph/Density.lean b/Mathlib/Combinatorics/SimpleGraph/Density.lean index e5ab58585e7e3a..b48007f1bbfb0d 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Density.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Density.lean @@ -186,8 +186,8 @@ theorem mul_edgeDensity_le_edgeDensity (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (s₂.card : ℚ) / s₁.card * (t₂.card / t₁.card) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁ := by have hst : (s₂.card : ℚ) * t₂.card ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty] rw [edgeDensity, edgeDensity, div_mul_div_comm, mul_comm, div_mul_div_cancel _ hst] - refine' div_le_div_of_le (mod_cast (s₁.card * t₁.card).zero_le) _ - exact mod_cast card_le_card (interedges_mono hs ht) + gcongr + exact interedges_mono hs ht #align rel.mul_edge_density_le_edge_density Rel.mul_edgeDensity_le_edgeDensity theorem edgeDensity_sub_edgeDensity_le_one_sub_mul (hs : s₂ ⊆ s₁) (ht : t₂ ⊆ t₁) (hs₂ : s₂.Nonempty) diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean index c314ff8f8648c4..13f87073c57ee4 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean @@ -356,7 +356,7 @@ private theorem edgeDensity_chunk_aux [Nonempty α] · refine' (sub_nonpos_of_le <| (sq_le _ _).trans <| hGε.trans _).trans (sq_nonneg _) · exact mod_cast G.edgeDensity_nonneg _ _ · exact mod_cast G.edgeDensity_le_one _ _ - · exact div_le_div_of_le_left (by sz_positivity) (by norm_num) (by norm_num) + · exact div_le_div_of_nonneg_left (by sz_positivity) (by norm_num) (by norm_num) rw [← sub_nonneg] at hGε have : ↑(G.edgeDensity U V) - ε ^ 5 / ↑50 ≤ (∑ ab in (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, @@ -393,15 +393,14 @@ private theorem eps_le_card_star_div [Nonempty α] (hPα : P.parts.card * 16 ^ P have hm : (0 : ℝ) ≤ 1 - (↑m)⁻¹ := sub_nonneg_of_le (inv_le_one <| one_le_m_coe hPα) have hε : 0 ≤ 1 - ε / 10 := sub_nonneg_of_le (div_le_one_of_le (hε₁.trans <| by norm_num) <| by norm_num) + have hε₀ : 0 < ε := by sz_positivity calc 4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num - _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * ((G.nonuniformWitness ε U V).card / U.card) := - (mul_le_mul (mul_le_mul (sub_le_sub_left (div_le_div_of_le (by norm_num) hε₁) _) - (sub_le_sub_left (inv_le_inv_of_le (by norm_num) <| - mod_cast (show 9 ≤ 100 by norm_num).trans - (hundred_le_m hPα hPε hε₁)) _) (by norm_num) hε) - ((le_div_iff' <| (@cast_pos ℝ _ _ _).2 (P.nonempty_of_mem_parts hU).card_pos).2 <| - G.le_card_nonuniformWitness hunif) (by sz_positivity) (by positivity)) + _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * ((G.nonuniformWitness ε U V).card / U.card) := by + gcongr + exacts [mod_cast (show 9 ≤ 100 by norm_num).trans (hundred_le_m hPα hPε hε₁), + (le_div_iff' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <| + G.le_card_nonuniformWitness hunif] _ = (1 - ε / 10) * (G.nonuniformWitness ε U V).card * ((1 - (↑m)⁻¹) / U.card) := by rw [mul_assoc, mul_assoc, mul_div_left_comm] _ ≤ ((star hP G ε hU V).biUnion id).card * ((1 - (↑m)⁻¹) / U.card) := @@ -410,7 +409,7 @@ private theorem eps_le_card_star_div [Nonempty α] (hPα : P.parts.card * 16 ^ P _ ≤ (star hP G ε hU V).card * (m + 1) * ((1 - (↑m)⁻¹) / U.card) := (mul_le_mul_of_nonneg_right card_biUnion_star_le_m_add_one_card_star_mul (by positivity)) _ ≤ (star hP G ε hU V).card * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ P.parts.card * m)) := - (mul_le_mul_of_nonneg_left (div_le_div_of_le_left hm (by sz_positivity) <| + (mul_le_mul_of_nonneg_left (div_le_div_of_nonneg_left hm (by sz_positivity) <| pow_mul_m_le_card_part hP hU) (by positivity)) _ ≤ (star hP G ε hU V).card / ↑4 ^ P.parts.card := by rw [mul_assoc, mul_comm ((4 : ℝ) ^ P.parts.card), ← div_div, ← mul_div_assoc, ← mul_comm_div] @@ -462,9 +461,7 @@ private theorem edgeDensity_star_not_uniform [Nonempty α] exact this have hε' : ε ^ 5 ≤ ε := by simpa using pow_le_pow_of_le_one (by sz_positivity) hε₁ (show 1 ≤ 5 by norm_num) - have hpr' : |p - r| ≤ ε / 49 := hpr.trans (div_le_div_of_le (by norm_num) hε') - have hqt' : |q - t| ≤ ε / 49 := hqt.trans (div_le_div_of_le (by norm_num) hε') - rw [abs_sub_le_iff] at hrs hpr' hqt' + rw [abs_sub_le_iff] at hrs hpr hqt rw [le_abs] at hst ⊢ cases hst left; linarith diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean index 8352d16887eace..096831555b3b97 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean @@ -146,8 +146,7 @@ theorem energy_increment (hP : P.IsEquipartition) (hP₇ : 7 ≤ P.parts.card) P.parts.card ^ 2 * (ε ^ 5 / 4) : ℝ) / P.parts.card ^ 2 := by rw [coe_energy, add_div, mul_div_cancel_left]; positivity _ ≤ (∑ x in P.parts.offDiag.attach, (∑ i in distinctPairs G ε hP x, - G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ P.parts.card) / P.parts.card ^ 2 := - div_le_div_of_le (by positivity) ?_ + G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ P.parts.card) / P.parts.card ^ 2 := ?_ _ = (∑ x in P.parts.offDiag.attach, ∑ i in distinctPairs G ε hP x, G.edgeDensity i.1 i.2 ^ 2 : ℝ) / (increment hP G ε).parts.card ^ 2 := by rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm, @@ -157,6 +156,7 @@ theorem energy_increment (hP : P.IsEquipartition) (hP₇ : 7 ≤ P.parts.card) gcongr rw [← sum_biUnion pairwiseDisjoint_distinctPairs] exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _ + gcongr rw [Finpartition.IsUniform, not_le, mul_tsub, mul_one, ← offDiag_card] at hPG calc _ ≤ ∑ x in P.parts.offDiag, (edgeDensity G x.1 x.2 : ℝ) ^ 2 + @@ -180,8 +180,7 @@ theorem energy_increment (hP : P.IsEquipartition) (hP₇ : 7 ≤ P.parts.card) nlinarith · norm_num _ = (P.parts.offDiag.card * ε * (ε ^ 4 / 3) - P.parts.offDiag.card * (ε ^ 5 / 25)) := by ring - _ ≤ ((nonUniforms P G ε).card * (ε ^ 4 / 3) - P.parts.offDiag.card * (ε ^ 5 / 25)) := by - gcongr + _ ≤ ((nonUniforms P G ε).card * (ε ^ 4 / 3) - P.parts.offDiag.card * (ε ^ 5 / 25)) := by gcongr #align szemeredi_regularity.energy_increment SzemerediRegularity.energy_increment end SzemerediRegularity diff --git a/Mathlib/Data/Real/NNReal.lean b/Mathlib/Data/Real/NNReal.lean index 5ff454ac21382e..85879ce1192842 100644 --- a/Mathlib/Data/Real/NNReal.lean +++ b/Mathlib/Data/Real/NNReal.lean @@ -955,10 +955,9 @@ theorem mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) : a * r < b := (lt_div_iff fun hr => False.elim <| by simp [hr] at h).1 h #align nnreal.mul_lt_of_lt_div NNReal.mul_lt_of_lt_div --- Porting note: drop an unneeded assumption, assume `≠ 0` theorem div_le_div_left_of_le {a b c : ℝ≥0} (c0 : c ≠ 0) (cb : c ≤ b) : a / b ≤ a / c := - div_le_div_of_le_left (zero_le _) c0.bot_lt cb + div_le_div_of_nonneg_left (zero_le _) c0.bot_lt cb #align nnreal.div_le_div_left_of_le NNReal.div_le_div_left_of_leₓ nonrec theorem div_le_div_left {a b c : ℝ≥0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) : diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean index 7b3f71b9925dda..1e120b39235b22 100644 --- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean +++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean @@ -804,8 +804,8 @@ theorem tendsto_translation_number' (x : ℝ) : #align circle_deg1_lift.tendsto_translation_number' CircleDeg1Lift.tendsto_translation_number' theorem translationNumber_mono : Monotone τ := fun f g h => - le_of_tendsto_of_tendsto' f.tendsto_translation_number₀ g.tendsto_translation_number₀ fun n => - div_le_div_of_le n.cast_nonneg (pow_mono h n 0) + le_of_tendsto_of_tendsto' f.tendsto_translation_number₀ g.tendsto_translation_number₀ fun n => by + gcongr; exact pow_mono h _ _ #align circle_deg1_lift.translation_number_mono CircleDeg1Lift.translationNumber_mono theorem translationNumber_translate (x : ℝ) : τ (translate <| Multiplicative.ofAdd x) = x := diff --git a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean index 3b69621ce089b8..96ba4f44a95e0f 100644 --- a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean +++ b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean @@ -240,10 +240,9 @@ theorem integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ (I : Box ( _ ≤ ε := by rw [Box.Icc_def, Real.volume_Icc_pi_toReal ((J k).face i).lower_le_upper, ← le_div_iff (hvol_pos _)] - refine' div_le_div_of_le_left εpos.le (hvol_pos _) - (prod_le_prod (fun j _ => _) fun j _ => _) - exacts [sub_nonneg.2 (Box.lower_le_upper _ _), - sub_le_sub ((hJ_sub' _ (J _).upper_mem_Icc).2 _) ((hJ_sub' _ (J _).lower_mem_Icc).1 _)] + gcongr + exacts [hvol_pos _, fun _ _ ↦ sub_nonneg.2 (Box.lower_le_upper _ _), + (hJ_sub' _ (J _).upper_mem_Icc).2 _, (hJ_sub' _ (J _).lower_mem_Icc).1 _] #align measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_aux₂ MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ variable (a b : Fin (n + 1) → ℝ) diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean index 225e2e30e91474..048cd0b71088a9 100644 --- a/Mathlib/Topology/UrysohnsLemma.lean +++ b/Mathlib/Topology/UrysohnsLemma.lean @@ -305,8 +305,8 @@ theorem continuous_lim (c : CU P) : Continuous c.lim := by simp only [pow_succ, c.lim_eq_midpoint, c.left.lim_eq_midpoint, c.left.left.lim_of_nmem_U _ hxl, c.left.left.lim_of_nmem_U _ hyl] refine' (dist_midpoint_midpoint_le _ _ _ _).trans _ - refine' (div_le_div_of_le zero_le_two - (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _)).trans _ + refine' (div_le_div_of_nonneg_right (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _) + zero_le_two).trans _ rw [dist_self, zero_add] set r := (3 / 4 : ℝ) ^ n calc _ ≤ (r / 2 + r) / 2 := by gcongr