feat(data/real/nnreal): add mul csupr/cinfi lemmas (#13936)

Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

src/algebra/order/with_zero.lean

@@ -285,15 +285,43 @@ end
 lemma mul_le_mul_right₀ (hc : c ≠ 0) : a * c ≤ b * c ↔ a ≤ b :=
 ⟨le_of_le_mul_right hc, λ hab, mul_le_mul_right' hab _⟩
 
+lemma mul_le_mul_left₀ (ha : a ≠ 0) : a * b ≤ a * c ↔ b ≤ c :=
+by {simp only [mul_comm a], exact mul_le_mul_right₀ ha }
+
 lemma div_le_div_right₀ (hc : c ≠ 0) : a/c ≤ b/c ↔ a ≤ b :=
 by rw [div_eq_mul_inv, div_eq_mul_inv, mul_le_mul_right₀ (inv_ne_zero hc)]
 
+lemma div_le_div_left₀ (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : a/b ≤ a/c ↔ c ≤ b :=
+by simp only [div_eq_mul_inv, mul_le_mul_left₀ ha, inv_le_inv₀ hb hc]
+
 lemma le_div_iff₀ (hc : c ≠ 0) : a ≤ b/c ↔ a*c ≤ b :=
 by rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]
 
 lemma div_le_iff₀ (hc : c ≠ 0) : a/c ≤ b ↔ a ≤ b*c :=
 by rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]
 
+/-- `equiv.mul_left₀` as an order_iso on a `linear_ordered_comm_group_with_zero.`.
+
+Note that `order_iso.mul_left₀` refers to the `linear_ordered_field` version. -/
+@[simps apply to_equiv {simp_rhs := tt}]
+def order_iso.mul_left₀' {a : α} (ha : a ≠ 0) : α ≃o α :=
+{ map_rel_iff' := λ x y,  mul_le_mul_left₀ ha, ..equiv.mul_left₀ a ha }
+
+lemma order_iso.mul_left₀'_symm {a : α} (ha : a ≠ 0) :
+  (order_iso.mul_left₀' ha).symm = order_iso.mul_left₀' (inv_ne_zero ha) :=
+by { ext, refl }
+
+/-- `equiv.mul_right₀` as an order_iso on a `linear_ordered_comm_group_with_zero.`.
+
+Note that `order_iso.mul_right₀` refers to the `linear_ordered_field` version. -/
+@[simps apply to_equiv {simp_rhs := tt}]
+def order_iso.mul_right₀' {a : α} (ha : a ≠ 0) : α ≃o α :=
+{ map_rel_iff' := λ _ _, mul_le_mul_right₀ ha, ..equiv.mul_right₀ a ha }
+
+lemma order_iso.mul_right₀'_symm {a : α} (ha : a ≠ 0) :
+  (order_iso.mul_right₀' ha).symm = order_iso.mul_right₀' (inv_ne_zero ha) :=
+by { ext, refl }
+
 instance : linear_ordered_add_comm_group_with_top (additive αᵒᵈ) :=
 { neg_top := inv_zero,
   add_neg_cancel := λ a ha, mul_inv_cancel ha,

src/data/real/basic.lean

@@ -484,6 +484,9 @@ end
 theorem Sup_of_not_bdd_above {s : set ℝ} (hs : ¬ bdd_above s) : Sup s = 0 :=
 dif_neg $ assume h, hs h.2
 
+lemma supr_of_not_bdd_above {α : Sort*} {f : α → ℝ} (hf : ¬ bdd_above (set.range f)) :
+  (⨆ i, f i) = 0 := Sup_of_not_bdd_above hf
+
 theorem Sup_univ : Sup (@set.univ ℝ) = 0 :=
 real.Sup_of_not_bdd_above $ λ ⟨x, h⟩, not_le_of_lt (lt_add_one _) $ h (set.mem_univ _)
 
@@ -503,6 +506,9 @@ end
 theorem Inf_of_not_bdd_below {s : set ℝ} (hs : ¬ bdd_below s) : Inf s = 0 :=
 neg_eq_zero.2 $ Sup_of_not_bdd_above $ mt bdd_above_neg.1 hs
 
+lemma infi_of_not_bdd_below  {α : Sort*} {f : α → ℝ} (hf : ¬ bdd_below (set.range f)) :
+  (⨅ i, f i) = 0 := Inf_of_not_bdd_below hf
+
 /--
 As `0` is the default value for `real.Sup` of the empty set or sets which are not bounded above, it
 suffices to show that `S` is bounded below by `0` to show that `0 ≤ Inf S`.

src/data/real/nnreal.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import algebra.big_operators.ring
-import data.real.basic
+import data.real.pointwise
 import algebra.indicator_function
 import algebra.algebra.basic
+import algebra.order.module
 import algebra.order.nonneg
 
 /-!
@@ -735,6 +736,75 @@ end inv
 @[simp] lemma abs_eq (x : ℝ≥0) : |(x : ℝ)| = x :=
 abs_of_nonneg x.property
 
+section csupr
+open set
+
+variables {ι : Sort*} {f : ι → ℝ≥0}
+
+lemma le_to_nnreal_of_coe_le {x : ℝ≥0} {y : ℝ} (h : ↑x ≤ y) : x ≤ y.to_nnreal :=
+(le_to_nnreal_iff_coe_le $ x.2.trans h).2 h
+
+lemma Sup_of_not_bdd_above {s : set ℝ≥0} (hs : ¬bdd_above s) : has_Sup.Sup s = 0 :=
+begin
+  rw [← bdd_above_coe] at hs,
+  rw [← nnreal.coe_eq, coe_Sup],
+  exact Sup_of_not_bdd_above hs,
+end
+
+lemma supr_of_not_bdd_above (hf : ¬ bdd_above (range f)) : (⨆ i, f i) = 0 :=
+Sup_of_not_bdd_above hf
+
+lemma infi_empty [is_empty ι] (f : ι → ℝ≥0) : (⨅ i, f i) = 0 :=
+by { rw [← nnreal.coe_eq, coe_infi], exact real.cinfi_empty _, }
+
+@[simp] lemma infi_const_zero {α : Sort*} : (⨅ i : α, (0 : ℝ≥0)) = 0 :=
+by { rw [← nnreal.coe_eq, coe_infi], exact real.cinfi_const_zero, }
+
+lemma infi_mul (f : ι → ℝ≥0) (a : ℝ≥0)  : infi f * a = ⨅ i, f i * a :=
+begin
+  rw [← nnreal.coe_eq, nnreal.coe_mul, coe_infi, coe_infi],
+  exact real.infi_mul_of_nonneg (nnreal.coe_nonneg _) _,
+end
+
+lemma mul_infi (f : ι → ℝ≥0) (a : ℝ≥0) : a * infi f = ⨅ i, a * f i :=
+by simpa only [mul_comm] using infi_mul f a
+
+lemma mul_supr (f : ι → ℝ≥0) (a : ℝ≥0) : a * (⨆ i, f i) = ⨆ i, a * f i :=
+begin
+  rw [← nnreal.coe_eq, nnreal.coe_mul, nnreal.coe_supr, nnreal.coe_supr],
+  exact real.mul_supr_of_nonneg (nnreal.coe_nonneg _) _,
+end
+
+lemma supr_mul (f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) * a = ⨆ i, f i * a :=
+by { rw [mul_comm, mul_supr], simp_rw [mul_comm] }
+
+lemma supr_div (f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) / a = ⨆ i, f i / a :=
+by simp only [div_eq_mul_inv, supr_mul]
+
+variable [nonempty ι]
+
+lemma le_mul_infi {a : ℝ≥0} {g : ℝ≥0} {h : ι → ℝ≥0} (H : ∀ j, a ≤ g * h j) : a ≤ g * infi h :=
+by { rw [mul_infi], exact le_cinfi H }
+
+lemma mul_supr_le {a : ℝ≥0} {g : ℝ≥0} {h : ι → ℝ≥0} (H : ∀ j, g * h j ≤ a) : g * supr h ≤ a :=
+by { rw [mul_supr], exact csupr_le H }
+
+lemma le_infi_mul {a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, a ≤ g i * h) : a ≤ infi g * h :=
+by { rw infi_mul, exact le_cinfi H }
+
+lemma supr_mul_le {a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, g i * h ≤ a) : supr g * h ≤ a :=
+by { rw supr_mul, exact csupr_le H }
+
+lemma le_infi_mul_infi {a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, a ≤ g i * h j) :
+  a ≤ infi g * infi h :=
+le_infi_mul  $ λ i, le_mul_infi $ H i
+
+lemma supr_mul_supr_le {a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, g i * h j ≤ a) :
+  supr g * supr h ≤ a :=
+supr_mul_le $ λ i, mul_supr_le $ H _
+
+end csupr
+
 end nnreal
 
 namespace real

src/data/set/pointwise.lean

@@ -158,6 +158,9 @@ lemma inv_subset_inv : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t :=
 @[simp, to_additive] lemma inv_singleton (a : α) : ({a} : set α)⁻¹ = {a⁻¹} :=
 by rw [←image_inv, image_singleton]
 
+@[to_additive] lemma inv_range {ι : Sort*} {f : ι → α} : (range f)⁻¹ = range (λ i, (f i)⁻¹) :=
+by { rw ←image_inv, exact (range_comp _ _).symm }
+
 open mul_opposite
 
 @[to_additive]
@@ -850,6 +853,9 @@ ext $ λ x, ⟨λ hx, let ⟨p, q, ⟨i, hi⟩, ⟨j, hj⟩, hpq⟩ := set.mem_s
   ⟨(i, j), hpq ▸ hi ▸ hj ▸ rfl⟩,
 λ ⟨⟨i, j⟩, h⟩, set.mem_smul.2 ⟨b i, c j, ⟨i, rfl⟩, ⟨j, rfl⟩, h⟩⟩
 
+@[to_additive] lemma smul_set_range [has_scalar α β] {ι : Sort*} {f : ι → β} :
+  a • range f = range (λ i, a • f i) := (range_comp _ _).symm
+
 @[to_additive]
 instance smul_comm_class_set [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ] :
   smul_comm_class α (set β) (set γ) :=