feat(Mathlib/Algebra/Order): add equivalent conditions to a ≤ b (#1…

…9166)

Two theorems that give equivalent conditions to `a ≤ b` in terms of `ε`-approximation.
- Generalize `a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε` (`le_iff_forall_one_lt_le_mul`) to monoids.
- Add `(hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε` for linearly ordered semifields.

the proofs were suggested by @fpvandoorn in [this thread](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.60le_iff_forall_pos_le_add.60.20for.20.60NNReal.60)

motivation: I will need them in the proof of regularity of `rieszContent`, that will be defined after #18775

Co-authored-by: Yoh Tanimoto <[email protected]>

Mathlib/Algebra/Order/Field/Basic.lean

@@ -435,6 +435,16 @@ theorem inv_pow_anti (a1 : 1 ≤ a) : Antitone fun n : ℕ => (a ^ n)⁻¹ := fu
 theorem inv_pow_strictAnti (a1 : 1 < a) : StrictAnti fun n : ℕ => (a ^ n)⁻¹ := fun _ _ =>
   inv_pow_lt_inv_pow_of_lt a1
 
+theorem le_iff_forall_one_lt_le_mul₀ {α : Type*} [LinearOrderedSemifield α]
+    {a b : α} (hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε := by
+  refine ⟨fun h _ hε ↦ h.trans <| le_mul_of_one_le_right hb hε.le, fun h ↦ ?_⟩
+  obtain rfl|hb := hb.eq_or_lt
+  · simp_rw [zero_mul] at h
+    exact h 2 one_lt_two
+  refine le_of_forall_le_of_dense fun x hbx => ?_
+  convert h (x / b) ((one_lt_div hb).mpr hbx)
+  rw [mul_div_cancel₀ _ hb.ne']
+
 /-! ### Results about `IsGLB` -/
 
 

Mathlib/Algebra/Order/Group/DenselyOrdered.lean

@@ -28,10 +28,6 @@ theorem le_of_forall_one_lt_div_le (h : ∀ ε : α, 1 < ε → a / ε ≤ b) :
   le_of_forall_lt_one_mul_le fun ε ε1 => by
     simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)
 
-@[to_additive]
-theorem le_iff_forall_one_lt_le_mul : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε :=
-  ⟨fun h _ ε_pos => le_mul_of_le_of_one_le h ε_pos.le, le_of_forall_one_lt_le_mul⟩
-
 @[to_additive]
 theorem le_iff_forall_lt_one_mul_le : a ≤ b ↔ ∀ ε < 1, a * ε ≤ b :=
   le_iff_forall_one_lt_le_mul (α := αᵒᵈ)

Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean

@@ -82,4 +82,9 @@ theorem le_iff_forall_one_lt_lt_mul' [MulLeftStrictMono α] :
     a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε :=
   ⟨fun h _ => lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul'⟩
 
+@[to_additive]
+theorem le_iff_forall_one_lt_le_mul [MulLeftStrictMono α] :
+    a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε :=
+  ⟨fun h _ hε ↦ lt_mul_of_le_of_one_lt h hε |>.le, le_of_forall_one_lt_le_mul⟩
+
 end ExistsMulOfLE