Let (M,F) be a Finsler disk that isometrically fills its boundary of length 2L. We may assume that M is the standard round disk in ℝ², and the Finsler metric F:TM = M × ℝ² → [0,+∞) is smooth and strongly convex.^[5] The Holmes–Thompson area of the filling can be computed by the formula

${\displaystyle \operatorname {Area} _{\mathrm {HT} }(M,F)={\frac {1}{\pi }}\iint _{M}|B_{x}^{*}|\,\mathrm {d} x_{0}\,\mathrm {d} x_{1}}$

where for each point ${\displaystyle x\in M}$, the set ${\displaystyle B_{x}^{*}\subseteq \mathbb {R} ^{2}}$ is the dual unit ball of the norm ${\displaystyle F_{x}}$ (the unit ball of the dual norm ${\displaystyle F_{x}^{*}}$), and ${\displaystyle |B_{x}^{*}|}$ is its usual area as a subset of ${\displaystyle \mathbb {R} ^{2}}$.

Choose a collection ${\displaystyle P=(p_{i})_{0\leq i<n}\subseteq \partial M}$ of boundary points, listed in counterclockwise order. For each point ${\displaystyle p_{i}}$, we define on M the scalar function ${\displaystyle f_{i}(x)=\mathrm {dist} _{F}(p_{i},x)}$. These functions have the following properties:

• Each function ${\displaystyle f_{i}:M\to \mathbb {R} }$ is Lipschitz on M and therefore (by Rademacher's theorem) differentiable at almost every point ${\displaystyle x\in M}$.
• If ${\displaystyle f_{i}}$ is differentiable at an interior point ${\displaystyle x\in M^{\circ }}$, then there is a unique shortest curve from ${\displaystyle p_{i}}$ to x (parametrized with unit speed), that arrives at x with a speed ${\displaystyle v_{i}}$. The differential ${\displaystyle \mathrm {d} _{x}f_{i}}$ has norm 1 and is the unique covector ${\displaystyle \varphi \in B_{x}^{*}}$ such that ${\displaystyle \varphi (v_{i})=F_{x}(v_{i})}$.
• In each point ${\displaystyle x\in M^{\circ }}$ where all the functions ${\displaystyle f_{i}}$ are differentiable, the covectors ${\displaystyle \mathrm {d} f_{i}}$ are distinct and placed in counterclockwise order on the dual unit sphere ${\displaystyle \partial B_{x}^{*}}$. Indeed, they must be distinct because different geodesics cannot arrive at ${\displaystyle x}$ with the same speed. Also, if three of these covectors ${\displaystyle \mathrm {d} _{x}f_{i},\mathrm {d} _{x}f_{j},\mathrm {d} _{x}f_{k}}$ (for some ${\displaystyle 0\leq i<j<k<n}$) appeared in inverted order, then two of the three shortest curves from the points ${\displaystyle p_{i},p_{j},p_{k}\in \partial M}$ to ${\displaystyle x}$ would cross each other, which is not possible.

In summary, for almost every interior point ${\displaystyle x\in M^{\circ }}$, the covectors ${\displaystyle \mathrm {d} _{x}f_{i}}$ are vertices, listed in counterclockwise order, of a convex polygon inscribed in the dual unit ball ${\displaystyle B_{x}^{*}}$. The area of this polygon is ${\displaystyle \sum _{i}{\frac {1}{2}}\mathrm {d} _{x}f_{i}\wedge \mathrm {d} _{x}f_{i+1}}$ (where the index i + 1 is computed modulo n). Therefore we have a lower bound

${\displaystyle c_{P}:=\int _{M}\sum _{i}{\frac {1}{2}}\mathrm {d} f_{i}\wedge \mathrm {d} f_{i+1}\leq \pi \,\operatorname {Area} _{\mathrm {HT} }(M,F),}$

for the area of the filling. If we define the 1-form ${\displaystyle \theta _{P}=\sum _{i}{\frac {1}{2}}f_{i}\,\mathrm {d} f_{i+1}}$, then we can rewrite this lower bound using the Stokes formula as

${\displaystyle c_{P}=\int _{M}\mathrm {d} \theta _{P}=\int _{\partial M}\theta _{P}=\dots =2L^{2}-\sum _{i}\delta _{i}^{2}\ {\xrightarrow {P\ {\text{dense}}}}\ 2L^{2}}$.

The boundary integral that appears here is defined in terms of the distance functions ${\displaystyle f_{i}}$ restricted to the boundary, which do not depend on the isometric filling. The result of the integral therefore depends only on the placement of the points ${\displaystyle p_{i}}$ on the circle of length 2L. We omitted the computation, and expressed the result in terms of the lengths ${\displaystyle \delta _{i}}$ of each counterclockwise boundary arc from a point ${\displaystyle p_{i}}$ to the following point ${\displaystyle p_{i+1}}$. The computation is valid only if ${\displaystyle \delta _{i}<{\frac {L}{2}}}$.

In summary, our lower bound for the area of the Finsler isometric filling converges to ${\displaystyle {\frac {1}{\pi }}2L^{2}}$ as the collection ${\displaystyle P\subseteq \partial M}$ is densified. This implies that

${\displaystyle \operatorname {Area} _{\mathrm {HT} }(M,F)\geq {\frac {1}{\pi }}\,2L^{2}=\operatorname {Area} ({\text{hemisphere}})}$,

as we had to prove.