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. The Mathlib version currently used is v4.26.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

Login to submit a solution.