# Documentation

Mathlib.Algebra.Order.Monovary

# Monovarying functions and algebraic operations #

This file characterises the interaction of ordered algebraic structures with monovariance of functions.

Algebra.Order.Rearrangement for the n-ary rearrangement inequality

### Algebraic operations on monovarying functions #

@[simp]
theorem monovaryOn_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn (-f) g s AntivaryOn f g s
@[simp]
theorem monovaryOn_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
@[simp]
theorem antivaryOn_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn (-f) g s MonovaryOn f g s
@[simp]
theorem antivaryOn_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
@[simp]
theorem monovaryOn_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f (-g) s AntivaryOn f g s
@[simp]
theorem monovaryOn_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
@[simp]
theorem antivaryOn_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f (-g) s MonovaryOn f g s
@[simp]
theorem antivaryOn_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
theorem monovaryOn_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn (-f) (-g) s MonovaryOn f g s
theorem monovaryOn_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
theorem antivaryOn_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn (-f) (-g) s AntivaryOn f g s
theorem antivaryOn_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
@[simp]
theorem monovary_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
@[simp]
theorem monovary_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
@[simp]
theorem antivary_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
@[simp]
theorem antivary_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
@[simp]
theorem monovary_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
@[simp]
theorem monovary_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
@[simp]
theorem antivary_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
@[simp]
theorem antivary_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
theorem monovary_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Monovary (-f) (-g) Monovary f g
theorem monovary_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
theorem antivary_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Antivary (-f) (-g) Antivary f g
theorem antivary_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
theorem AntivaryOn.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g sMonovaryOn f⁻¹ g s

Alias of the reverse direction of monovaryOn_inv_left.

theorem MonovaryOn.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f⁻¹ g sAntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_left.

theorem AntivaryOn.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g sMonovaryOn (-f) g s
theorem MonovaryOn.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn (-f) g sAntivaryOn f g s
theorem AntivaryOn.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f⁻¹ g sMonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_left.

theorem MonovaryOn.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g sAntivaryOn f⁻¹ g s

Alias of the reverse direction of antivaryOn_inv_left.

theorem MonovaryOn.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g sAntivaryOn (-f) g s
theorem AntivaryOn.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn (-f) g sMonovaryOn f g s
theorem AntivaryOn.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g sMonovaryOn f g⁻¹ s

Alias of the reverse direction of monovaryOn_inv_right.

theorem MonovaryOn.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g⁻¹ sAntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_right.

theorem AntivaryOn.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g sMonovaryOn f (-g) s
theorem MonovaryOn.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f (-g) sAntivaryOn f g s
theorem AntivaryOn.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g⁻¹ sMonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_right.

theorem MonovaryOn.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g sAntivaryOn f g⁻¹ s

Alias of the reverse direction of antivaryOn_inv_right.

theorem AntivaryOn.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f (-g) sMonovaryOn f g s
theorem MonovaryOn.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g sAntivaryOn f (-g) s
theorem MonovaryOn.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g s

Alias of the forward direction of monovaryOn_inv.

theorem MonovaryOn.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g s

Alias of the reverse direction of monovaryOn_inv.

theorem MonovaryOn.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn (-f) (-g) sMonovaryOn f g s
theorem MonovaryOn.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
MonovaryOn f g sMonovaryOn (-f) (-g) s
theorem AntivaryOn.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g s

Alias of the forward direction of antivaryOn_inv.

theorem AntivaryOn.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g s

Alias of the reverse direction of antivaryOn_inv.

theorem AntivaryOn.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn (-f) (-g) sAntivaryOn f g s
theorem AntivaryOn.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} :
AntivaryOn f g sAntivaryOn (-f) (-g) s
theorem Antivary.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Antivary f g

Alias of the reverse direction of monovary_inv_left.

theorem Monovary.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Antivary f g

Alias of the forward direction of monovary_inv_left.

theorem Monovary.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Monovary (-f) gAntivary f g
theorem Antivary.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Antivary f gMonovary (-f) g
theorem Antivary.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Monovary f g

Alias of the forward direction of antivary_inv_left.

theorem Monovary.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Monovary f g

Alias of the reverse direction of antivary_inv_left.

theorem Antivary.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Antivary (-f) gMonovary f g
theorem Monovary.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Monovary f gAntivary (-f) g
theorem Monovary.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Antivary f g

Alias of the forward direction of monovary_inv_right.

theorem Antivary.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Antivary f g

Alias of the reverse direction of monovary_inv_right.

theorem Antivary.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Antivary f gMonovary f (-g)
theorem Monovary.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Monovary f (-g)Antivary f g
theorem Monovary.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Monovary f g

Alias of the reverse direction of antivary_inv_right.

theorem Antivary.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Monovary f g

Alias of the forward direction of antivary_inv_right.

theorem Antivary.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Antivary f (-g)Monovary f g
theorem Monovary.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Monovary f gAntivary f (-g)
theorem Monovary.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Monovary f g

Alias of the forward direction of monovary_inv.

theorem Monovary.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Monovary f g

Alias of the reverse direction of monovary_inv.

theorem Monovary.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Monovary f gMonovary (-f) (-g)
theorem Monovary.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Monovary (-f) (-g)Monovary f g
theorem Antivary.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Antivary f g

Alias of the reverse direction of antivary_inv.

theorem Antivary.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} :
Antivary f g

Alias of the forward direction of antivary_inv.

theorem Antivary.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Antivary f gAntivary (-f) (-g)
theorem Antivary.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} :
Antivary (-f) (-g)Antivary f g
theorem MonovaryOn.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : MonovaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) :
MonovaryOn (f₁ + f₂) g s
theorem MonovaryOn.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : MonovaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) :
MonovaryOn (f₁ * f₂) g s
theorem AntivaryOn.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : AntivaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) :
AntivaryOn (f₁ + f₂) g s
theorem AntivaryOn.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : AntivaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) :
AntivaryOn (f₁ * f₂) g s
theorem MonovaryOn.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : MonovaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) :
MonovaryOn (f₁ - f₂) g s
theorem MonovaryOn.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : MonovaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) :
MonovaryOn (f₁ / f₂) g s
theorem AntivaryOn.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : AntivaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) :
AntivaryOn (f₁ - f₂) g s
theorem AntivaryOn.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : AntivaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) :
AntivaryOn (f₁ / f₂) g s
theorem MonovaryOn.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (n : ) :
MonovaryOn (n f) g s
theorem MonovaryOn.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (n : ) :
MonovaryOn (f ^ n) g s
theorem AntivaryOn.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (n : ) :
AntivaryOn (n f) g s
theorem AntivaryOn.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (n : ) :
AntivaryOn (f ^ n) g s
theorem Monovary.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Monovary f₁ g) (h₂ : Monovary f₂ g) :
Monovary (f₁ + f₂) g
theorem Monovary.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Monovary f₁ g) (h₂ : Monovary f₂ g) :
Monovary (f₁ * f₂) g
theorem Antivary.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) :
Antivary (f₁ + f₂) g
theorem Antivary.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) :
Antivary (f₁ * f₂) g
theorem Monovary.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Monovary f₁ g) (h₂ : Antivary f₂ g) :
Monovary (f₁ - f₂) g
theorem Monovary.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Monovary f₁ g) (h₂ : Antivary f₂ g) :
Monovary (f₁ / f₂) g
theorem Antivary.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) :
Antivary (f₁ - f₂) g
theorem Antivary.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f₁ : ια} {f₂ : ια} {g : ιβ} (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) :
Antivary (f₁ / f₂) g
theorem Monovary.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hfg : Monovary f g) (n : ) :
Monovary (n f) g
theorem Monovary.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} (hfg : Monovary f g) (n : ) :
Monovary (f ^ n) g
theorem Antivary.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hfg : Antivary f g) (n : ) :
Antivary (n f) g
theorem Antivary.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} (hfg : Antivary f g) (n : ) :
Antivary (f ^ n) g
theorem MonovaryOn.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) :
MonovaryOn f (g₁ + g₂) s
theorem MonovaryOn.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) :
MonovaryOn f (g₁ * g₂) s
theorem AntivaryOn.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : AntivaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) :
AntivaryOn f (g₁ + g₂) s
theorem AntivaryOn.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : AntivaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) :
AntivaryOn f (g₁ * g₂) s
theorem MonovaryOn.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : MonovaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) :
MonovaryOn f (g₁ - g₂) s
theorem MonovaryOn.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : MonovaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) :
MonovaryOn f (g₁ / g₂) s
theorem AntivaryOn.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : AntivaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) :
AntivaryOn f (g₁ - g₂) s
theorem AntivaryOn.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : AntivaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) :
AntivaryOn f (g₁ / g₂) s
theorem MonovaryOn.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (n : ) :
MonovaryOn f (n g) s
theorem MonovaryOn.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {s : Set ι} {f : ια} {g : ιβ} (hfg : MonovaryOn f g s) (n : ) :
MonovaryOn f (g ^ n) s
theorem AntivaryOn.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (n : ) :
AntivaryOn f (n g) s
theorem AntivaryOn.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {s : Set ι} {f : ια} {g : ιβ} (hfg : AntivaryOn f g s) (n : ) :
AntivaryOn f (g ^ n) s
theorem Monovary.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Monovary f g₁) (h₂ : Monovary f g₂) :
Monovary f (g₁ + g₂)
theorem Monovary.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Monovary f g₁) (h₂ : Monovary f g₂) :
Monovary f (g₁ * g₂)
theorem Antivary.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) :
Antivary f (g₁ + g₂)
theorem Antivary.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) :
Antivary f (g₁ * g₂)
theorem Monovary.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) :
Monovary f (g₁ - g₂)
theorem Monovary.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) :
Monovary f (g₁ / g₂)
theorem Antivary.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) :
Antivary f (g₁ - g₂)
theorem Antivary.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {f : ια} {g₁ : ιβ} {g₂ : ιβ} (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) :
Antivary f (g₁ / g₂)
theorem Monovary.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hfg : Monovary f g) (n : ) :
Monovary f (n g)
theorem Monovary.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {f : ια} {g : ιβ} (hfg : Monovary f g) (n : ) :
Monovary f (g ^ n)
theorem Antivary.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hfg : Antivary f g) (n : ) :
Antivary f (n g)
theorem Antivary.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] {f : ια} {g : ιβ} (hfg : Antivary f g) (n : ) :
Antivary f (g ^ n)
theorem MonovaryOn.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : is, 0 f₁ i) (hf₂ : is, 0 f₂ i) (h₁ : MonovaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) :
MonovaryOn (f₁ * f₂) g s
theorem AntivaryOn.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : is, 0 f₁ i) (hf₂ : is, 0 f₂ i) (h₁ : AntivaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) :
AntivaryOn (f₁ * f₂) g s
theorem MonovaryOn.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 f i) (hfg : MonovaryOn f g s) (n : ) :
MonovaryOn (f ^ n) g s
theorem AntivaryOn.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 f i) (hfg : AntivaryOn f g s) (n : ) :
AntivaryOn (f ^ n) g s
theorem Monovary.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : 0 f₁) (hf₂ : 0 f₂) (h₁ : Monovary f₁ g) (h₂ : Monovary f₂ g) :
Monovary (f₁ * f₂) g
theorem Antivary.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : 0 f₁) (hf₂ : 0 f₂) (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) :
Antivary (f₁ * f₂) g
theorem Monovary.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} (hf : 0 f) (hfg : Monovary f g) (n : ) :
Monovary (f ^ n) g
theorem Antivary.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {f : ια} {g : ιβ} (hf : 0 f) (hfg : Antivary f g) (n : ) :
Antivary (f ^ n) g
theorem MonovaryOn.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : is, 0 g₁ i) (hg₂ : is, 0 g₂ i) (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) :
MonovaryOn f (g₁ * g₂) s
theorem AntivaryOn.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : is, 0 g₁ i) (hg₂ : is, 0 g₂ i) (h₁ : AntivaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) :
AntivaryOn f (g₁ * g₂) s
theorem MonovaryOn.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 g i) (hfg : MonovaryOn f g s) (n : ) :
MonovaryOn f (g ^ n) s
theorem AntivaryOn.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 g i) (hfg : AntivaryOn f g s) (n : ) :
AntivaryOn f (g ^ n) s
theorem Monovary.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : 0 g₁) (hg₂ : 0 g₂) (h₁ : Monovary f g₁) (h₂ : Monovary f g₂) :
Monovary f (g₁ * g₂)
theorem Antivary.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : 0 g₁) (hg₂ : 0 g₂) (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) :
Antivary f (g₁ * g₂)
theorem Monovary.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : 0 g) (hfg : Monovary f g) (n : ) :
Monovary f (g ^ n)
theorem Antivary.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : 0 g) (hfg : Antivary f g) (n : ) :
Antivary f (g ^ n)
@[simp]
theorem monovaryOn_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) :
@[simp]
theorem antivaryOn_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) :
@[simp]
theorem monovaryOn_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 < g i) :
@[simp]
theorem antivaryOn_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 < g i) :
theorem monovaryOn_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) (hg : is, 0 < g i) :
theorem antivaryOn_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) (hg : is, 0 < g i) :
@[simp]
theorem monovary_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) :
@[simp]
theorem antivary_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) :
@[simp]
theorem monovary_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : StrongLT 0 g) :
@[simp]
theorem antivary_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : StrongLT 0 g) :
theorem monovary_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) (hg : StrongLT 0 g) :
theorem antivary_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) (hg : StrongLT 0 g) :
theorem MonovaryOn.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) :
MonovaryOn f⁻¹ g sAntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_left₀.

theorem AntivaryOn.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) :
AntivaryOn f g sMonovaryOn f⁻¹ g s

Alias of the reverse direction of monovaryOn_inv_left₀.

theorem MonovaryOn.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) :
MonovaryOn f g sAntivaryOn f⁻¹ g s

Alias of the reverse direction of antivaryOn_inv_left₀.

theorem AntivaryOn.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) :
AntivaryOn f⁻¹ g sMonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_left₀.

theorem MonovaryOn.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 < g i) :
MonovaryOn f g⁻¹ sAntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_right₀.

theorem AntivaryOn.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 < g i) :
AntivaryOn f g sMonovaryOn f g⁻¹ s

Alias of the reverse direction of monovaryOn_inv_right₀.

theorem MonovaryOn.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 < g i) :
MonovaryOn f g sAntivaryOn f g⁻¹ s

Alias of the reverse direction of antivaryOn_inv_right₀.

theorem AntivaryOn.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hg : is, 0 < g i) :
AntivaryOn f g⁻¹ sMonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_right₀.

theorem MonovaryOn.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) (hg : is, 0 < g i) :
MonovaryOn f g s

Alias of the reverse direction of monovaryOn_inv₀.

theorem MonovaryOn.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) (hg : is, 0 < g i) :
MonovaryOn f g s

Alias of the forward direction of monovaryOn_inv₀.

theorem AntivaryOn.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) (hg : is, 0 < g i) :
AntivaryOn f g s

Alias of the forward direction of antivaryOn_inv₀.

theorem AntivaryOn.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g : ιβ} (hf : is, 0 < f i) (hg : is, 0 < g i) :
AntivaryOn f g s

Alias of the reverse direction of antivaryOn_inv₀.

theorem Monovary.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) :
Antivary f g

Alias of the forward direction of monovary_inv_left₀.

theorem Antivary.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) :
Antivary f g

Alias of the reverse direction of monovary_inv_left₀.

theorem Monovary.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) :
Monovary f g

Alias of the reverse direction of antivary_inv_left₀.

theorem Antivary.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) :
Monovary f g

Alias of the forward direction of antivary_inv_left₀.

theorem Monovary.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : StrongLT 0 g) :
Antivary f g

Alias of the forward direction of monovary_inv_right₀.

theorem Antivary.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : StrongLT 0 g) :
Antivary f g

Alias of the reverse direction of monovary_inv_right₀.

theorem Antivary.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : StrongLT 0 g) :
Monovary f g

Alias of the forward direction of antivary_inv_right₀.

theorem Monovary.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hg : StrongLT 0 g) :
Monovary f g

Alias of the reverse direction of antivary_inv_right₀.

theorem Monovary.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) (hg : StrongLT 0 g) :
Monovary f g

Alias of the reverse direction of monovary_inv₀.

theorem Monovary.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) (hg : StrongLT 0 g) :
Monovary f g

Alias of the forward direction of monovary_inv₀.

theorem Antivary.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) (hg : StrongLT 0 g) :
Antivary f g

Alias of the reverse direction of antivary_inv₀.

theorem Antivary.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g : ιβ} (hf : StrongLT 0 f) (hg : StrongLT 0 g) :
Antivary f g

Alias of the forward direction of antivary_inv₀.

theorem MonovaryOn.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : is, 0 f₁ i) (hf₂ : is, 0 < f₂ i) (h₁ : MonovaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) :
MonovaryOn (f₁ / f₂) g s
theorem AntivaryOn.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : is, 0 f₁ i) (hf₂ : is, 0 < f₂ i) (h₁ : AntivaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) :
AntivaryOn (f₁ / f₂) g s
theorem Monovary.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : 0 f₁) (hf₂ : StrongLT 0 f₂) (h₁ : Monovary f₁ g) (h₂ : Antivary f₂ g) :
Monovary (f₁ / f₂) g
theorem Antivary.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f₁ : ια} {f₂ : ια} {g : ιβ} (hf₁ : 0 f₁) (hf₂ : StrongLT 0 f₂) (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) :
Antivary (f₁ / f₂) g
theorem MonovaryOn.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : is, 0 g₁ i) (hg₂ : is, 0 < g₂ i) (h₁ : MonovaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) :
MonovaryOn f (g₁ / g₂) s
theorem AntivaryOn.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {s : Set ι} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : is, 0 g₁ i) (hg₂ : is, 0 < g₂ i) (h₁ : AntivaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) :
AntivaryOn f (g₁ / g₂) s
theorem Monovary.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : 0 g₁) (hg₂ : StrongLT 0 g₂) (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) :
Monovary f (g₁ / g₂)
theorem Antivary.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {f : ια} {g₁ : ιβ} {g₂ : ιβ} (hg₁ : 0 g₁) (hg₂ : StrongLT 0 g₂) (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) :
Antivary f (g₁ / g₂)

### Rearrangement inequality characterisation #

theorem monovaryOn_iff_forall_smul_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s0 (f j - f i) (g j - g i)
theorem antivaryOn_iff_forall_smul_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s(f j - f i) (g j - g i) 0
theorem monovary_iff_forall_smul_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Monovary f g ∀ (i j : ι), 0 (f j - f i) (g j - g i)
theorem antivary_iff_forall_smul_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Antivary f g ∀ (i j : ι), (f j - f i) (g j - g i) 0
theorem monovaryOn_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i g j + f j g i f i g i + f j g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivaryOn_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i g i + f j g j f i g j + f j g i

Two functions antivary iff the rearrangement inequality holds.

theorem monovary_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Monovary f g ∀ (i j : ι), f i g j + f j g i f i g i + f j g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivary_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Antivary f g ∀ (i j : ι), f i g i + f j g j f i g j + f j g i

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.sub_smul_sub_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s0 (f j - f i) (g j - g i)

Alias of the forward direction of monovaryOn_iff_forall_smul_nonneg.

theorem AntivaryOn.sub_smul_sub_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s(f j - f i) (g j - g i) 0

Alias of the forward direction of antivaryOn_iff_forall_smul_nonpos.

theorem Monovary.sub_smul_sub_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Monovary f g∀ (i j : ι), 0 (f j - f i) (g j - g i)

Alias of the forward direction of monovary_iff_forall_smul_nonneg.

theorem Antivary.sub_smul_sub_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Antivary f g∀ (i j : ι), (f j - f i) (g j - g i) 0

Alias of the forward direction of antivary_iff_forall_smul_nonpos.

theorem Monovary.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Monovary f g∀ (i j : ι), f i g j + f j g i f i g i + f j g j

Alias of the forward direction of monovary_iff_smul_rearrangement.

Two functions monovary iff the rearrangement inequality holds.

theorem Antivary.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} :
Antivary f g∀ (i j : ι), f i g i + f j g j f i g j + f j g i

Alias of the forward direction of antivary_iff_smul_rearrangement.

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i g j + f j g i f i g i + f j g j

Alias of the forward direction of monovaryOn_iff_smul_rearrangement.

Two functions monovary iff the rearrangement inequality holds.

theorem AntivaryOn.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Module α β] [] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i g i + f j g j f i g j + f j g i

Alias of the forward direction of antivaryOn_iff_smul_rearrangement.

Two functions antivary iff the rearrangement inequality holds.

theorem monovaryOn_iff_forall_mul_nonneg {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
MonovaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s0 (f j - f i) * (g j - g i)
theorem antivaryOn_iff_forall_mul_nonpos {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
AntivaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s(f j - f i) * (g j - g i) 0
theorem monovary_iff_forall_mul_nonneg {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Monovary f g ∀ (i j : ι), 0 (f j - f i) * (g j - g i)
theorem antivary_iff_forall_mul_nonpos {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Antivary f g ∀ (i j : ι), (f j - f i) * (g j - g i) 0
theorem monovaryOn_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
MonovaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i * g j + f j * g i f i * g i + f j * g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivaryOn_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
AntivaryOn f g s ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i * g i + f j * g j f i * g j + f j * g i

Two functions antivary iff the rearrangement inequality holds.

theorem monovary_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Monovary f g ∀ (i j : ι), f i * g j + f j * g i f i * g i + f j * g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivary_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Antivary f g ∀ (i j : ι), f i * g i + f j * g j f i * g j + f j * g i

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.sub_mul_sub_nonneg {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
MonovaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s0 (f j - f i) * (g j - g i)

Alias of the forward direction of monovaryOn_iff_forall_mul_nonneg.

theorem AntivaryOn.sub_mul_sub_nonpos {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
AntivaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j s(f j - f i) * (g j - g i) 0

Alias of the forward direction of antivaryOn_iff_forall_mul_nonpos.

theorem Monovary.sub_mul_sub_nonneg {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Monovary f g∀ (i j : ι), 0 (f j - f i) * (g j - g i)

Alias of the forward direction of monovary_iff_forall_mul_nonneg.

theorem Antivary.sub_mul_sub_nonpos {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Antivary f g∀ (i j : ι), (f j - f i) * (g j - g i) 0

Alias of the forward direction of antivary_iff_forall_mul_nonpos.

theorem Monovary.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Monovary f g∀ (i j : ι), f i * g j + f j * g i f i * g i + f j * g j

Alias of the forward direction of monovary_iff_mul_rearrangement.

Two functions monovary iff the rearrangement inequality holds.

theorem Antivary.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} :
Antivary f g∀ (i j : ι), f i * g i + f j * g j f i * g j + f j * g i

Alias of the forward direction of antivary_iff_mul_rearrangement.

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
MonovaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i * g j + f j * g i f i * g i + f j * g j

Alias of the forward direction of monovaryOn_iff_mul_rearrangement.

Two functions monovary iff the rearrangement inequality holds.

theorem AntivaryOn.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} {f : ια} {g : ια} {s : Set ι} :
AntivaryOn f g s∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j sf i * g i + f j * g j f i * g j + f j * g i

Alias of the forward direction of antivaryOn_iff_mul_rearrangement.

Two functions antivary iff the rearrangement inequality holds.