Lemma 3 — weighted ratio bound and equality case

Proved

FlagshipMEA.Monopoly.lemma_3

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

marketing-effortp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1product-lineratio-inequality

Let $a_i\geq0$ , $b_i>0$ , and $m_i\geq0$ for a nonempty finite index set, with positive total weight $\sum_i m_i>0$ . Choose $k$ attaining the largest component ratio $a_i/b_i$ . Lemma 3 states

\frac{\sum_i m_i a_i}{\sum_i m_i b_i}\leq\frac{a_k}{b_k}=\max_i\frac{a_i}{b_i},

with equality precisely when $m_i=0$ for every $i$ that does not attain the maximum. The equality condition identifies which products may receive effort in a revenue maximizing allocation.

Formalization Note The positive total weight excludes the undefined zero over zero ratio at the all-zero allocation. A nonempty product set makes the maximum attainable.

Preamble

import Mathlib

Formal statement

namespace FlagshipMEA.Monopoly

/-- Lemma 3 (p. 40): the weighted ratio is bounded by its largest component ratio,
with equality exactly when all positive weights are on maximizers. -/
theorem lemma_3 {n : ℕ} (hn : 0 < n) (a b m : Fin n → ℝ)
    (ha : ∀ i, 0 ≤ a i) (hb : ∀ i, 0 < b i) (hm : ∀ i, 0 ≤ m i)
    (hM : 0 < ∑ i, m i) :
    ∃ k : Fin n,
      (∀ i, a i / b i ≤ a k / b k) ∧
      (∑ i, m i * a i) / (∑ i, m i * b i) ≤ a k / b k ∧
      ((∑ i, m i * a i) / (∑ i, m i * b i) = a k / b k ↔
        ∀ i, m i ≠ 0 → a i / b i = a k / b k) := by sorry

end FlagshipMEA.Monopoly

Source

He, Ke & Zhang, A Model of Product Line Marketing, SSRN 3631879 (version of August 2021), p. 40 (PDF 42), Lemma 3, (C–1)

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph