Antivary.of_inv_right₀
theorem Antivary.of_inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 g → Antivary f g⁻¹ → Monovary f g
This theorem, referred to as an alias of the forward direction of `antivary_inv_right₀`, states that for any types `ι`, `α`, and `β` wherein `α` and `β` are linear ordered semifields, and for any functions `f: ι → α` and `g: ι → β` satisfying the condition that for all `ι`, `g` is strictly greater than zero (i.e., `StrongLT 0 g`), if `f` antivaries with the inverse of `g` (i.e., `Antivary f g⁻¹`), then `f` monovaries with `g` (i.e., `Monovary f g`). In other words, if `f` decreases as `g⁻¹` increases, then `f` increases as `g` increases, provided `g` is always above zero.
More concisely: If `f: ι -> α` and `g: ι -> β` are functions on a type `ι` such that `α` and `β` are linear ordered semifields, `g` is strictly positive, and `f` antivaries with the inverse of `g`, then `f` monovaries with `g`.
|
Antivary.of_inv_right
theorem Antivary.of_inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f g⁻¹ → Monovary f g
This theorem, named "Antivary.of_inv_right", states that for any two functions `f` and `g` mapping from an arbitrary type `ι` to two types `α` and `β` respectively, where both `α` and `β` are ordered commutative groups, if the function `f` antivaries with the inverse of function `g`, then function `f` monovaries with function `g`. In other words, if for all indices `i` and `j`, when the value of `g⁻¹` at `j` is greater than `g⁻¹` at `i` implies the value of `f` at `i` is greater than or equal to `f` at `j`, then for all such `i` and `j`, a greater value of `g` at `j` compared to `g` at `i` implies a greater or equal value of `f` at `j` compared to `f` at `i`.
More concisely: If `f: ι → α` and `g: ι → β` are functions with `α` and `β` ordered commutative groups, and `g⁻¹` satisfies `g⁻¹ i < g⁻¹ j` implies `f i ≤ f j`, then `g j ≤ g i` implies `f j ≤ f i`.
|
AntivaryOn.inv_right
theorem AntivaryOn.inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f g s → MonovaryOn f g⁻¹ s
The theorem `AntivaryOn.inv_right` states that for any set `s` of an arbitrary type `ι`, and two functions `f` and `g` from `ι` to ordered commutative groups `α` and `β` respectively, if `f` antivaries with `g` on `s`, then `f` monovaries with the inverse of `g` on `s`. In other words, if for all elements `i` and `j` in `s`, a smaller value of `g` implies a larger or equal value of `f`, then a smaller value of `g⁻¹` (the inverse of `g`) implies a smaller or equal value of `f`.
More concisely: If function `f` antivaries with `g` on set `s`, then `f` monovaries with the inverse of `g` on `s`.
|
monovary_inv_right₀
theorem monovary_inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 g → (Monovary f g⁻¹ ↔ Antivary f g)
The theorem `monovary_inv_right₀` states that for any types `ι`, `α`, and `β`, and for any functions `f : ι → α` and `g : ι → β`, where `α` and `β` are both linear ordered semifields, if the function `g` is strongly greater than 0 (i.e., all its values are positive), then `f` monovaries with the inverse of `g` if and only if `f` antivaries with `g`. In other words, if `g` increases, then `f` follows the inverse of `g` in the sense that it decreases when `g` increases and vice versa, and this condition is equivalent to `f` being antivariant with `g`, meaning `f` decreases when `g` increases.
More concisely: For functions `f : ι -> α` and `g : ι -> β` between linear ordered semifields, `f` monovaries with the inverse of `g` if and only if `f` antivaries with `g`, given that `g` is strictly positive.
|
MonovaryOn.inv
theorem MonovaryOn.inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f g s → MonovaryOn f⁻¹ g⁻¹ s
This theorem is an alias for the reverse direction of `monovaryOn_inv`. It states that for any types `ι`, `α`, and `β` where `α` and `β` are ordered commutative groups—along with a set `s` of type `ι`, and functions `f` and `g` from `ι` to `α` and `β`, respectively—if `f` monovaries with `g` on `s` (i.e., whenever `g i < g j` for any `i, j` in `s`, we have `f i ≤ f j`), then the inverse of `f` monovaries with the inverse of `g` on `s`. In other words, if `g⁻¹ j < g⁻¹ i`, then `f⁻¹ j ≤ f⁻¹ i` for any `i, j` in `s`.
More concisely: If functions `f: ι → α` and `g: ι → β` are order-preserving on a set `s` with `g` being the inverse of `g'` and `f` the inverse of some function `h`, then `h` is order-preserving on `s` with respect to `g`.
|
Monovary.inv
theorem Monovary.inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f g → Monovary f⁻¹ g⁻¹
The theorem `Monovary.inv` states that for all types `ι`, `α`, and `β`, with `α` and `β` being ordered commutative groups, and for all functions `f` from `ι` to `α` and `g` from `ι` to `β`, if `f` monovaries with `g` (that is, for any `i` and `j` in `ι`, if `g(i)` is less than `g(j)` then `f(i)` is less or equal to `f(j)`), then the inverse of `f`, `f⁻¹`, monovaries with the inverse of `g`, `g⁻¹`. In other words, the monovary property is preserved under taking inverses of both the functions.
More concisely: If functions `f: ι -> α` and `g: ι -> β` are monovariant with each other, then their inverses `f⁻¹: α -> ι` and `g⁻¹: β -> ι` are monovariant with each other.
|
Antivary.inv_left
theorem Antivary.inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f g → Monovary f⁻¹ g
The theorem `Antivary.inv_left` states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, given functions `f` from `ι` to `α` and `g` from `ι` to `β`, if `f` antivaries with `g` (i.e., whenever `g i` is less than `g j`, `f j` is less than or equal to `f i`), then the inverse of `f` monovaries with `g` (i.e., whenever `g i` is less than `g j`, `f⁻¹ i` is less than or equal to `f⁻¹ j`). This theorem is essentially a restatement of the reverse direction of the theorem `monovary_inv_left`.
More concisely: If a function from a type to an ordered commutative group antivaries with another function from the same type to the same ordered commutative group, then the inverse of the first function monovaries with the second.
|
monovary_iff_smul_rearrangement
theorem monovary_iff_smul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β},
Monovary f g ↔ ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j
The theorem `monovary_iff_smul_rearrangement` states that for any two functions `f` and `g`, which map from an arbitrary type `ι` to a linearly ordered ring `α` and a linearly ordered additive commutative group `β` respectively, `f` monovaries with `g` if and only if for all pairs of elements `i` and `j` in `ι`, the inequality `f(i)*g(j) + f(j)*g(i) ≤ f(i)*g(i) + f(j)*g(j)` holds. This inequality is known as the rearrangement inequality. Here, the `•` operation represents scalar multiplication in the module structure of `β` over `α`. The monovariation property is defined as: if `g(i) < g(j)` then `f(i) ≤ f(j)`.
More concisely: The theorem `monovary_iff_rearrangement` in Lean 4 states that two functions `f` from a type `ι` to a linearly ordered ring `α` and `g` from `ι` to a linearly ordered additive commutative group `β` are related by the monovariation property if and only if for all `i, j` in `ι`, we have `f(i)*g(j) + f(j)*g(i) ≤ f(i)*g(i) + f(j)*g(j)`.
|
antivaryOn_iff_smul_rearrangement
theorem antivaryOn_iff_smul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι},
AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
This theorem states that for two functions `f` and `g` mapping from a set `s` of some type `ι`, `f` antivaries with `g` on `s` if and only if the rearrangement inequality holds for all `i, j` in `s`. The rearrangement inequality here is defined as `f i • g i + f j • g j ≤ f i • g j + f j • g i`, where `•` denotes scalar multiplication. This means that for any two elements `i` and `j` in the set `s`, swapping the inputs of functions `f` and `g` causes the result to be less than or equal to the original. The notion of antivariation used here is that if `g i` is less than `g j`, then `f j` is less than or equal to `f i`.
More concisely: For functions `f` and `g` mapping from a set `s`, `f` antivariates with `g` if and only if the rearrangement inequality holds for all `i, j` in `s`, i.e., `f i * g i + f j * g j <= f i * g j + f j * g i`.
|
AntivaryOn.sub_mul_sub_nonpos
theorem AntivaryOn.sub_mul_sub_nonpos :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} {s : Set ι},
AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0
The theorem `AntivaryOn.sub_mul_sub_nonpos` states that for any type `ι`, any linearly ordered ring `α`, any functions `f` and `g` from `ι` to `α`, and any set `s` of type `ι`, if `f` antivaries with `g` on `s`, then for all `i` and `j` in `s`, the product of the differences `(f j - f i)` and `(g j - g i)` is less than or equal to zero.
In other words, whenever `f` and `g` are two functions that antivary on a certain set (meaning that if `g` increases, `f` decreases), then the product of the differences in values of `f` and `g` for any two elements in the set is always non-positive.
More concisely: For any linearly ordered ring `α`, if functions `f` and `g` from a set `ι` to `α` antivary on `ι`, then for all `i, j` in `ι`, the product `(f j - f i) * (g j - g i)` is non-positive.
|
Antivary.inv_right
theorem Antivary.inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f g → Monovary f g⁻¹
The theorem `Antivary.inv_right` states that for all types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, for any two functions `f: ι → α` and `g: ι → β`, if `f` antivariates with `g` (meaning whenever `g i` is less than `g j`, `f j` is less than or equal to `f i`), then `f` monovariates with the inverse of `g` (`g⁻¹`). This implies that whenever `g⁻¹ i` is less than `g⁻¹ j`, `f i` is less than or equal to `f j`.
More concisely: If functions `f: ι → α` and `g: ι → β` are such that `g i <= g j` implies `f j <= f i` for all `i, j` in `ι`, where `α` and `β` are ordered commutative groups, then `g⁻¹ i <= g⁻¹ j` implies `f i <= f j`.
|
antivary_inv_right₀
theorem antivary_inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 g → (Antivary f g⁻¹ ↔ Monovary f g)
The theorem `antivary_inv_right₀` states that for any given types `ι`, `α`, and `β`, where `α` and `β` are both linear ordered semifields, and any given functions `f : ι → α` and `g : ι → β`, if the function `g` is strongly greater than the zero function (i.e., `g(i) > 0` for all `i`), then `f` antivaries with the inverse of `g` if and only if `f` monovaries with `g`. In other words, if all values of `g` are positive, then `f` decreases as the inverse of `g` increases if and only if `f` increases as `g` increases.
More concisely: For functions \(f : ι \to α\) and \(g : ι \to β\) over linearly ordered semifields \(α\) and \(β\), if \(g(i) > 0\) for all \(i\), then \(f\) antivaries with the inverse of \(g\) if and only if \(f\) monovaries with \(g\).
|
AntivaryOn.sub_smul_sub_nonpos
theorem AntivaryOn.sub_smul_sub_nonpos :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι},
AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
The theorem `AntivaryOn.sub_smul_sub_nonpos` states that for any set `s` of elements of some type `ι`, and any two functions `f: ι → α` and `g: ι → β`, where `α` is a type with an ordered ring structure and `β` is a type with an ordered additive commutative group structure and a module structure over `α`, if `f` antivaries with `g` on the set `s` (i.e., `g(i) < g(j)` implies `f(j) ≤ f(i)` for all `i` and `j` in `s`), then for all `i` and `j` in `s`, the product of `f(j) - f(i)` and `g(j) - g(i)` is less than or equal to zero.
More concisely: For functions `f: ι -> α` on a set `s` with values in an ordered ring `α`, and functions `g: ι -> β` on `s` with values in an ordered additive commutative group `β` with a module structure over `α`, if `g` antitonically maps `s` and `f(j) ≤ f(i)` whenever `g(j) < g(i)`, then `f(j) - f(i) * (g(j) - g(i)) <= 0` for all `i, j` in `s`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.1
theorem Mathlib.Algebra.Order.Monovary._auxLemma.1 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f⁻¹ g s = AntivaryOn f g s
The theorem states that for any set `s` of elements of type `ι`, and any two functions `f : ι → α` and `g : ι → β`, where `α` and `β` are types over which an ordered commutative group structure is defined, the function `f` inversely monovaries with `g` on `s` if and only if `f` antivaries with `g` on `s`. In other words, if for every pair of elements `i, j` in `s` such that `g(i) < g(j)`, we have `f(j) ≤ f(i)`, then for the same pair `i, j`, we have `(f⁻¹)(i) ≤ (f⁻¹)(j)`. Here, `f⁻¹` refers to the inverse function of `f` in the group structure.
More concisely: For functions `f : ι → α` and `g : ι → β` defined on a set `s` with `α` and `β` having ordered commutative group structures, `f` inversely monovaries with `g` on `s` if and only if `f` antivaries with `g` on `s`, that is, for all `i, j` in `s` with `g(i) < g(j)`, we have `(f⁻¹)(i) ≤ (f⁻¹)(j)` if and only if `f(j) ≤ f(i)`.
|
Antivary.inv_left₀
theorem Antivary.inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → Antivary f g → Monovary f⁻¹ g
The theorem `Antivary.inv_left₀` states that for any types `ι`, `α`, and `β`, where `α` and `β` are linearly ordered semifields, and any functions `f : ι → α` and `g : ι → β`, if `f` is strictly greater than zero for all `i` (i.e., `f` is strongly greater than the zero function) and `f` antivaries with `g` (i.e., whenever `g i < g j`, we have `f j ≤ f i`), then the reciprocal of `f` monovaries with `g` (i.e., whenever `g i < g j`, we have `(f⁻¹) i ≤ (f⁻¹) j`). In other words, if `f` is positive and decreases when `g` increases, then the reciprocal of `f` increases when `g` increases.
More concisely: If `f : ι → α` is a strictly positive function that antivaries with another function `g : ι → β` (i.e., `f j ≤ f i` whenever `g i < g j`), then the reciprocal function `f⁻¹ : α → ι` monovaries with `g` (i.e., `(f⁻¹) i ≤ (f⁻¹) j` whenever `g i < g j`).
|
Antivary.smul_add_smul_le_smul_add_smul
theorem Antivary.smul_add_smul_le_smul_add_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β},
Antivary f g → ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
This theorem, known as an **Alias** of the forward direction of `antivary_iff_smul_rearrangement`, states that for any two functions `f` and `g`, if `f` is antivariant with `g`, then for any two indices `i` and `j`, the inequality `f(i) * g(i) + f(j) * g(j) ≤ f(i) * g(j) + f(j) * g(i)` holds. Here, `f` and `g` are functions from the index set `ι` to a linearly ordered ring `α` and a linearly ordered additive commutative group `β` respectively, and `•` denotes scalar multiplication in the module structure of `β` over `α`. Antivariance between `f` and `g` means that whenever `g(i) < g(j)`, we have `f(j) ≤ f(i)`.
More concisely: If functions $f:\ι \to \alpha$ and $g:\ι \to \beta$ are such that $g(i) < g(j) \implies f(j) \leq f(i)$, then for all $i,j \in \ι$, we have $f(i) \cdot g(i) + f(j) \cdot g(j) \leq f(i) \cdot g(j) + f(j) \cdot g(i)$.
|
antivaryOn_iff_mul_rearrangement
theorem antivaryOn_iff_mul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} {s : Set ι},
AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i
This theorem states that for any set `s` of a generic type `ι` and any two functions `f` and `g` mapping `ι` to a linearly ordered ring `α`, the condition that `f` antivaries with `g` on `s` is equivalent to the following inequality holding for all `i, j` in `s`: the sum of `f(i)` times `g(i)` and `f(j)` times `g(j)` is less than or equal to the sum of `f(i)` times `g(j)` and `f(j)` times `g(i)`.
This inequality is often referred to as the rearrangement inequality. The condition of `f` antivarying with `g` on `s` means that if `g(i)` is less than `g(j)`, then `f(j)` is less than or equal to `f(i)` for all `i, j` in `s`.
More concisely: For any set `s` of a linearly ordered index type `ι`, functions `f` and `g` mapping `ι` to a linearly ordered ring `α`, the functions `f` and `g` antivary on `s` if and only if for all `i, j` in `s`, the sum `f(i) * g(i) + f(j) * g(j)` is less than or equal to the sum `f(i) * g(j) + f(j) * g(i)`.
|
AntivaryOn.of_inv₀
theorem AntivaryOn.of_inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β},
(∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → AntivaryOn f⁻¹ g⁻¹ s → AntivaryOn f g s
This theorem, which can be referred to as an alias of the forward direction of `antivaryOn_inv₀`, states that for any types `ι`, `α`, `β` where `α` and `β` are linear ordered semifields, given a set `s` of type `ι` and two functions `f: ι → α` and `g: ι → β`, if for all elements `i` in `s`, `f(i)` and `g(i)` are greater than 0, and `f⁻¹` antivaries with `g⁻¹` on `s` (i.e., whenever `g⁻¹(i) < g⁻¹(j)` for any `i, j` in `s`, it implies `f⁻¹(j) ≤ f⁻¹(i)`), then `f` antivaries with `g` on `s` (i.e., whenever `g(i) < g(j)` for any `i, j` in `s`, it implies `f(j) ≤ f(i)`).
More concisely: If `f: ι -> α` and `g: ι -> β` are functions from a set `s` of linear ordered semifields `ι`, `α`, and `β`, where `f(i)`, `g(i)` are positive for all `i` in `s`, and `f⁻¹` antivariance with `g⁻¹` holds on `s`, then `f` antivaries with `g` on `s`. That is, `g(i) < g(j)` implies `f(j) <= f(i)` for all `i, j` in `s`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.7
theorem Mathlib.Algebra.Order.Monovary._auxLemma.7 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f g⁻¹ s = MonovaryOn f g s
The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.7` states that for all types `ι`, `α`, and `β`, where `α` and `β` form ordered commutative groups, and for any set `s` of type `ι`, and functions `f : ι → α` and `g : ι → β`, the statement that `f` antivaries with the inverse of `g` on `s` is equivalent to the statement that `f` monovaries with `g` on `s`. In other words, `f` and `g⁻¹` varying in opposite directions on `s` is equivalent to `f` and `g` varying in the same direction on `s`.
More concisely: The theorem states that for functions `f : ι → α` and `g : ι → β` defining ordered commutative groups `α` and `β`, the condition that `f` antivaries with the inverse of `g` on a set `s` is equivalent to `f` monovaries with `g` on `s`.
|
Monovary.inv₀
theorem Monovary.inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → StrongLT 0 g → Monovary f g → Monovary f⁻¹ g⁻¹
The theorem `Monovary.inv₀` states that for any types `ι`, `α`, and `β`, with `α` and `β` being linear ordered semifields, and for any functions `f : ι → α` and `g : ι → β`, if `0` is strictly less than each value of `f` and `g` (in other words, `f` and `g` are strongly greater than zero), and if `f` monovaries with `g` (meaning whenever `g i` is less than `g j`, then `f i` is less than or equal to `f j`), then the inverses of `f` and `g` also have the property that `f` monovaries with `g`. In other words, whenever `(g⁻¹) i` is less than `(g⁻¹) j`, then `(f⁻¹) i` is less than or equal to `(f⁻¹) j`.
More concisely: If functions `f : ι → α` and `g : ι → β` are strictly positive linear order preserving maps between linearly ordered semifields `α` and `β`, then their inverses also preserve the linear order.
|
antivary_inv_left₀
theorem antivary_inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → (Antivary f⁻¹ g ↔ Monovary f g)
The theorem `antivary_inv_left₀` states that for all types `ι`, `α`, and `β` where `α` and `β` are linear ordered semifields, and for all functions `f : ι → α` and `g : ι → β`, if function `f` is strongly greater than 0 (meaning for all `i` in `ι`, `f(i)` is greater than 0), then the function `f⁻¹` (the reciprocal function of `f`) antivaries with `g` if and only if `f` monovaries with `g`. In other words, if `g i < g j` implies `f⁻¹ j ≤ f⁻¹ i`, then and only then `g i < g j` implies `f i ≤ f j`.
More concisely: For functions \(f : ι \to \alpha\) and \(g : ι \to \beta\) over linear ordered semifield types \(\alpha\) and \(\beta\), if \(f\) is strictly positive and \(f⁻¹\) antivaries with \(g\), then \(f\) monovaries with \(g\), and conversely.
|
monovary_inv_left₀
theorem monovary_inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → (Monovary f⁻¹ g ↔ Antivary f g)
The theorem `monovary_inv_left₀` states that for any types `ι`, `α`, and `β`, where `α` and `β` are linear ordered semifields, and any functions `f` from `ι` to `α` and `g` from `ι` to `β`, if `f` is strongly greater than 0 (i.e., for all `i` in `ι`, `0 < f(i)`), then `f⁻¹` monovaries with `g` if and only if `f` antivaries with `g`. Here, `f⁻¹` monovaries with `g` means that whenever `g(i) < g(j)`, we have `f⁻¹(i) ≤ f⁻¹(j)`, and `f` antivaries with `g` means that whenever `g(i) < g(j)`, we have `f(j) ≤ f(i)`.
More concisely: For functions \(f: ι \to \alpha\) and \(g: ι \to \beta\), where \(\alpha\) and \(\beta\) are linear ordered semifields, \(f\) is strictly positive, and \(f\) monovaries with \(g\) if and only if \(f\) antivaries with \(g\).
|
monovary_iff_mul_rearrangement
theorem monovary_iff_mul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α},
Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j
The theorem `monovary_iff_mul_rearrangement` states that for any two functions, `f` and `g`, defined on a common domain of type `ι`, and with a range in a linearly ordered ring `α`, the functions `f` and `g` monovary (i.e., if `g(i) < g(j)`, then `f(i) ≤ f(j)`) if and only if the rearrangement inequality holds for all values of `i` and `j` in the domain. The rearrangement inequality in this context is represented by the inequality `f(i) * g(j) + f(j) * g(i) ≤ f(i) * g(i) + f(j) * g(j)`. In essence, it connects the concept of monovariation, which captures a form of order-preserving behavior between two functions, with a specific inequality involving the products of function values.
More concisely: For functions `f` and `g` on a linearly ordered domain `ι` with ranges in a linearly ordered ring `α`, `f` monovaryes with respect to `g` if and only if the product inequality `f(i) * g(j) + f(j) * g(i) ≤ f(i) * g(i) + f(j) * g(j)` holds for all `i ≠ j` in `ι`.
|
MonovaryOn.inv₀
theorem MonovaryOn.inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β},
(∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → MonovaryOn f g s → MonovaryOn f⁻¹ g⁻¹ s
This theorem, named "MonovaryOn.inv₀", states that for any two functions `f` and `g` on a set `s` under the conditions that all elements of the set `s` map to positive values under both `f` and `g`, if `f` monovaries with `g` on `s`, then the inverses of `f` and `g` also monovary on `s`. Here, a function `f` monovaries with a function `g` on a set `s` if for all `i, j` in `s`, when `g(i)` is less than `g(j)`, `f(i)` is less than or equal to `f(j)`. The types `ι`, `α`, and `β` are any types where `α` and `β` are linear ordered semifields. A linear ordered semifield is a field that is also a linear order, meaning it is commutative, has an identity, and is associative, and also has a total order compatible with the field operations. The theorem applies to the inverses of `f` and `g` as long as `f` and `g` are entirely positive on `s`.
More concisely: If functions `f` and `g` on a set `s` of elements with positive images under both functions satisfy `f` monovaries with `g`, then the inverses of `f` and `g` monovary on `s`.
|
AntivaryOn.smul_add_smul_le_smul_add_smul
theorem AntivaryOn.smul_add_smul_le_smul_add_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι},
AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
This theorem, an alias of the forward direction of `antivaryOn_iff_smul_rearrangement`, states that for any two functions `f` and `g` mapping elements of type `ι` to `α` and `β` respectively, and a set `s` of elements of type `ι`, if `f` and `g` antivary on `s` (which means that if `g i` is less than `g j` then `f j` is less than or equal to `f i` for all `i` and `j` in `s`), then for any `i` and `j` in `s`, the inequality `f i * g i + f j * g j ≤ f i * g j + f j * g i` holds. Here, `α` is a linear-ordered ring, `β` is a linear-ordered additive commutative group, and `β` is a module over `α` with an ordered scalar multiplication.
More concisely: For functions `f: ι -> α` and `g: ι -> β` mapping elements of type `ι` to a linear-ordered ring `α` and a linear-ordered additive commutative group `β` that is a module over `α` with an ordered scalar multiplication, if `f` and `g` antivary on a set `s` of elements of type `ι`, then for all `i, j` in `s`, we have `f i * g i + f j * g j ≤ f i * g j + f j * g i`.
|
AntivaryOn.inv_left₀
theorem AntivaryOn.inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < f i) → AntivaryOn f g s → MonovaryOn f⁻¹ g s
The theorem `AntivaryOn.inv_left₀` states that for any type `ι`, and any two types `α` and `β` that are linearly ordered semifields, and given a set `s` of elements of type `ι`, and two functions `f : ι → α` and `g : ι → β`, if every element `i` in `s` maps to a positive value under `f`, and if `f` antivaries with `g` on `s` (that is, if for all `i` and `j` in `s`, `g(i) < g(j)` implies `f(j) ≤ f(i)`), then the inverse function of `f`, denoted `f⁻¹`, monovaries with `g` on `s` (that is, if for all `i` and `j` in `s`, `g(i) < g(j)` implies `f⁻¹(i) ≤ f⁻¹(j)`).
More concisely: If `f : ι → α` and `g : ι → β` are functions on a linearly ordered semifield `ι`, `s` is a set of elements in `ι` such that every element in `s` maps to a positive value under `f` and `f` antivaries with `g` on `s`, then `f⁻¹` monovaries with `g` on `s`.
|
AntivaryOn.inv_right₀
theorem AntivaryOn.inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < g i) → AntivaryOn f g s → MonovaryOn f g⁻¹ s
The theorem `AntivaryOn.inv_right₀` states that for any set `s` of elements of a certain type `ι`, and any two functions `f : ι → α` and `g : ι → β` where `α` and `β` are linear ordered semifields, if every element `i` in `s` satisfies that `0 < g i`, and if `f` antivaries with `g` on `s` (meaning that if `g i < g j` then `f j ≤ f i` for all `i, j ∈ s`), then `f` monovaries with the inverse of `g` on `s` (meaning that if `(g⁻¹) i < (g⁻¹) j` then `f i ≤ f j` for all `i, j ∈ s`).
More concisely: If functions `f` and `g` map a linearly ordered set `s` with `0 < g i` for all `i ∈ s`, and `f` antivaries with `g`, then `f` monovaries with the inverse of `g`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.13
theorem Mathlib.Algebra.Order.Monovary._auxLemma.13 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f g⁻¹ = Antivary f g
The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.13` states that for all types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, and functions `f : ι → α` and `g : ι → β`, the function `f` monovaries with the inverse of `g` if and only if `f` antivaries with `g`. In other words, if for all indices `i` and `j`, `g(i) < g(j)` implies `f(i) ≤ f(j)`, then `g(i) > g(j)` implies `f(j) ≤ f(i)`, and vice versa.
More concisely: The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.13` in Lean 4 states that for ordered commutative groups `α` and `β`, functions `f : ι → α` and `g : ι → β` are monovariant and antivariant with each other if and only if for all indices `i` and `j`, `g(i) < g(j)` if and only if `f(i) ≤ f(j)` and `g(i) > g(j)` if and only if `f(j) ≤ f(i)`.
|
monovaryOn_iff_mul_rearrangement
theorem monovaryOn_iff_mul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} {s : Set ι},
MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j
The theorem `monovaryOn_iff_mul_rearrangement` states that for any type `ι`, any linear ordered ring `α`, any two functions `f` and `g` from `ι` to `α`, and any set `s` of `ι`, the conditions of monovariation for `f` and `g` over `s` are equivalent to the hold of the rearrangement inequality. The rearrangement inequality here means that for every `i` and `j` in `s`, the value of `f(i) * g(j) + f(j) * g(i)` is always less than or equal to `f(i) * g(i) + f(j) * g(j)`. The concept of monovariation is that if `g(i)` is less than `g(j)`, then `f(i)` should be less than or equal to `f(j)`.
More concisely: The theorem `monovariationOn_iff_mul_rearrangement` in Lean 4 states that for any linear ordered ring `α`, functions `f` and `g` from a type `ι` to `α`, and set `s` of `ι`, the functions `f` and `g` are monovariant over `s` if and only if for all `i, j` in `s`, `f(i) * g(j) + f(j) * g(i) ≤ f(i) * g(i) + f(j) * g(j)`.
|
AntivaryOn.of_inv
theorem AntivaryOn.of_inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f⁻¹ g⁻¹ s → AntivaryOn f g s
The theorem `AntivaryOn.of_inv` states that for any type ι and types α and β which are ordered commutative groups, given a set `s` of type ι and functions `f` from ι to α and `g` from ι to β, if the inverse functions `f⁻¹` and `g⁻¹` antivary on the set `s` (meaning, if `g⁻¹(i) < g⁻¹(j)` implies `f⁻¹(j) ≤ f⁻¹(i)` for all `i, j` in the set `s`), then the functions `f` and `g` also antivary on the set `s` (that is, `g(i) < g(j)` implies `f(j) ≤ f(i)` for all `i, j` in the set `s`).
More concisely: If the inverse functions of two functions between commutative groups antivary on a set, then the original functions also antivary on that set.
|
Antivary.inv₀
theorem Antivary.inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → StrongLT 0 g → Antivary f g → Antivary f⁻¹ g⁻¹
The theorem `Antivary.inv₀` states that for any types `ι`, `α`, and `β`, if `α` and `β` are linear ordered semifields, and `f` and `g` are functions from `ι` to `α` and `β` respectively, then if `f` and `g` are strongly greater than zero (i.e., each value they produce is greater than zero), and if `f` antivaries with `g` (meaning whenever `g` increases, `f` decreases or stays the same), then the inverse functions of `f` and `g`, `f⁻¹` and `g⁻¹`, also antivary with each other. In other words, the property of antivarying is preserved under inversion for functions that are strongly greater than zero.
More concisely: If `f` and `g` are strongly positive, linearly ordered semifield functions with `f` antivarying with `g`, then their inverse functions `f⁻¹` and `g⁻¹` antivary with each other.
|
Monovary.of_inv_right
theorem Monovary.of_inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f g⁻¹ → Antivary f g
The theorem `Monovary.of_inv_right` states that for all types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, and for all functions `f : ι → α` and `g : ι → β`, if `f` monovaries with the inverse of `g` (i.e., if whenever `g⁻¹(i) < g⁻¹(j)` then `f(i) ≤ f(j)`), then `f` antivaries with `g` (i.e., if `g(i) < g(j)`, then `f(j) ≤ f(i)`). In other words, the relationship between `f` and `g⁻¹` being monovariant implies that the relationship between `f` and `g` is antivariant.
More concisely: If a function `f : ι → α` monovaries with the inverse of another function `g : ι → β` (i.e., `g⁻¹(i) < g⁻¹(j)` implies `f(i) ≤ f(j)`), then `f` antivaries with `g` (i.e., `g(i) < g(j)` implies `f(j) ≤ f(i)`).
|
Mathlib.Algebra.Order.Monovary._auxLemma.9
theorem Mathlib.Algebra.Order.Monovary._auxLemma.9 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f⁻¹ g = Antivary f g
The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.9` states that for all types `ι`, `α`, and `β`, if `α` and `β` are ordered commutative groups, and if `f` is a function from `ι` to `α` and `g` is a function from `ι` to `β`, then `f` is said to monovary inversely with `g` if and only if `f` antivaries with `g`. In mathematical terms, this means that for all elements `i` and `j` in `ι`, if `g(i) < g(j)` then `1/f(i) ≤ 1/f(j)` if and only if `f(j) ≤ f(i)`.
More concisely: For functions $f:\ι\to\alpha$ and $g:\ι\to\β$ between ordered commutative groups $\alpha$ and $\beta$, $f$ monovaries inversely with $g$ if and only if $f$ antivaries with $g$, i.e., for all $i,j\in\ι$, $g(i)
|
MonovaryOn.of_inv_right₀
theorem MonovaryOn.of_inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < g i) → MonovaryOn f g⁻¹ s → AntivaryOn f g s
The theorem `MonovaryOn.of_inv_right₀` states that for any types `ι`, `α`, and `β` with `α` and `β` being linearly ordered semifields, any set `s` of type `ι`, and any two functions `f` and `g` with types `ι → α` and `ι → β` respectively, if every element `i` in set `s` satisfies `0 < g i`, and if function `f` monovaries with the reciprocal of function `g` on set `s`, then function `f` antivaries with function `g` on set `s`. In other words, if `g i < g j` implies `f i ≤ f j` for `g` being the reciprocal, then `g i < g j` implies `f j ≤ f i` for the original function `g`.
More concisely: If `α` and `β` are linearly ordered semifields, `s` is a set, `0 < g i for all i in s`, and `f` monovaries with the reciprocal of `g` on `s`, then `f` antivaries with `g` on `s`.
|
Monovary.of_inv_right₀
theorem Monovary.of_inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 g → Monovary f g⁻¹ → Antivary f g
The theorem `Monovary.of_inv_right₀` states that for all types `ι`, `α` and `β`, where `α` and `β` are linear ordered semifields, and for all functions `f` from `ι` to `α` and `g` from `ι` to `β`, if `g` is strongly greater than `0` (that is, for all `i` in the domain `ι`, `g(i)` is greater than `0`) and `f` monovaries with the inverse of `g` (that is, for any `i` and `j` in the domain `ι`, if `g(i)` is less than `g(j)`, then `f(i)` is less than or equal to `f(j)`), then `f` antivaries with `g` (that is, for any `i` and `j` in the domain `ι`, if `g(i)` is less than `g(j)`, then `f(j)` is less than or equal to `f(i)`).
More concisely: If `f: ι → α` monovaries with the inverse of the strongly positive function `g: ι → β`, then `f` antivaries with `g`.
|
MonovaryOn.of_inv_right
theorem MonovaryOn.of_inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f g⁻¹ s → AntivaryOn f g s
This theorem, referred to as an **Alias** of the forward direction of `monovaryOn_inv_right`, states that for any set `s` of a certain type `ι` and any two functions `f : ι → α` and `g : ι → β`, where `α` and `β` are types with ordered commutative group structures, if `f` monovaries with the inverse of `g` on `s` (that is, whenever `g⁻¹(i) < g⁻¹(j)` for any `i, j ∈ s`, we have `f(i) ≤ f(j)`), then `f` antivaries with `g` on `s` (that is, whenever `g(i) < g(j)` for any `i, j ∈ s`, we have `f(j) ≤ f(i)`).
More concisely: If a function `f` monovaries with the inverse of another function `g` on a set `s`, then `f` antivaries with `g` on `s`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.11
theorem Mathlib.Algebra.Order.Monovary._auxLemma.11 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f⁻¹ g = Monovary f g
This theorem states that for any types `ι`, `α`, and `β`, with `α` and `β` being ordered commutative groups, and for any functions `f : ι → α` and `g : ι → β`, the property of `f⁻¹` (the inverse function of `f`) antivarying with `g` is equivalent to `f` monovarying with `g`. In other words, if for all `i`, `j` in `ι`, `g(i) < g(j)` implies that `f⁻¹(j) ≤ f⁻¹(i)`, then it is also true that `g(i) < g(j)` implies that `f(i) ≤ f(j)`, and vice versa. This captures a fundamental symmetry between the antivariation and monovariation of functions in the context of ordered commutative groups.
More concisely: For functions `f : ι -> α` and `g : ι -> β` between ordered commutative groups `α` and `β`, `f⁻¹` antivaries with `g` if and only if `f` monovaries with `g`.
|
MonovaryOn.mul_add_mul_le_mul_add_mul
theorem MonovaryOn.mul_add_mul_le_mul_add_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} {s : Set ι},
MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j
The theorem `MonovaryOn.mul_add_mul_le_mul_add_mul` can be described as follows:
Given a type `ι`, a linear ordered ring `α`, two functions `f` and `g` from `ι` to `α`, and a set `s` of type `ι`, if the functions `f` and `g` monovary on the set `s` (that is, whenever `g i < g j` for `i, j ∈ s`, it follows that `f i ≤ f j`), then for any two elements `i` and `j` in the set `s`, the inequality `f i * g j + f j * g i ≤ f i * g i + f j * g j` holds. That is, the sum of the products of the values of `f` and `g` at `i` and `j`, when arranged such that the larger values of `g` correspond to the larger values of `f`, is less than or equal to the sum of the products of `f` and `g` at the same points when the values are arranged in matching order. This theorem is an alias for the forward direction of the theorem `monovaryOn_iff_mul_rearrangement`, which states this relationship in a different form.
More concisely: If functions `f` and `g` monovary on a set `s` in a linear ordered ring `α`, then for all `i, j` in `s`, we have `f i * g j + f j * g i ≤ f i * g i + f j * g j`.
|
Monovary.mul_add_mul_le_mul_add_mul
theorem Monovary.mul_add_mul_le_mul_add_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α},
Monovary f g → ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j
This theorem, which can also be referred to as an **Alias** of the forward direction of `monovary_iff_mul_rearrangement`, states that for any type `ι` and a `LinearOrderedRing` `α`, given two functions `f` and `g` from `ι` to `α` which monovary (meaning if `g i` is less than `g j` then `f i` is less than or equal to `f j`), for any `i` and `j` in `ι`, the inequality `f i * g j + f j * g i` is less than or equal to `f i * g i + f j * g j` will always hold.
In LaTeX mathematics, the theorem can be written as: If $f$ and $g$ are functions such that $g(i) < g(j)$ implies $f(i) \leq f(j)$, then for any $i, j$, the inequality $f(i)g(j) + f(j)g(i) \leq f(i)g(i) + f(j)g(j)$ is always satisfied.
More concisely: If two functions satisfy the monotonicity property that `g(i) < g(j)` implies `f(i) <= f(j)`, then their pointwise product satisfies the inequality `f * g <= g * f pointwise`.
|
Antivary.inv_right₀
theorem Antivary.inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 g → Antivary f g → Monovary f g⁻¹
This theorem, which is an alias of the reverse direction of `monovary_inv_right₀`, states that for any types `ι`, `α`, and `β` where `α` and `β` are linear ordered semifields, and any functions `f : ι → α` and `g : ι → β`, if the function `g` is strictly greater than zero for all inputs (i.e., `StrongLT 0 g`) and `f` antivaries with `g` (that is, whenever `g i < g j`, we have `f j ≤ f i`), then `f` monovaries with the inverse of `g` (that is, whenever `g⁻¹ i < g⁻¹ j`, we have `f i ≤ f j`). This essentially means that if `f` decreases when `g` increases and `g` is always positive, then `f` increases when `g` decreases (considering `g⁻¹` as the decreasing version of `g`).
More concisely: If `f : ι -> α` and `g : ι -> β` are functions on a type `ι` with `α` and `β` being linear ordered semifields, and `g` is strictly positive and `f` antivaries with `g`, then `f` monovaries with the inverse of `g`.
|
Monovary.of_inv_left
theorem Monovary.of_inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f⁻¹ g → Antivary f g
The theorem `Monovary.of_inv_left` states that for any types `ι`, `α`, and `β` with `α` and `β` being ordered commutative groups, and any two functions `f : ι → α` and `g : ι → β`, if the inverse of `f` monovaries with `g` (that is, whenever `g i < g j`, we have `(f i)⁻¹ ≤ (f j)⁻¹`), then `f` antivaries with `g` (that is, whenever `g i < g j`, we have `f j ≤ f i`).
More concisely: If the inverse of a function between commutative groups varies with another function, then the function itself antivaries with that function.
|
MonovaryOn.of_inv_left
theorem MonovaryOn.of_inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f⁻¹ g s → AntivaryOn f g s
This theorem, referred to as the alias of the forward direction of `monovaryOn_inv_left`, states that for any types `ι`, `α` and `β` where `α` and `β` are ordered commutative groups, and for any set `s` of type `ι`, if a function `f` monovaries with `g` on `s` when `f` is inverted, then `f` antivaries with `g` on `s`. In other words, if for all indices `i` and `j` in `s` such that `g(i) < g(j)` implies `f(i)⁻¹ ≤ f(j)⁻¹`, then it also implies `f(j) ≤ f(i)`.
More concisely: If a function `f` monovaries with `g` on a set `s` with respect to inverses in commutative groups `α` and `β`, then `f` antivaries with `g` on `s`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.16
theorem Mathlib.Algebra.Order.Monovary._auxLemma.16 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{f : ι → α} {g : ι → β}, Antivary f (-g) = Monovary f g
The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.16` states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered additive commutative groups, and any two functions `f : ι → α` and `g : ι → β`, the function `f` antivaries with `(-g)` if and only if it monovaries with `g`. In other words, if for all `i` and `j` such that `(-g(i)) < (-g(j))` implies `f(j) ≤ f(i)`, then it is equivalent to saying that for all `i` and `j` such that `g(i) < g(j)` it implies `f(i) ≤ f(j)`.
More concisely: For functions between ordered additive commutative groups `f : ι → α` and `g : ι → β`, `f` antivaries with `-g` if and only if it monovaries with `g`. In other words, the order `-g(i) < -g(j)` implies `f(i) ≤ f(j)` if and only if the order `g(i) < g(j)` implies `f(i) ≤ f(j)`.
|
Monovary.of_inv_left₀
theorem Monovary.of_inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → Monovary f⁻¹ g → Antivary f g
The theorem `Monovary.of_inv_left₀` states that for all ι indexing types, and all α and β of types `LinearOrderedSemifield`, if a function `f` is strongly greater than 0 (that is, for all index `i`, `f(i)` is greater than 0) and `f⁻¹` (the inverse of `f`) monovaries with `g` (meaning, whenever `g(i)` is less than `g(j)`, `f⁻¹(i)` is less than or equal to `f⁻¹(j)`), then `f` antivaries with `g` (meaning, whenever `g(i)` is less than `g(j)`, `f(j)` is less than or equal to `f(i)`). This theorem is an alias of the forward direction of another theorem `monovary_inv_left₀`.
More concisely: If a function `f` is strictly positive and its inverse monotonically increases with another function `g`, then `f` antimonotonically decreases with `g`.
|
MonovaryOn.of_inv_left₀
theorem MonovaryOn.of_inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < f i) → MonovaryOn f⁻¹ g s → AntivaryOn f g s
The theorem `MonovaryOn.of_inv_left₀` states that for any set `s` of some type `ι` and functions `f : ι → α` and `g : ι → β`, where `α` and `β` are types with a linear ordered semifield structure, if every element `i` in the set `s` has the property that `f i` is greater than zero, and if the function `f⁻¹` (the inverse of `f`) "monovaries" with `g` on `s` (meaning that whenever `g i` is less than `g j` for elements `i` and `j` in `s`, then `f⁻¹ i` is less than or equal to `f⁻¹ j`), then `f` "antivaries" with `g` on `s` (meaning that whenever `g i` is less than `g j` for elements `i` and `j` in `s`, then `f j` is less than or equal to `f i`). In simpler terms, the theorem relates the property of "monovarying" with the inverse of a function to "antivarying" with the original function under certain conditions.
More concisely: If `f : ι → α` and `g : ι → β` are functions with values in linearly ordered semifields, and `s ⊆ ι` has the property that `f i > 0` for all `i ∈ s` and `f⁻¹` monovaries with `g` on `s`, then `f` antivaries with `g` on `s`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.3
theorem Mathlib.Algebra.Order.Monovary._auxLemma.3 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f⁻¹ g s = MonovaryOn f g s
This theorem states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, and any set `s` of type `ι`, the functions `f : ι → α` and `g : ι → β` antivary on `s` with respect to the inverse of `f` if and only if they monovary on `s` with respect to `f`. In other words, if for all `i, j` in `s`, `g(i) < g(j)` implies `1/f(j) ≤ 1/f(i)`, then it also implies `f(i) ≤ f(j)`, and vice versa.
More concisely: For types `ι`, `α` with commutative ordered groups `α` and `β`, and functions `f : ι → α` and `g : ι → β` over `ι`, if `g` antivaries with respect to the inverse of `f` over a set `s`, then `f` and `g` monovary with respect to each other over `s`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.14
theorem Mathlib.Algebra.Order.Monovary._auxLemma.14 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{f : ι → α} {g : ι → β}, Monovary f (-g) = Antivary f g
The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.14` states that for any types `ι`, `α`, and `β`, where `α` and `β` have ordered additive commutative group structures, and any functions `f : ι → α` and `g : ι → β`, the function `f` monovaries with the negation of `g` if and only if `f` antivaries with `g`. In other words, if for any two elements `i` and `j` in the domain of `f` and `g`, `g(i) < g(j)` implies `f(i) ≤ f(j)`, then and only then `g(i) < g(j)` also implies `f(j) ≤ f(i)`.
More concisely: For functions $f : ι → α$ and $g : ι → β$ between ordered additive commutative groups, $f$ monovaries with the negation of $g$ if and only if $f$ antivaries with $g$. That is, $i < j$ implies $f(i) ≤ f(j)$ if and only if $i < j$ implies $f(j) ≤ f(i)$.
|
AntivaryOn.inv_left
theorem AntivaryOn.inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f g s → MonovaryOn f⁻¹ g s
This theorem, referred to as an alias of the reverse direction of `monovaryOn_inv_left`, states that for all types `ι`, `α`, and `β` where `α` and `β` are ordered commutative groups and `s` is a set of type `ι`, if a function `f` from `ι` to `α` antivaries with a function `g` from `ι` to `β` on `s`, then the inverse of `f` monovaries with `g` on `s`. In more informal terms, if `f` decreases when `g` increases, then the inverse of `f` increases when `g` increases, for all elements in the set `s`.
More concisely: If a function from a set to an ordered commutative group antivaries with another function on a subset, then the inverse of the first function monovaries with the second function on that subset.
|
Mathlib.Algebra.Order.Monovary._auxLemma.5
theorem Mathlib.Algebra.Order.Monovary._auxLemma.5 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f g⁻¹ s = AntivaryOn f g s
This theorem states that for any types `ι`, `α`, and `β` with `α` and `β` being ordered commutative groups, and for any set `s` of type `ι`, and any functions `f` from `ι` to `α` and `g` from `ι` to `β`, the function `f` monovaries with the inverse function `g⁻¹` on the set `s` if and only if the function `f` antivaries with the function `g` on the set `s`. In other words, if for all `i, j ∈ s`, `g(i) < g(j)` implies `f(i) ≤ f(j)` when considering `g⁻¹`, then the same condition implies `f(j) ≤ f(i)` when considering `g`.
More concisely: For types `ι`, `α` with `α` being an ordered commutative group, and functions `f: ι → α` and `g: ι → α⁇` from a set `s ∈ ι` with `g` order-preserving, `f` monovaries with `g⁻¹` on `s` if and only if `f` antivaries with `g` on `s`. Here, `α⁇` denotes the additive group inverse of `α`.
|
Monovary.inv_right
theorem Monovary.inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f g → Antivary f g⁻¹
The theorem `Monovary.inv_right` states that for any two types `ι` and `α`, and any two types `β` and `ι`, where `α` and `β` are ordered commutative groups, if a function `f` from `ι` to `α` monovaries with a function `g` from `ι` to `β`, then `f` antivaries with the inverse `g⁻¹` of `g`. In other words, if when `g` increases, `f` does not decrease (monovary), then when `g` decreases (as `g⁻¹` is increasing), `f` does not increase (antivary).
More concisely: If a function from one commutative group to another, ordered commutative group monovaries with a function between the same domains, then it antivaries with the inverse of that function.
|
MonovaryOn.inv_right
theorem MonovaryOn.inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f g s → AntivaryOn f g⁻¹ s
The theorem `MonovaryOn.inv_right` states that for any ordered commutative group `α` and `β`, and any set `s` of type `ι`, if a function `f : ι → α` monovaries with a function `g : ι → β` on `s`, then `f` antivaries with the inverse of `g` on `s`. Here, "monovaries" means that if `g i` is less than `g j` for any `i, j` in `s`, then `f i` is less than or equal to `f j`. "Antivaries", on the other hand, means that if `g i` is less than `g j` for any `i, j` in `s`, then `f j` is less than or equal to `f i`. In other words, the theorem describes a situation where the relationship of `f` to `g` switches from being direct to inverse when the function `g` is replaced by its inverse.
More concisely: If a function `f : ι → α` monovaries with another function `g : ι → β` on a set `s`, then `f` antivaries with the inverse of `g` on `s`.
|
monovaryOn_iff_smul_rearrangement
theorem monovaryOn_iff_smul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι},
MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j
The theorem states that for any set `s` of elements of some type `ι`, and any two functions `f : ι → α` and `g : ι → β` where `α` is a linear ordered ring and `β` is a linear ordered add commutative group with an ordered scalar multiplication operation on `α` and `β`, the functions `f` and `g` monovary on `s` if and only if for all elements `i` and `j` in `s`, the inequality `f i * g j + f j * g i ≤ f i * g i + f j * g j` holds. Here, monovarying means that if `g i < g j`, then `f i ≤ f j`.
More concisely: For sets `s` of elements from a type, functions `f : ι → α` (where `α` is a linear ordered ring) and `g : ι → β` (where `β` is a linear ordered add commutative group with ordered scalar multiplication) monovary on `s` if and only if for all `i, j` in `s`, `f i * g j + f j * g i ≤ f i * g i + f j * g j`.
|
AntivaryOn.inv
theorem AntivaryOn.inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f g s → AntivaryOn f⁻¹ g⁻¹ s
This theorem, called "AntivaryOn.inv", states the following: for any types `ι`, `α`, and `β`, where `α` and `β` are both ordered commutative groups, for any set `s` of type `ι`, and for any functions `f` from `ι` to `α` and `g` from `ι` to `β`, if `f` and `g` are antivarying on `s`, then the inverses of `f` and `g` (denoted `f⁻¹` and `g⁻¹`) will also be antivarying on `s`. Here, `f` and `g` are said to antivary on `s` if, for all `i, j` in `s`, `g i < g j` implies `f j ≤ f i`.
More concisely: If functions `f: ι -> α` and `g: ι -> β` are antivarying on a set `s` of type `ι`, then their inverses `f⁻¹` and `g⁻¹` are also antivarying on `s`, where `α` and `β` are ordered commutative groups.
|
Antivary.of_inv_left
theorem Antivary.of_inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f⁻¹ g → Monovary f g
This theorem, referred to as **Alias** of the forward direction of `antivary_inv_left`, states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, and for any functions `f : ι → α` and `g : ι → β`, if `f⁻¹` (the inverse function of `f`) antivaries with `g` (i.e., `g i < g j` implies `(f⁻¹) j ≤ (f⁻¹) i` for all `i` and `j`), then `f` monovaries with `g` (i.e., `g i < g j` implies `f i ≤ f j` for all `i` and `j`).
More concisely: If a function `f : ι → α` (where `α` is an ordered commutative group) has an inverse function `f⁻¹` that antivaries with another function `g : ι → β` (i.e., `g i < g j` implies `(f⁻¹) j ≤ (f⁻¹) i`), then `f` monovaries with `g` (i.e., `g i < g j` implies `f i ≤ f j`).
|
Antivary.of_inv_left₀
theorem Antivary.of_inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → Antivary f⁻¹ g → Monovary f g
This theorem, named `Antivary.of_inv_left₀`, states that for any types `ι`, `α`, and `β` where `α` and `β` are linearly ordered semi-fields, given any two functions `f : ι → α` and `g : ι → β`, if `0` is strongly less than `f` (meaning, `0 < f(i)` for all `i` in `ι`) and `f⁻¹` antivaries with `g` (meaning, whenever `g(i) < g(j)`, we have `f⁻¹(j) ≤ f⁻¹(i)`), then `f` monovaries with `g` (meaning, whenever `g(i) < g(j)`, we have `f(i) ≤ f(j)`). In simpler terms, this theorem relates the conditions under which a function is increasing in relation to another function and its inverse.
More concisely: If `0` is strictly less than every image of a function `f : ι → α` over a linearly ordered semi-field `ι`, and the inverse function `f⁻¹` antitone-preserves the order of another function `g : ι → β`, then `f` is order-preserving (monotonic) with respect to `g`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.15
theorem Mathlib.Algebra.Order.Monovary._auxLemma.15 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f g⁻¹ = Monovary f g
The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.15` states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, and for any functions `f : ι → α` and `g : ι → β`, the function `f` antivaries with the inverse of `g` if and only if `f` monovaries with `g`. In other words, if for all `i` and `j` such that `g⁻¹(i) < g⁻¹(j)` implies `f(j) ≤ f(i)`, it also holds true that `g(i) < g(j)` implies `f(i) ≤ f(j)`, and vice versa.
More concisely: For functions $f : ι → α$ and $g : ι → β$ between ordered commutative groups $α$ and $β$, $f$ antivaries with the inverse of $g$ if and only if $f$ monovaries with $g$.
|
Antivary.sub_smul_sub_nonpos
theorem Antivary.sub_smul_sub_nonpos :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β},
Antivary f g → ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
The theorem `Antivary.sub_smul_sub_nonpos` states that for any types `ι`, `α`, and `β`, given `α` is a linear ordered ring, `β` is a linear ordered additive commutative group, and `β` is a module over `α` with ordered scalar multiplication, if a function `f` from `ι` to `α` antivaries with a function `g` from `ι` to `β`, then for all `i` and `j` in `ι`, the scalar product of the differences `f(j) - f(i)` and `g(j) - g(i)` is less than or equal to zero. In other words, if `f` decreases when `g` increases, then the product of the differences between `f` and `g` at two points is always nonpositive.
More concisely: For functions $f:\ι \to \alpha$ and $g:\ι \to \beta$ with $\alpha$ a linear ordered ring, $\beta$ a linear ordered additive commutative group, and $\beta$ a $\alpha$-module with ordered scalar multiplication, if $f$ antivaries with $g$, then for all $i,j \in \ι$, the scalar product $f(j) - f(i) \cdot (g(j) - g(i)) \le 0$.
|
antivary_iff_mul_rearrangement
theorem antivary_iff_mul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α},
Antivary f g ↔ ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i
The theorem states that for any two functions `f` and `g` from the same domain `ι` to a linearly ordered ring `α`, the functions `f` and `g` antivary if and only if the rearrangement inequality holds for all pairs `i`, `j` in their domain. The rearrangement inequality here is expressed as `f i * g i + f j * g j ≤ f i * g j + f j * g i`. In other words, for all pairs of elements in the domain, the sum of the product of `f` and `g` at each element is less than or equal to the corresponding rearrangement of the terms.
More concisely: For functions `f` and `g` from a linearly ordered domain to a linearly ordered ring, `f` and `g` antivary if and only if the rearrangement inequality `f i * g i + f j * g j ≤ f i * g j + f j * g i` holds for all `i`, `j` in their domain.
|
Mathlib.Algebra.Order.Monovary._auxLemma.12
theorem Mathlib.Algebra.Order.Monovary._auxLemma.12 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{f : ι → α} {g : ι → β}, Antivary (-f) g = Monovary f g
The `Mathlib.Algebra.Order.Monovary._auxLemma.12` theorem states that for any two functions `f` and `g`, where `f` maps from an arbitrary type `ι` to an ordered additive commutative group `α`, and `g` maps from `ι` to another ordered additive commutative group `β`, the property of `f` being antivariant with `g` under negation (i.e., `f` decreasing when `g` increases) is equivalent to `f` being monovariant with `g` (i.e., `f` increasing when `g` increases).
More concisely: The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.12` in Lean 4 states that for functions `f : ι → α` and `g : ι → β` from an arbitrary type `ι` to ordered additive commutative groups `α` and `β`, respectively, `f` being antivariant with `g` under negation (i.e., `f(x) ≤ f(y)` whenever `g(x) ≥ g(y)`) is equivalent to `f` being monovariant with `g` (i.e., `f(x) ≤ f(y)` whenever `g(x) ≤ g(y)`).
|
Antivary.of_inv₀
theorem Antivary.of_inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → StrongLT 0 g → Antivary f⁻¹ g⁻¹ → Antivary f g
This theorem, referred to as the **Alias** of the forward direction of `antivary_inv₀`, states that for any types `ι`, `α`, and `β`, where `α` and `β` are linear ordered semifields, given two functions `f : ι → α` and `g : ι → β`, if `f` and `g` are both strongly greater than zero (i.e., for every `i`, `f(i) > 0` and `g(i) > 0`), and if the inverse function of `f` antivaries with the inverse function of `g` (i.e., for all `i, j`, if `g⁻¹(i) < g⁻¹(j)` then `f⁻¹(j) ≤ f⁻¹(i)`), then `f` antivaries with `g` (i.e., for all `i, j`, if `g(i) < g(j)` then `f(j) ≤ f(i)`).
More concisely: If `α` and `β` are linear ordered semifields, and `f : ι → α` and `g : ι → β` are strictly positive functions with `f⁻¹` antivariance with `g⁻¹`, then `f` antivariance holds between `f` and `g`.
|
Antivary.sub_mul_sub_nonpos
theorem Antivary.sub_mul_sub_nonpos :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α},
Antivary f g → ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0
This theorem, referred to as an alias of the forward direction of `antivary_iff_forall_mul_nonpos`, states that for any types `ι` and `α` where `α` is a linear ordered ring and functions `f` and `g` from `ι` to `α`, if `f` antivaries with `g` (meaning that if `g i` is less than `g j`, then `f j` is less than or equal to `f i`), then for any `i` and `j` in `ι`, the product of `(f j - f i)` and `(g j - g i)` is less than or equal to zero. In other words, the difference between the output of `f` and `g` when applied to `j` and `i`, when multiplied, is non-positive. This captures a kind of inverse relationship between `f` and `g`.
More concisely: For functions `f: ι -> α` and `g: ι -> α` from a linear ordered ring `α` over a type `ι`, if `f` antivaries with `g`, then for all `i, j ∈ ι`, `(f j - f i) * (g j - g i) ≤ 0`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.6
theorem Mathlib.Algebra.Order.Monovary._auxLemma.6 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f (-g) s = AntivaryOn f g s
This theorem states that for any set `s` of some type `ι`, a function `f` from `ι` to an ordered additive commutative group `α`, and a function `g` from `ι` to another ordered additive commutative group `β`, the function `f` monovaries with the negation of `g` on `s` if and only if `f` antivaries with `g` on `s`. In other words, if `f` increases when `-g` increases, then `f` decreases when `g` increases, and vice versa. This bridges the concept of monovariation and antivariation in the context of ordered additive commutative groups.
More concisely: For any functions $f : X \rightarrow (-\alpha, \infty), g : X \rightarrow \beta$ on ordered additive commutative groups, where $X$ is a set of some type, $f$ monovaries with the negation of $g$ if and only if $f$ antivaries with $g$.
|
Monovary.sub_smul_sub_nonneg
theorem Monovary.sub_smul_sub_nonneg :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β},
Monovary f g → ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)
The theorem `Monovary.sub_smul_sub_nonneg` states that for all types `ι`, `α`, and `β`, given a linear ordered ring instance for `α`, a linear ordered additive commutative group instance for `β`, a module instance for `α` and `β`, and an ordered scalar multiplication instance for `α` and `β`, if a function `f` from `ι` to `α` monovaries with another function `g` from `ι` to `β`, then for all `i` and `j` in `ι`, the scalar product of the difference between `f j` and `f i` and the difference between `g j` and `g i` is nonnegative, i.e., `0 ≤ (f j - f i) • (g j - g i)`. In mathematical terms, if `g i < g j` implies `f i ≤ f j`, then `0 ≤ (f(j) - f(i))(g(j) - g(i))` for all `i` and `j`.
More concisely: If `f: ι → α` monovaries with `g: ι → β` under ordered scalar multiplication in a linear ordered ring `α` and a linear ordered additive commutative group `β`, then for all `i, j ∈ ι` with `g(i) < g(j)`, we have `(f(j) - f(i))(g(j) - g(i)) ≥ 0`.
|
MonovaryOn.sub_smul_sub_nonneg
theorem MonovaryOn.sub_smul_sub_nonneg :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι},
MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)
This theorem, referred to as an alias of the forward direction of `monovaryOn_iff_forall_smul_nonneg`, essentially states that for any set `s` of a certain type `ι`, and any two functions `f : ι → α` and `g : ι → β`, where `α` is a linearly ordered ring and `β` is a linearly ordered additive commutative group with additional structure (a module over `α` and an ordered smul), if `f` monovaries with `g` on `s` (meaning that whenever `g i` is less than `g j` for any `i` and `j` in `s`, `f i` is less than or equal to `f j`), then for all `i` and `j` in `s`, the scalar product of the differences `(f j - f i)` and `(g j - g i)` is nonnegative. This theorem provides a connection between the concepts of monovariance and nonnegative scalar products of differences.
More concisely: If `f : ι -> α` and `g : ι -> β` are functions where `α` is a linearly ordered ring and `β` is a linearly ordered additive commutative group with module and ordered smul structures, and `f` monovaries with `g` on `s`, then for all `i, j` in `s`, the scalar product `(f j - f i) * (g j - g i)` is nonnegative.
|
Mathlib.Algebra.Order.Monovary._auxLemma.10
theorem Mathlib.Algebra.Order.Monovary._auxLemma.10 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{f : ι → α} {g : ι → β}, Monovary (-f) g = Antivary f g
The theorem `Mathlib.Algebra.Order.Monovary._auxLemma.10` states that for any types `ι`, `α`, and `β`, and for any functions `f : ι → α` and `g : ι → β`, where `α` and `β` are both ordered additive commutative groups, the condition that `-f` monovaries with `g` is equivalent to the condition that `f` antivaries with `g`. In other words, if for all `i` and `j`, `g i < g j` implies `-f i ≤ -f j`, then `g i < g j` also implies `f j ≤ f i` and vice versa.
More concisely: For functions `f : ι -> α` and `g : ι -> β` between ordered additive commutative groups `α` and `β`, `-f` monovaries with `g` if and only if `f` antivaries with `g`, i.e., `g i < g j` implies both `-f i <= -f j` and `f j <= f i`.
|
MonovaryOn.of_inv₀
theorem MonovaryOn.of_inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β},
(∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → MonovaryOn f⁻¹ g⁻¹ s → MonovaryOn f g s
This theorem, referred to as an "Alias" of the forward direction of `monovaryOn_inv₀`, states that for any types `ι`, `α`, and `β` with `α` and `β` being linear ordered semifields, and any set `s` of type `ι`, and functions `f : ι → α` and `g : ι → β`. If all elements `i` in the set `s` satisfy that `f i` and `g i` are both greater than 0, and the function `f⁻¹` monovaries with `g⁻¹` on `s`, then function `f` also monovaries with `g` on `s`. Here, monovarying means that if `g i < g j` then `f i ≤ f j` for all `i, j ∈ s`.
More concisely: If `f : ι → α` and `g : ι → β` are functions from a set `s` of linear ordered semifield types `ι`, `α`, and `β`, with `f i`, `g i` > 0 for all `i ∈ s`, and `f⁻¹` monovaries with `g⁻¹` on `s`, then `f` monovaries with `g` on `s`. (That is, if `g i < g j` for all `i, j ∈ s`, then `f i ≤ f j` holds.)
|
Monovary.of_inv₀
theorem Monovary.of_inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → StrongLT 0 g → Monovary f⁻¹ g⁻¹ → Monovary f g
The theorem `Monovary.of_inv₀` states that for any types `ι`, `α`, and `β`, where `α` and `β` are both linear ordered semifields, given two functions `f : ι → α` and `g : ι → β` that are strongly greater than zero (meaning for every `i`, `f(i)` and `g(i)` are both greater than zero), if the inverses of `f` and `g` monovary (meaning whenever `g⁻¹(i) < g⁻¹(j)`, it implies `f⁻¹(i) ≤ f⁻¹(j)`), then `f` and `g` themselves also monovary. In terms of mathematics, if $f(i) > 0$ and $g(i) > 0$ for all $i$, and whenever $g^{-1}(i) < g^{-1}(j)$ implies $f^{-1}(i) \leq f^{-1}(j)$, it follows that whenever $g(i) < g(j)$, $f(i) \leq f(j)$.
More concisely: If two functions from a type to linear ordered semifields, with inverses that monovary and are strictly positive, then the functions themselves are monotonic.
|
Mathlib.Algebra.Order.Monovary._auxLemma.8
theorem Mathlib.Algebra.Order.Monovary._auxLemma.8 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f (-g) s = MonovaryOn f g s
This theorem, named `Mathlib.Algebra.Order.Monovary._auxLemma.8`, establishes an equivalence between two types of variations, namely antivariation and monovariation, under a specific condition. Specifically, it states that for any typology `ι`, and any ordered additive commutative groups `α` and `β`, a function `f : ι → α` antivaries with the negation of function `g : ι → β` on a set `s` if and only if `f` monovaries with `g` on the same set `s`. In other words, if for all `i, j ∈ s`, `g i < g j` implies `f j ≤ f i` (definition of antivariation with `-g`), it is equivalent to saying that `g i < g j` implies `f i ≤ f j` (definition of monovariation with `g`).
More concisely: For any typology `ι`, ordered additive commutative groups `α` and `β`, and sets `s`, a function `f : ι → α` antivaries with the negation of `g : ι → β` on `s` if and only if `f` monovaries with `g` on `s`. That is, `g i < g j` implies `f j ≤ f i` (antivariation) if and only if `g i < g j` implies `f i ≤ f j` (monovariation).
|
Antivary.of_inv
theorem Antivary.of_inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f⁻¹ g⁻¹ → Antivary f g
The theorem `Antivary.of_inv` states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, if a function `f` antivaries with another function `g` under their inverse mappings, then `f` antivaries with `g` under their original mappings. In other words, given two functions `f: ι → α` and `g: ι → β`, if `g⁻¹(i) < g⁻¹(j)` implies `f⁻¹(j) ≤ f⁻¹(i)`, then `g(i) < g(j)` also implies `f(j) ≤ f(i)`.
More concisely: If `f: ι → α` and `g: ι → β` are functions between ordered commutative groups such that `g⁻¹(i) < g⁻¹(j)` implies `f⁻¹(j) ≤ f⁻¹(i)`, then `g(i) < g(j)` implies `f(j) ≤ f(i)`.
|
AntivaryOn.inv₀
theorem AntivaryOn.inv₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β},
(∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → AntivaryOn f g s → AntivaryOn f⁻¹ g⁻¹ s
The theorem `AntivaryOn.inv₀` states that for any types `ι`, `α`, and `β`, where `α` and `β` are linear ordered semifields, if we have a set `s` of type `ι`, and functions `f : ι → α` and `g : ι → β`, such that for every element `i` in `s`, `f(i)` and `g(i)` are both greater than zero, and the function `f` antivaries with the function `g` on the set `s` (meaning that whenever `g(i)` is less than `g(j)` for any `i` and `j` in `s`, `f(j)` is less than or equal to `f(i)`), then the function `f⁻¹` antivaries with the function `g⁻¹` on the set `s` (meaning that whenever `g⁻¹(i)` is less than `g⁻¹(j)` for any `i` and `j` in `s`, `f⁻¹(j)` is less than or equal to `f⁻¹(i)`). It could be seen as a generalization of the inverse function rule to the setting of antivariation.
More concisely: If functions `f : ι → α` and `g : ι → β` are linear ordered semifield homomorphisms with positive values on a set `s subset ι`, and `f` antivaries with `g` on `s`, then the inverse functions `f⁻¹` and `g⁻¹` antivary on `s`.
|
MonovaryOn.inv_left₀
theorem MonovaryOn.inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < f i) → MonovaryOn f g s → AntivaryOn f⁻¹ g s
This theorem, referred to as an alias of the reverse direction of `antivaryOn_inv_left₀`, states that for any set 's' of a certain type 'ι', and any two functions 'f : ι → α' and 'g : ι → β' (where α and β are linearly ordered semifields), if all elements 'i' in the set 's' satisfy the condition '0 < f i' and the function 'f' monovaries with 'g' on 's', then the inverse of 'f' antivaries with 'g' on 's'. In simpler terms, if all values of 'f' over 's' are positive and 'f' increases when 'g' increases, then as 'g' increases, the inverse of 'f' decreases.
More concisely: If 'f' is a function from a set 's' of positive elements in a linearly ordered semifield, and 'f' monovaries with another function 'g' on 's', then the inverse of 'f' antivaries with 'g' on 's'.
|
Monovary.smul_add_smul_le_smul_add_smul
theorem Monovary.smul_add_smul_le_smul_add_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β},
Monovary f g → ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j
This theorem states that, for all indexed types ι and types α and β such that α forms a linearly ordered ring, β forms a linearly ordered additive commutative group, and β is an α-module ordered by scalar multiplication, if a function f from ι to α monovaries with a function g from ι to β, then for all indices i, j in ι, the scalar product of f(i) and g(j) plus the scalar product of f(j) and g(i) is less than or equal to the scalar product of f(i) and g(i) plus the scalar product of f(j) and g(j). Basically, this theorem establishes a relationship between two functions that monovary, asserting a specific rearrangement inequality involving scalar products.
More concisely: For all indexed types ι, linearly ordered rings α, linearly ordered additive commutative groups β that are α-modules, and functions f : ι -> α and g : ι -> β with f monovarying g, the scalar product of f(i) and g(j) plus the scalar product of f(j) and g(i) is less than or equal to the sum of the scalar products of f(i) and g(i), and f(j) and g(j), for all i, j in ι.
|
MonovaryOn.smul_add_smul_le_smul_add_smul
theorem MonovaryOn.smul_add_smul_le_smul_add_smul :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι},
MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j
The theorem `MonovaryOn.smul_add_smul_le_smul_add_smul` states that for any set `s` and any two functions `f : ι → α` and `g : ι → β`, where `α` is a linearly ordered ring, `β` is a linearly ordered additive commutative group, and `β` is a module over `α` with an ordered scalar multiplication, if `f` monovaries with `g` on `s`, then for all `i` and `j` in `s`, the inequality `f(i)*g(j) + f(j)*g(i) ≤ f(i)*g(i) + f(j)*g(j)` holds. This theorem is an alias of the forward direction of the `monovaryOn_iff_smul_rearrangement` theorem, which says that two functions monovary if and only if the rearrangement inequality holds.
More concisely: For functions $f : ι → α$ and $g : ι → β$ over linearly ordered rings $\alpha$, additive commutative groups $\beta$, and $\beta$ being a module over $\alpha$ with an ordered scalar multiplication, if $f$ monovaries with $g$ on a set $s$, then for all $i, j$ in $s$, we have $f(i)*g(j) + f(j)*g(i) \leq f(i)*g(i) + f(j)*g(j)$.
|
Monovary.inv_left₀
theorem Monovary.inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 f → Monovary f g → Antivary f⁻¹ g
The theorem `Monovary.inv_left₀` states that for any types `ι`, `α`, and `β`, with `α` and `β` being linear ordered semifields, any functions `f: ι → α` and `g: ι → β`, if `f` is strictly greater than zero for all inputs (`StrongLT 0 f`), and `f` monovaries with `g` (meaning that whenever `g i` is less than `g j`, `f i` is less than or equal to `f j`), then the inverse of `f` antivaries with `g` (meaning that whenever `g i` is less than `g j`, `f^-1 j` is less than or equal to `f^-1 i`). This is essentially a statement about the transformation of a monovarying function to an antivarying function when it is strictly positive and inverted.
More concisely: If `f: ι → α` is a strictly positive, monovarying function from a linearly ordered index type `ι` to a linear ordered semifield `α`, then its inverse `f^-1` is an antivarying function with respect to `g`.
|
antivary_iff_smul_rearrangement
theorem antivary_iff_smul_rearrangement :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : OrderedSMul α β] {f : ι → α} {g : ι → β},
Antivary f g ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
The theorem states that for any two functions `f : ι → α` and `g : ι → β`, where `α` is a type with a structure of a linearly ordered ring, `β` is a type with a structure of a linearly ordered additive commutative group and also a module over `α`, and `ι` is any type, the functions `f` and `g` can be said to "antivary" if and only if the "rearrangement inequality" holds for all pairs of elements in `ι`. Here "antivary" means that if `g i` is less than `g j` then `f j` is less than or equal to `f i`. The "rearrangement inequality" is the inequality `f i • g i + f j • g j ≤ f i • g j + f j • g i`.
More concisely: For functions `f : ι -> α` and `g : ι -> β` over types `α` (linearly ordered ring) and `β` (linearly ordered additive commutative group and module over `α`), `f` and `g` antivary if and only if the rearrangement inequality `∑ i, j in ι, f i * g i + f j * g j ≤ f j * g i + f i * g j` holds.
|
MonovaryOn.inv_right₀
theorem MonovaryOn.inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < g i) → MonovaryOn f g s → AntivaryOn f g⁻¹ s
This theorem, referred to as **Alias** of the reverse direction of `antivaryOn_inv_right₀`, states that for all types ι, α, β, where α and β are linear ordered semifields, and for any set `s` of type ι, if we have two functions `f : ι → α` and `g : ι → β`, and for all elements `i` in `s`, `g i` is greater than 0, then if `f` is monovarying on `g` over `s`, it implies that `f` is antivarying on `g⁻¹` over `s`.
In other words, if `f` increases or remains the same whenever `g` increases for all elements in set `s` (that is, `f` monovaries with `g`), then `f` will decrease or remain the same whenever `g` decreases for all elements in set `s` (that is, `f` antivaries with the inverse of `g`). This is true when `g i` is greater than 0 for all `i` in set `s`.
More concisely: If `f : ι → α` is monovarying on `g : ι → β`, where `g` is a linear ordered semifield with `g i > 0` for all `i` in a set `s`, then `f` is antivarying on `g⁻¹` over `s`.
|
Antivary.mul_add_mul_le_mul_add_mul
theorem Antivary.mul_add_mul_le_mul_add_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α},
Antivary f g → ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i
The theorem `Antivary.mul_add_mul_le_mul_add_mul` states that for all types `ι` and `α`, where `α` is a linearly ordered ring, and for all functions `f` and `g` from `ι` to `α`, if `f` antivaries with `g` (meaning that whenever `g i` is less than `g j`, it follows that `f j` is less than or equal to `f i`), then for all `i` and `j` in `ι`, the inequality `f i * g i + f j * g j ≤ f i * g j + f j * g i` holds. This theorem connects the concept of antivariation with a specific inequality involving multiplication and addition of function values.
More concisely: For all linearly ordered rings `α` and functions `f` and `g` from a type `ι` to `α`, if `f` antivaries with `g`, then for all `i` and `j` in `ι`, we have `f i * g i + f j * g j ≤ f i * g j + f j * g i`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.2
theorem Mathlib.Algebra.Order.Monovary._auxLemma.2 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn (-f) g s = AntivaryOn f g s
This theorem states that for any types `ι`, `α` and `β` and for any two functions `f : ι → α` and `g : ι → β` defined on a set `s` of elements of type `ι`, the condition that `-f` monovaries with `g` on `s` is equivalent to `f` antivaries with `g` on `s`. Here, `α` and `β` are ordered additive commutative groups, which give an ordering and addition operation on `α` and `β`. The term "monovary" means that as `g` increases, `-f` does not decrease, and "antivary" means that as `g` increases, `f` does not increase.
More concisely: For functions `f : ι -> α` and `g : ι -> β` on a set `s` with `α` and `β` ordered additive commutative groups, `-f` monovaries with `g` if and only if `f` antivaries with `g`, that is, `g(x) > g(y) => -f(x) <= -f(y) <-> f(x) <= f(y)` for all `x, y in s`.
|
Monovary.inv_right₀
theorem Monovary.inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{f : ι → α} {g : ι → β}, StrongLT 0 g → Monovary f g → Antivary f g⁻¹
The theorem `Monovary.inv_right₀` states that for any types `ι`, `α`, and `β`, with `α` and `β` being linear ordered semifields, and given functions `f : ι → α` and `g : ι → β`, if the function `g` is strongly greater than the zero function (i.e., `g i > 0` for all `i` in `ι`), and `f` monovaries with `g` (meaning that whenever `g i < g j`, we have `f i ≤ f j`), then `f` antivaries with the inverse of `g` (that is, whenever `g i < g j`, we have `f j ≤ f i`). Essentially, if a function `f` increases as `g` increases (monovaries), then `f` will decrease as `1/g` increases (antivaries), provided `g` is always positive.
More concisely: If `f : ι → α` monovaries with the strictly positive function `g : ι → β`, then `f` antivaries with the inverse function of `g`.
|
Monovary.of_inv
theorem Monovary.of_inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f⁻¹ g⁻¹ → Monovary f g
The theorem `Monovary.of_inv` is an alias of the forward direction of `monovary_inv`. It states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, and any functions `f : ι → α` and `g : ι → β`, if `f` and `g` are monovariant with respect to their inverses—that is, for any `i` and `j` such that `g⁻¹(i) < g⁻¹(j)`, we have `f⁻¹(i) ≤ f⁻¹(j)`—then `f` and `g` are monovariant—that is, for any `i` and `j` such that `g(i) < g(j)`, we have `f(i) ≤ f(j)`.
More concisely: If functions `f : ι → α` and `g : ι → β` between ordered commutative groups are monovariant with respect to their inverses, then they are monovariant.
|
MonovaryOn.sub_mul_sub_nonneg
theorem MonovaryOn.sub_mul_sub_nonneg :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} {s : Set ι},
MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)
This theorem, referred to as an alias of the forward direction of `monovaryOn_iff_forall_mul_nonneg`, states that for any types `ι` and `α`, where `α` is a linear ordered ring, for any functions `f` and `g` from `ι` to `α`, and for any set `s` of type `ι`, if `f` monovaries with `g` on `s` (meaning that whenever `g i` is less than `g j` for any `i, j` in `s`, then `f i` is less than or equal to `f j`), then for any `i, j` in `s`, the result of `(f j - f i) * (g j - g i)` will always be greater than or equal to zero. In mathematical terms, it can be written as if $g(i) < g(j)$ implies $f(i) \leq f(j)$ for all $i, j \in s$, then $0 \leq (f(j) - f(i)) * (g(j) - g(i))$ for all $i, j \in s$.
More concisely: For any types `ι` and `α` where `α` is a linear ordered ring, and for any functions `f` and `g` from `ι` to `α`, if `f` monovaries with `g` on a set `s`, then `(f j - f i) * (g j - g i)` is non-negative for all `i, j` in `s`.
|
MonovaryOn.of_inv
theorem MonovaryOn.of_inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f⁻¹ g⁻¹ s → MonovaryOn f g s
This theorem, known as `MonovaryOn.of_inv`, states that for any types `ι`, `α`, and `β`, if `α` and `β` are both ordered commutative groups and we have a set `s` of type `ι`, and functions `f : ι → α` and `g : ι → β`, then if the inverse of `f` monovaries with the inverse of `g` on the set `s`, it implies that `f` also monovaries with `g` on the same set `s`. In simpler words, if an increase in `g⁻¹` leads to a non-decrease in `f⁻¹` for all elements in `s`, then the same holds for `f` and `g` themselves.
More concisely: If the inverse of a function `g : ι → β` makes the inverse of another function `f : ι → α` non-decreasing on a set `s`, then `f` is non-decreasing with respect to `g` on `s`.
|
Monovary.sub_mul_sub_nonneg
theorem Monovary.sub_mul_sub_nonneg :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α},
Monovary f g → ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)
This theorem, referred to as an alias of the forward direction of `monovary_iff_forall_mul_nonneg`, states that for any types `ι` and `α` where `α` is a linearly ordered ring, and any functions `f` and `g` from `ι` to `α`, if `f` monovaries with `g` (i.e., whenever `g(i)` is less than `g(j)`, `f(i)` is less than or equal to `f(j)`), then for any `i` and `j` in `ι`, the expression `(f(j) - f(i)) * (g(j) - g(i))` is greater than or equal to zero. In other words, the product of the differences between the values of `f` and the values of `g` is nonnegative.
More concisely: If `f` monovaries with `g` over a linearly ordered ring `α`, then for all `i` and `j` in the domain of `f`, the product `(f(j) - f(i)) * (g(j) - g(i))` is nonnegative.
|
AntivaryOn.of_inv_right
theorem AntivaryOn.of_inv_right :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f g⁻¹ s → MonovaryOn f g s
The theorem `AntivaryOn.of_inv_right` states that for any types `ι`, `α`, and `β`, where `α` and `β` are ordered commutative groups, and for any set `s` of type `ι` and functions `f : ι → α` and `g : ι → β`, if `f` antivaries with the inverse of `g` on `s` (that is, whenever `g j < g i` for some `i, j` in `s`, we have `f i ≤ f j`), then `f` monovaries with `g` on `s` (that is, whenever `g i < g j` for some `i, j` in `s`, we have `f i ≤ f j`). This theorem is a particular case of `antivaryOn_inv_right`, and hence given the alias name.
More concisely: If a function between ordered commutative groups antivaries with the inverse of another function on a set, then it monovaries with that function on the same set.
|
AntivaryOn.of_inv_right₀
theorem AntivaryOn.of_inv_right₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < g i) → AntivaryOn f g⁻¹ s → MonovaryOn f g s
The theorem `AntivaryOn.of_inv_right₀` states that for any types `ι`, `α`, and `β` where `α` and `β` are linear ordered semifields, any set `s` of type `ι`, and any functions `f : ι → α` and `g : ι → β`, if every element `i` in `s` satisfies `0 < g i` and the function `f` antivaries with the inverse of `g` on `s` (meaning that `g i < g j` implies `f j ≤ f i` for all `i, j ∈ s`), then the function `f` also monovaries with `g` on `s` (meaning that `g i < g j` implies `f i ≤ f j` for all `i, j ∈ s`). In simpler terms, if a function decreases as another function's inverse increases, then the original function also increases as the second function increases, given that the second function's values are all positive.
More concisely: If `f : ι -> α` and `g : ι -> β` are functions on a linearly ordered semifield `ι`, `α`, and `β`, with `β` positive, and `f` antivaries with the inverse of `g` on `s`, then `f` monovaries with `g` on `s`.
|
Mathlib.Algebra.Order.Monovary._auxLemma.4
theorem Mathlib.Algebra.Order.Monovary._auxLemma.4 :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : OrderedAddCommGroup β]
{s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn (-f) g s = MonovaryOn f g s
This theorem states that for any set `s` of elements of type `ι`, and any two functions `f : ι → α` and `g : ι → β`, where `α` and `β` are both ordered additive commutative groups, the condition that `-f` antivaries with `g` on `s` is equivalent to `f` monovaries with `g` on `s`. In other words, `g` increasing while `-f` decreases is the same as `g` increasing while `f` also increases over the set `s`.
More concisely: For sets `s` of elements, functions `f : ι → α` and `g : ι → β` from the same index type `ι` with values in ordered additive commutative groups `α` and `β`, respectively, the condition that `-f` antitones (or decreases) with `g` is equivalent to `f` cotones (or increases) with `g` on `s`.
|
AntivaryOn.mul_add_mul_le_mul_add_mul
theorem AntivaryOn.mul_add_mul_le_mul_add_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrderedRing α] {f g : ι → α} {s : Set ι},
AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i
The theorem `AntivaryOn.mul_add_mul_le_mul_add_mul` states that for a given type `ι` and a linear ordered ring `α`, if two functions `f` and `g` from `ι` to `α` satisfy the property of antivarying on a certain set `s` of `ι`, then for all elements `i` and `j` in `s`, the inequality `f(i)*g(i) + f(j)*g(j) ≤ f(i)*g(j) + f(j)*g(i)` holds. Here, a function `f` antivaries with a function `g` on a set `s` if when `g(i)` is less than `g(j)`, `f(j)` is less than or equal to `f(i)` for all elements `i` and `j` in `s`.
More concisely: For functions `f` and `g` from a linearly ordered index type `ι` to a linear ordered ring `α` that antivary on a set `s ⊆ ι`, the inequality `f(i)*g(i) + f(j)*g(j) ≤ f(i)*g(j) + f(j)*g(i)` holds for all `i, j ∈ s` with `g(i) < g(j)`.
|
Monovary.inv_left
theorem Monovary.inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Monovary f g → Antivary f⁻¹ g
The theorem `Monovary.inv_left` states that for any types ι, α, and β, where α and β are ordered commutative groups, if a function `f` (from ι to α) monovaries with a function `g` (from ι to β), then the inverse function of `f` will antivary with `g`. In other words, if for any `i` and `j` in ι, `g i < g j` implying `f i ≤ f j`, then it's also true that `g i < g j` will imply `(f i)⁻¹ ≥ (f j)⁻¹`.
More concisely: If functions `f` from `ι` to `α` and `g` from `ι` to `β` satisfy `α` and `β` being ordered commutative groups and the monotonicity condition `g i < g j → f i ≤ f j` for all `i, j` in `ι`, then `g i < g j` implies `(f i)⁻¹ ≥ (f j)⁻¹`.
|
Antivary.inv
theorem Antivary.inv :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {f : ι → α}
{g : ι → β}, Antivary f g → Antivary f⁻¹ g⁻¹
The theorem `Antivary.inv` states that for all types `ι`, `α`, `β` where `α` and `β` have the structure of an ordered commutative group, if a function `f` from `ι` to `α` antivaries with a function `g` from `ι` to `β`, then the function `f⁻¹` (the inverse of `f` under the group operation) antivaries with `g⁻¹` (the inverse of `g` under the group operation). In other words, if for all indices `i` and `j`, when `g(i) < g(j)` implies `f(j) ≤ f(i)`, then for the inversed functions, `g⁻¹(i) < g⁻¹(j)` will imply `f⁻¹(j) ≤ f⁻¹(i)`.
More concisely: If functions `f: ι -> α` and `g: ι -> β` are ordered commutative groups with `f` antivariant with respect to `g`, then the inverse functions `f⁻¹` and `g⁻¹` are also antivariant.
|
MonovaryOn.inv_left
theorem MonovaryOn.inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, MonovaryOn f g s → AntivaryOn f⁻¹ g s
The theorem `MonovaryOn.inv_left` states that for any ordered commutative group `α` and `β`, a set `s` of type `ι`, and mappings `f: ι → α` and `g: ι → β`, if `f` monovaries with `g` on `s` (that is, whenever `g i < g j` it follows that `f i ≤ f j` for all `i, j` in `s`), then the inverse of `f` antivaries with `g` on `s` (meaning that whenever `g i < g j`, it follows that `(f⁻¹) j ≤ (f⁻¹) i` for all `i, j` in `s`). This theorem is essentially a restatement of `antivaryOn_inv_left` in the opposite direction.
More concisely: If `f: ι --> α` monovaries with `g: ι --> β` on a set `s`, then the inverse function `(f^-1): β --> α` antivaries with `g` on `s`.
|
AntivaryOn.of_inv_left
theorem AntivaryOn.of_inv_left :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : OrderedCommGroup α] [inst_1 : OrderedCommGroup β] {s : Set ι}
{f : ι → α} {g : ι → β}, AntivaryOn f⁻¹ g s → MonovaryOn f g s
The theorem named `AntivaryOn.of_inv_left` states that for any types `ι`, `α`, `β`, where `α` and `β` are ordered commutative groups, and for any set `s` of type `ι`, if a function `f⁻¹` antivaries with a function `g` on `s`, then the function `f` monovaries with the function `g` on `s`. Here, a function `f⁻¹` is said to antivary with a function `g` on `s` if for all `i, j` in `s`, `g(i) < g(j)` implies `f⁻¹(j) ≤ f⁻¹(i)`. Similarly, a function `f` is said to monovary with a function `g` on `s` if for all `i, j` in `s`, `g(i) < g(j)` implies `f(i) ≤ f(j)`.
More concisely: If a function `f`'s inverse antivaries with a function `g` on a set `s` of ordered commutative groups, then `f` monovaries with `g` on `s`.
|
AntivaryOn.of_inv_left₀
theorem AntivaryOn.of_inv_left₀ :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrderedSemifield α] [inst_1 : LinearOrderedSemifield β]
{s : Set ι} {f : ι → α} {g : ι → β}, (∀ i ∈ s, 0 < f i) → AntivaryOn f⁻¹ g s → MonovaryOn f g s
This theorem, named `AntivaryOn.of_inv_left₀`, states that for any set `s` of elements of type `ι`, and any two functions `f : ι → α` and `g : ι → β`, where `α` and `β` are both types with a linear ordered semifield structure, if every element `i` in `s` maps to a positive number under `f`, and the inverse of `f` antivaries with `g` on `s` (i.e., whenever `g i < g j` for any two elements `i, j` in `s`, we have `f j ≤ f i`), then `f` monovaries with `g` on `s` (i.e., whenever `g i < g j`, we have `f i ≤ f j`). In simpler terms, if `f` and `g` are inversely related and `f` only produces positive results, then `f` and `g` are also directly related.
More concisely: If `f : ι → α` and `g : ι → β` are functions from a set `s` of elements with positive images under `f`, and `f` is inverse-ordered with `g` on `s`, then `f` is order-preserving with respect to `g` on `s` (i.e., `f i ≤ f j` whenever `g i < g j`).
|