Finite products under a valuative relation

For a valuative relation on a commutative semiring, a finite product has positive value exactly when every factor does, and finite products are monotone. When the other factors have positive value, replacing one factor of a finite product moves the value of the product in the same direction as the value of that factor.

Main results

• TauCeti.ValuativeRel.zero_vlt_prod_iff : 0 <ᵥ ∏ i ∈ s, f i exactly when 0 <ᵥ f i for every i ∈ s.
• TauCeti.ValuativeRel.prod_vle_prod : finite products are monotone for ≤ᵥ.
• TauCeti.ValuativeRel.prod_update_vle_prod_iff and TauCeti.ValuativeRel.prod_vle_prod_update_iff : if the factors other than f j have positive value, replacing f j by x compares with the original product exactly as x compares with f j.
• TauCeti.ValuativeRel.prod_vle_prod_update : replacing a factor by an element of at least its value does not decrease the value of the product.

@[simp]

theorem TauCeti.ValuativeRel.zero_vlt_prod_iff {R : Type u_1} {ι : Type u_2} [CommSemiring R] [ValuativeRel R] {s : Finset ι} {f : ι → R} : 0 <ᵥ ∏ i ∈ s, f i ↔ ∀ i ∈ s, 0 <ᵥ f i

A finite product has positive value exactly when every factor does. This extends ValuativeRel.zero_vlt_mul from two factors to finite products, and adds the converse.

theorem TauCeti.ValuativeRel.prod_vle_prod {R : Type u_1} {ι : Type u_2} [CommSemiring R] [ValuativeRel R] {s : Finset ι} {f g : ι → R} (h : ∀ i ∈ s, f i ≤ᵥ g i) : ∏ i ∈ s, f i ≤ᵥ ∏ i ∈ s, g i

Finite products are monotone for a valuative relation. This is the analogue of Finset.prod_le_prod, and extends ValuativeRel.mul_vle_mul from two factors to finite products.

@[simp]

theorem TauCeti.ValuativeRel.prod_update_vle_prod_iff {R : Type u_1} {ι : Type u_2} [CommSemiring R] [ValuativeRel R] {s : Finset ι} {f : ι → R} [DecidableEq ι] {j : ι} {x : R} (hf : ∀ i ∈ s, i ≠ j → 0 <ᵥ f i) (hj : j ∈ s) : ∏ i ∈ s, Function.update f j x i ≤ᵥ ∏ i ∈ s, f i ↔ x ≤ᵥ f j

If the factors of a finite product other than f j have positive value, replacing f j by x does not increase the value of the product exactly when x ≤ᵥ f j. For the opposite comparison see prod_vle_prod_update_iff.

@[simp]

theorem TauCeti.ValuativeRel.prod_vle_prod_update_iff {R : Type u_1} {ι : Type u_2} [CommSemiring R] [ValuativeRel R] {s : Finset ι} {f : ι → R} [DecidableEq ι] {j : ι} {x : R} (hf : ∀ i ∈ s, i ≠ j → 0 <ᵥ f i) (hj : j ∈ s) : ∏ i ∈ s, f i ≤ᵥ ∏ i ∈ s, Function.update f j x i ↔ f j ≤ᵥ x

If the factors of a finite product other than f j have positive value, replacing f j by x does not decrease the value of the product exactly when f j ≤ᵥ x. Without the positivity hypothesis only the reverse implication holds; see prod_vle_prod_update. For the opposite comparison see prod_update_vle_prod_iff.

theorem TauCeti.ValuativeRel.prod_vle_prod_update {R : Type u_1} {ι : Type u_2} [CommSemiring R] [ValuativeRel R] {s : Finset ι} {f : ι → R} [DecidableEq ι] {j : ι} {x : R} (h : f j ≤ᵥ x) : ∏ i ∈ s, f i ≤ᵥ ∏ i ∈ s, Function.update f j x i

Replacing a factor of a finite product by an element of at least its value does not decrease the value of the product. Unlike prod_vle_prod_update_iff, no positivity hypothesis is needed.