Mathlib.Algebra.Order.GroupWithZero.Finset

Finset.sup_mul_le_mul_sup_of_nonneg theorem

 [SemilatticeSup M₀] [OrderBot M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) :
  s.sup (a * b) ≤ s.sup a * s.sup b

Full source

lemma sup_mul_le_mul_sup_of_nonneg [SemilatticeSup M₀] [OrderBot M₀] [PosMulMono M₀] [MulPosMono M₀]
    (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.sup (a * b) ≤ s.sup a * s.sup b :=
  Finset.sup_le fun _i hi ↦
    mul_le_mul (le_sup hi) (le_sup hi) (hb _ hi) ((ha _ hi).trans <| le_sup hi)

Supremum of Products is Bounded by Product of Suprema for Nonnegative Elements

Informal description

Let $M₀$ be a join-semilattice with a bottom element $\bot$, where left and right multiplication by nonnegative elements are monotone. For any finite set $s$ and functions $a, b : s \to M₀$ such that $a(i) \geq 0$ and $b(i) \geq 0$ for all $i \in s$, we have \[ \sup_{i \in s} (a(i) \cdot b(i)) \leq \left(\sup_{i \in s} a(i)\right) \cdot \left(\sup_{i \in s} b(i)\right). \]

Finset.mul_inf_le_inf_mul_of_nonneg theorem

 [SemilatticeInf M₀] [OrderTop M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) :
  s.inf a * s.inf b ≤ s.inf (a * b)

Full source

lemma mul_inf_le_inf_mul_of_nonneg [SemilatticeInf M₀] [OrderTop M₀] [PosMulMono M₀] [MulPosMono M₀]
    (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.inf a * s.inf b ≤ s.inf (a * b) :=
  Finset.le_inf fun i hi ↦ mul_le_mul (inf_le hi) (inf_le hi) (Finset.le_inf hb) (ha i hi)

Product of Infima is Bounded by Infimum of Products for Nonnegative Functions

Informal description

Let $M₀$ be a meet-semilattice with a top element $\top$, where left and right multiplication by nonnegative elements are monotone. For any finite set $s$ and nonnegative functions $a, b : s \to M₀$, the product of the infima of $a$ and $b$ is less than or equal to the infimum of the pointwise product $a \cdot b$, i.e., \[ \left(\inf_{i \in s} a_i\right) \cdot \left(\inf_{i \in s} b_i\right) \leq \inf_{i \in s} (a_i \cdot b_i). \]

Finset.sup'_mul_le_mul_sup'_of_nonneg theorem

 [SemilatticeSup M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (hs) :
  s.sup' hs (a * b) ≤ s.sup' hs a * s.sup' hs b

Full source

lemma sup'_mul_le_mul_sup'_of_nonneg [SemilatticeSup M₀] [PosMulMono M₀] [MulPosMono M₀]
    (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (hs) :
    s.sup' hs (a * b) ≤ s.sup' hs a * s.sup' hs b :=
  sup'_le _ _ fun _i hi ↦
    mul_le_mul (le_sup' _ hi) (le_sup' _ hi) (hb _ hi) ((ha _ hi).trans <| le_sup' _ hi)

Supremum of product is bounded by product of suprema for nonnegative functions

Informal description

Let $M₀$ be a join-semilattice with a zero element, where left and right multiplication by nonnegative elements are monotone. For a nonempty finite set $s$ and nonnegative functions $a, b : s \to M₀$ (i.e., $a(i) \geq 0$ and $b(i) \geq 0$ for all $i \in s$), the supremum of the pointwise product $a \cdot b$ over $s$ is less than or equal to the product of the suprema: $$\sup_{i \in s} (a(i) \cdot b(i)) \leq \left(\sup_{i \in s} a(i)\right) \cdot \left(\sup_{i \in s} b(i)\right).$$

Finset.inf'_mul_le_mul_inf'_of_nonneg theorem

 [SemilatticeInf M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (hs) :
  s.inf' hs a * s.inf' hs b ≤ s.inf' hs (a * b)

Full source

lemma inf'_mul_le_mul_inf'_of_nonneg [SemilatticeInf M₀] [PosMulMono M₀] [MulPosMono M₀]
    (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (hs) :
    s.inf' hs a * s.inf' hs b ≤ s.inf' hs (a * b) :=
  le_inf' _ _ fun _i hi ↦ mul_le_mul (inf'_le _ hi) (inf'_le _ hi) (le_inf' _ _ hb) (ha _ hi)

Product of Infima is Bounded by Infimum of Products for Nonnegative Functions

Informal description

Let $M₀$ be a meet-semilattice with a top element, and assume that left and right multiplication by nonnegative elements are monotone. For a nonempty finite set $s$ and nonnegative functions $a, b : s \to M₀$, the product of the infima of $a$ and $b$ over $s$ is less than or equal to the infimum of the pointwise product $a \cdot b$ over $s$. In symbols: \[ \left(\inf_{i \in s} a(i)\right) \cdot \left(\inf_{i \in s} b(i)\right) \leq \inf_{i \in s} (a(i) \cdot b(i)). \]

Finset.sup'_mul₀ theorem

 [MulPosReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) : s.sup' hs f * a = s.sup' hs fun i ↦ f i * a

Full source

lemma sup'_mul₀ [MulPosReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
    s.sup' hs f * a = s.sup' hs fun i ↦ f i * a := map_finset_sup' (OrderIso.mulRight₀ _ ha) hs f

Supremum Commutes with Right Multiplication by a Positive Element in a Group with Zero

Informal description

Let $G_0$ be a group with zero such that right multiplication by a positive element reflects the strict order relation. For any positive element $a \in G_0$ (i.e., $0 < a$), any function $f : \iota \to G_0$, and any nonempty finite set $s \subseteq \iota$, the supremum of $f$ over $s$ multiplied by $a$ is equal to the supremum over $s$ of the function $i \mapsto f(i) * a$. In other words, \[ \left(\sup_{i \in s} f(i)\right) * a = \sup_{i \in s} (f(i) * a). \]

Finset.mul₀_sup' theorem

 [PosMulReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) : a * s.sup' hs f = s.sup' hs fun i ↦ a * f i

Full source

lemma mul₀_sup' [PosMulReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
    a * s.sup' hs f = s.sup' hs fun i ↦ a * f i := map_finset_sup' (OrderIso.mulLeft₀ _ ha) hs f

Left Multiplication Commutes with Supremum in Ordered Group with Zero

Informal description

Let $G_0$ be a group with zero equipped with a partial order such that left multiplication by a positive element reflects the strict order (i.e., if $0 < a$ and $a \cdot x < a \cdot y$, then $x < y$). For any positive element $a \in G_0$ (i.e., $0 < a$), any function $f : \iota \to G_0$, and any nonempty finite set $s \subseteq \iota$, we have: \[ a \cdot \left( \sup_{i \in s} f(i) \right) = \sup_{i \in s} (a \cdot f(i)). \]

Finset.sup'_div₀ theorem

 [MulPosReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) : s.sup' hs f / a = s.sup' hs fun i ↦ f i / a

Full source

lemma sup'_div₀ [MulPosReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
    s.sup' hs f / a = s.sup' hs fun i ↦ f i / a :=
  map_finset_sup' (OrderIso.divRight₀ _ ha) hs f

Supremum of a Function Divided by a Positive Element in a Group with Zero

Informal description

Let $G_0$ be a group with zero equipped with a preorder such that right multiplication by a positive element reflects the strict order. For any positive element $a \in G_0$ (i.e., $0 < a$), any function $f : \iota \to G_0$, and any nonempty finite set $s \subseteq \iota$, the supremum of $f$ over $s$ divided by $a$ equals the supremum of the function $\lambda i, f(i) / a$ over $s$. That is: \[ \left(\sup_{i \in s} f(i)\right) / a = \sup_{i \in s} \left(f(i) / a\right). \]

Finset.sup_div₀ theorem

 [LinearOrderedCommGroupWithZero G₀] [OrderBot G₀] {a : G₀} (ha : 0 < a) (s : Finset ι) (f : ι → G₀) :
  s.sup f / a = s.sup fun i ↦ f i / a

Full source

lemma sup_div₀ [LinearOrderedCommGroupWithZero G₀] [OrderBot G₀] {a : G₀} (ha : 0 < a)
    (s : Finset ι) (f : ι → G₀) : s.sup f / a = s.sup fun i ↦ f i / a := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [← show (0 : G₀) = ⊥ from bot_unique zero_le']
  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]

Supremum Commutes with Division by Positive Element in Ordered Group with Zero

Informal description

Let $G_0$ be a linearly ordered commutative group with zero and a bottom element $\bot$. For any positive element $a \in G_0$ (i.e., $0 < a$), any function $f : \iota \to G_0$, and any finite set $s \subseteq \iota$, the supremum of $f$ over $s$ divided by $a$ equals the supremum of the function $\lambda i, f(i) / a$ over $s$. That is: \[ \left(\sup_{i \in s} f(i)\right) / a = \sup_{i \in s} \left(f(i) / a\right). \]