Resistive Inequality

Given natural numbers $m$ and $n$, let $a$ be a positive function from $\{0, \dots, m - 1\} \times \{0, \dots n - 1\}$ to the reals. Prove that $$\sum_{i = 0}^{m - 1} \frac{1}{\sum_{j = 0}^{n - 1} \frac{1}{a(i, j)}} \le \frac{1}{\sum_{j = 0}^{n - 1} \frac{1}{\sum_{i = 0}^{m - 1} a(i, j)}}.$$

_Replace_ `sorry` _in the template below with your solution. Mathlib version used by the checker is v4.28.0_.

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
open Finset

theorem solution (m n : ℕ) (a : ℕ → ℕ → ℝ) (h_pos : ∀ i < m, ∀ j < n, 0 < a i j) :
    ∑ i ∈ range m, 1 / (∑ j ∈ range n, 1 / a i j) ≤
    1 / (∑ j ∈ range n, 1 / (∑ i ∈ range m, a i j)) := sorry

Submit Solution

Login to submit a solution.

Recent Submissions