Comparing functions by a maximal coordinate ratio

On a finite nonempty type, every function lies below a scalar multiple of a strictly positive function, with equality at a coordinate where the ratio is maximal.

Main results

• TauCeti.exists_le_smul_of_pos: domination by a scalar multiple of a positive function, with a coordinate where equality holds.

theorem TauCeti.exists_le_smul_of_pos {n : Type u_1} {K : Type u_2} [Finite n] [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {v : n → K} (hv : ∀ (i : n), 0 < v i) (j : n) (y : n → K) : ∃ (i : n), y ≤ (y i / v i) • v ∧ y i = y i / v i * v i

Comparing coordinate ratios gives a scalar multiple lying above a vector and touching it.