Mathlib.Order.Filter.Ring

Filter.EventuallyLE.mul_le_mul theorem

 [MulZeroClass β] [Preorder β] [PosMulMono β] [MulPosMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂)
  (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁) (hf₀ : 0 ≤ᶠ[l] f₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Full source

theorem EventuallyLE.mul_le_mul [MulZeroClass β] [Preorder β] [PosMulMono β] [MulPosMono β]
    {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁)
    (hf₀ : 0 ≤ᶠ[l] f₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by
  filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul

Filtered Multiplication Preserves Inequality under Nonnegativity Conditions

Informal description

Let $\beta$ be a type with a multiplication operation and a zero element, forming a `MulZeroClass`, and equipped with a preorder. Assume $\beta$ satisfies the properties `PosMulMono` (positive multiplication is monotone) and `MulPosMono` (multiplication by a positive element is monotone). Let $l$ be a filter on a type $\alpha$, and let $f_1, f_2, g_1, g_2 : \alpha \to \beta$ be functions. If $f_1 \leq_{l} f_2$ and $g_1 \leq_{l} g_2$ eventually along $l$, and $g_1 \geq_{l} 0$ and $f_2 \geq_{l} 0$ eventually along $l$, then $f_1 \cdot g_1 \leq_{l} f_2 \cdot g_2$ eventually along $l$.

Filter.EventuallyLE.mul_le_mul' theorem

 [Mul β] [Preorder β] [MulLeftMono β] [MulRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂)
  (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Full source

@[to_additive EventuallyLE.add_le_add]
theorem EventuallyLE.mul_le_mul' [Mul β] [Preorder β] [MulLeftMono β]
    [MulRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β}
    (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by
  filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx

Eventual Monotonicity of Multiplication under Filter Comparison

Informal description

Let $\beta$ be a type with multiplication and a preorder, where multiplication is left and right monotone (i.e., $[MulLeftMono \beta]$ and $[MulRightMono \beta]$). Let $l$ be a filter on a type $\alpha$, and let $f_1, f_2, g_1, g_2 : \alpha \to \beta$ be functions. If $f_1 \leq_{l} f_2$ and $g_1 \leq_{l} g_2$ hold eventually along $l$, then $f_1 \cdot g_1 \leq_{l} f_2 \cdot g_2$ also holds eventually along $l$. Here, $f \leq_{l} g$ means that $f(x) \leq g(x)$ for all $x$ in some set belonging to the filter $l$.

Filter.EventuallyLE.mul_nonneg theorem

 [Semiring β] [PartialOrder β] [IsOrderedRing β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) :
  0 ≤ᶠ[l] f * g

Full source

theorem EventuallyLE.mul_nonneg [Semiring β] [PartialOrder β] [IsOrderedRing β]
    {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f)
    (hg : 0 ≤ᶠ[l] g) : 0 ≤ᶠ[l] f * g := by filter_upwards [hf, hg] with x using _root_.mul_nonneg

Product of Eventually Nonnegative Functions is Eventually Nonnegative

Informal description

Let $\beta$ be a semiring with a partial order and the structure of an ordered ring. For any filter $l$ on a type $\alpha$ and functions $f, g : \alpha \to \beta$, if $f$ is eventually nonnegative along $l$ and $g$ is eventually nonnegative along $l$, then the product $f \cdot g$ is also eventually nonnegative along $l$.

Filter.eventually_sub_nonneg theorem

[Ring β] [PartialOrder β] [IsOrderedRing β] {l : Filter α} {f g : α → β} : 0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g

Full source

theorem eventually_sub_nonneg [Ring β] [PartialOrder β] [IsOrderedRing β]
    {l : Filter α} {f g : α → β} :
    0 ≤ᶠ[l] g - f0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g :=
  eventually_congr <| Eventually.of_forall fun _ => sub_nonneg

Nonnegativity of Difference Equivalent to Inequality in Ordered Ring under Filter

Informal description

Let $β$ be a ring with a partial order and the structure of an ordered ring, and let $l$ be a filter on a type $α$. For any functions $f, g : α → β$, the inequality $0 ≤ᶠ[l] g - f$ holds if and only if $f ≤ᶠ[l] g$.

Filter.Germ.instIsOrderedRing instance

[Semiring β] [PartialOrder β] [IsOrderedRing β] : IsOrderedRing (Germ l β)

Full source

instance instIsOrderedRing [Semiring β] [PartialOrder β] [IsOrderedRing β] :
    IsOrderedRing (Germ l β) where
  zero_le_one := const_le zero_le_one
  mul_le_mul_of_nonneg_left x y z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono
    fun _a ↦ mul_le_mul_of_nonneg_left
  mul_le_mul_of_nonneg_right x y z := inductionOn₃ x y z fun _f _g _h hfg hh ↦ hh.mp <| hfg.mono
    fun _a ↦ mul_le_mul_of_nonneg_right

Ordered Ring Structure on Germs of Functions

Informal description

For any semiring $\beta$ with a partial order and an ordered ring structure, the germs of functions from $\alpha$ to $\beta$ at a filter $l$ also form an ordered ring.