Lean declarations

theorem Loomis.lamB.aux_gt_iff_gt EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
Characterisation: `lamB.aux A B x > c` iff every column ratio exceeds `c`.
```
theorem lamB.aux_gt_iff_gt (A B : I → J → ℝ) (c : ℝ) (x : stdSimplex ℝ I) :
    c < lamB.aux A B x ↔ ∀ j, c < colRatio A B x j
```
theorem Loomis.muB.aux_lt_iff_lt EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
Characterisation: `muB.aux A B y < c` iff every row ratio is below `c`.
```
theorem muB.aux_lt_iff_lt (A B : I → J → ℝ) (c : ℝ) (y : stdSimplex ℝ J) :
    muB.aux A B y < c ↔ ∀ i, rowRatio A B y i < c
```
theorem Loomis.colRatio.continuous EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
Each column ratio `(xA)_j / (xB)_j` is continuous on `Δ(I)`.
```
theorem colRatio.continuous {A B : I → J → ℝ} (hB : IsPositive B) (j : J) :
    Continuous (fun x : stdSimplex ℝ I => colRatio A B x j)
```

theorem Loomis.rowRatio.continuous EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis

Each row ratio `(Ay)_i / (By)_i` is continuous on `Δ(J)`.

theorem rowRatio.continuous {A B : I → J → ℝ} (hB : IsPositive B) (i : I) :
    Continuous (fun y : stdSimplex ℝ J => rowRatio A B y i)

theorem Loomis.lamB.aux.continuous EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
`lamB.aux A B` is continuous on the simplex.
```
theorem lamB.aux.continuous {A B : I → J → ℝ} (hB : IsPositive B) :
    Continuous (lamB.aux A B)
```
theorem Loomis.muB.aux.continuous EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
`muB.aux A B` is continuous on the simplex.
```
theorem muB.aux.continuous {A B : I → J → ℝ} (hB : IsPositive B) :
    Continuous (muB.aux A B)
```

theorem Loomis.lamB.aux.bddAbove EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis

theorem lamB.aux.bddAbove {A B : I → J → ℝ} (hB : IsPositive B) :
    ∃ C, ∀ x, lamB.aux A B x ≤ C

theorem Loomis.muB.aux.bddBelow EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
`muB.aux A B` is bounded below on the simplex.
```
theorem muB.aux.bddBelow {A B : I → J → ℝ} (hB : IsPositive B) :
    ∃ C, ∀ y, C ≤ muB.aux A B y
```
theorem Loomis.lamB.aux.le_lamB0 EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
Every `lamB.aux` value is bounded by the supremum `lamB0`.
```
theorem lamB.aux.le_lamB0 {A B : I → J → ℝ} (hB : IsPositive B)
    (x : stdSimplex ℝ I) :
    lamB.aux A B x ≤ lamB0 A B
```
theorem Loomis.muB.aux.ge_muB0 EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis
Every `muB.aux` value dominates the infimum `muB0`.
```
theorem muB.aux.ge_muB0 {A B : I → J → ℝ} (hB : IsPositive B)
    (y : stdSimplex ℝ J) :
    muB0 A B ≤ muB.aux A B y
```

theorem Loomis.exists_xx_lamB0 EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis

theorem exists_xx_lamB0 (A B : I → J → ℝ) (hB : IsPositive B) :
    ∃ xx : stdSimplex ℝ I, ∀ j, lamB0 A B * xB B xx j ≤ xA A xx j

theorem Loomis.exists_yy_muB0 EconCSLib @ cef01c7, EconCSLib.Math.Minimax.Loomis

theorem exists_yy_muB0 (A B : I → J → ℝ) (hB : IsPositive B) :
    ∃ yy : stdSimplex ℝ J, ∀ i, Ay A yy i ≤ muB0 A B * By B yy i

Modules: EconCSLib.Math.Minimax.Loomis

Existence of Loomis Optimisers

Compactness and continuity step for the Loomis induction (Direct Induction Proof Of Loomis Theorem): the Loomis ratios are continuous on the simplices, and their extrema are attained.

Setup

Fix $A, B \colon I \times J \to \mathbb{R}$ with $B$ entrywise positive (see Positive Aggregates xB and By). Define $$ \lambda_\mathrm{aux}(x) = \inf_{j \in J} \frac{(xA)_j}{(xB)_j}, \qquad \mu_\mathrm{aux}(y) = \sup_{i \in I} \frac{(Ay)_i}{(By)_i}, $$ and $$ \lambda_0 = \sup_{x \in \Delta(I)} \lambda_\mathrm{aux}(x), \qquad \mu_0 = \inf_{y \in \Delta(J)} \mu_\mathrm{aux}(y). $$

Statement

(i) Continuity. The maps $\lambda_\mathrm{aux} \colon \Delta(I) \to \mathbb{R}$ and $\mu_\mathrm{aux} \colon \Delta(J) \to \mathbb{R}$ are continuous.

(ii) Boundedness. $\lambda_\mathrm{aux}$ is bounded above and $\mu_\mathrm{aux}$ is bounded below on their respective simplices.

(iii) Attainment. There exist $x_0 \in \Delta(I)$ and $y_0 \in \Delta(J)$ such that $\lambda_\mathrm{aux}(x_0) = \lambda_0$ and $\mu_\mathrm{aux}(y_0) = \mu_0$. Equivalently, for every $j \in J$ and every $i \in I$, $$ (x_0 A)_j \ge \lambda_0\,(x_0 B)_j, \qquad (A y_0)_i \le \mu_0\,(B y_0)_i. $$

Proof

(i) Each coordinate $x \mapsto (xA)_j$ and $x \mapsto (xB)_j$ is a continuous linear functional on $\Delta(I)$. Their quotient is continuous because the denominator is strictly positive (Positive Aggregates xB and By). The finite infimum of continuous functions over the finite set $J$ is continuous. The argument for $\mu_\mathrm{aux}$ is dual.

(ii) Each ratio $(xA)_j / (xB)_j$ is bounded above by the obvious extreme $M_A / m_B$, where $M_A := \max_{i, j} A_{ij}$ and $m_B := \min_{i, j} B_{ij}

0$. So $\lambda_\mathrm{aux} \le M_A / m_B$. Symmetrically, $\mu_\mathrm{aux} \ge m_A / M_B$ where $m_A := \min_{i, j} A_{ij}$ and $M_B := \max_{i, j} B_{ij}$.

(iii) $\Delta(I)$ is compact in $\mathbb{R}^{|I|}$, and the continuous function $\lambda_\mathrm{aux}$ attains its supremum on a compact set (extreme-value theorem). Let $x_0$ be a maximiser; then $\lambda_\mathrm{aux}(x_0) = \lambda_0$, which by definition of the infimum-over-$j$ gives $(x_0 A)_j / (x_0 B)_j \ge \lambda_0$ for every $j$, i.e. $(x_0 A)_j \ge \lambda_0 (x_0 B)_j$ (multiplying by the strictly positive $(x_0 B)_j$). The $\mu_0$ side is dual.

The compact/continuous building blocks (Continuity on the Real Standard Simplex and Pointwise Bounds Are Simplex Bounds) live in the core simplex layer; this lemma extends the $B = \mathbf{1}$ case (Existence of Optimal Mixed Strategies (Loomis Foundations)) to general positive $B$ by composing with positive division. $\square$

References

[MFoGT, Section 2.5] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Compactness step for the Loomis ratios.

Existence of Loomis Optimisers

Setup

Statement

References

Used by

Also in