Weil's Haar measure construction from below Weil's construction of a Haar measure on a locally compact group rests on approximating a function from above by sums of translates of another function.
I would need to know something similar for an approximation from below.
Actually, I need something stronger:
Let $G$ be a locally compact group and let $C_c^+(G)$ be the set of all compactly supported functions $f$ on $G$ with $f\ne 0$ and $f(x)\ge 0$ for all $x\in G$.
For $\phi,f\in C_c^+(G)$ let
$(\phi,f)$ be the infimum over all sums $\sum_{j=1}^nc_j$, where $c_j>0$ such that there exist $s_1,\dots, s_n\in G$ with
$$
\phi(x)\le\sum_{j=1}^nc_j\ f(s_jx),\quad \forall\ x\in G.
$$
Likewise, let $[\phi,f]$ be the supremum over all $\sum_{j=1}^nc_j$ such that there exist $s_1,\dots, s_n\in G$ with
$$
\phi(x)\ge\sum_{j=1}^nc_j\ f(s_jx),\quad \forall\ x\in G.
$$
Then Weil's proof of the existence and uniqueness of the Haar measure implies that for every net $(f_\alpha)_{\alpha\in A}$ with the properties
$$
\alpha\le\beta\quad\Rightarrow\quad \mathrm{supp} (f_\alpha)\supset \mathrm{supp} (f_\beta)
$$
and
$$
\bigcap_{\alpha\in A}\mathrm{supp}(f_\alpha)=\{1\},
$$
and any two $\phi,\psi\in C_c^+(G)$,
the quotient
$
\frac{(\phi,f_\alpha)}{(\psi,f_\alpha)}
$
converges to $\frac{\int_G\phi\,d\mu}{\int_G\psi\,d\mu}$.
My question is this: For given $\phi\in C_c^+(G)$, does the quotient
$$
\frac{[\phi,f_\alpha]}{(\phi,f_\alpha)}
$$
converge to 1?
In case this is not true for any net as above, does there exist one net with this property?
It would be enough to assume that $G$ is first countable, so instead of nets you may as well use sequences.
 A: The answer is Yes, provided that for every $\alpha$ and every $x\in G$, $f_\alpha(x^{-1})=f_\alpha(x)$.
Since we already completed the construction of the Haar measure we can actually use it in our proof. I suppose that one can show this also elementarily, but why bother?
Choose a left Haar measure on $G$.
Let me assume, as the expression in consideration is homogeneous, that the $L^1(G)$ norm of all $f_\alpha,\phi$ is 1. 
The answer will follow from the claims $\lim[\phi,f_\alpha]=1$ and $\lim(\phi,f_\alpha)= 1$.
I will prove the first claim, the second being similar.
Let me first note that for every $\alpha$, $\phi(x)\leq \sum c_jf_\alpha(s_jx)$ implies by taking integrals that $1\leq \sum c_j$. Therefore $[\phi,f_\alpha]\geq 1$. We are left to show that for every $m>1$ there exists $\alpha_0$ such that for every $\alpha\geq \alpha_0$, $[\phi,f_\alpha] \leq m$.
Fix $m>1$.
Choose a compactly supported $[0,1]$-valued continuous function $\psi$ which is 1 on the support of $\phi$. Denote $\epsilon=(m-1)/\|\psi\|_1$.
Set $\phi'=\phi+\epsilon \psi$ and note that $\|\phi'\|_1=m$.
Note that the net $(f_\alpha)$ forms an approximate identity and therefore $\phi'*f_\alpha \to \phi'$ in the sup norm. See e.g: Folland, "A course in Abstract Harmonic Analysis" (2.42) - this is why I needed the assumption $f_\alpha(x^{-1})=f_\alpha(x)$.
Find $\alpha_0$ such that for every $\alpha\geq \alpha_0$, $\|\phi'*f_\alpha- \phi'\|_\infty <\epsilon/2$.
We now fix $\alpha\geq\alpha_0$ and denote for convenience $f=f_\alpha$.
We are left to show that $[\phi,f]\leq m$.
Let $K$ be the support of $\phi'$ and $K'$ be the support of $\phi'*f$.
Let $Q$ be the convex set of positive measures on $G$ with total mass $m$ and support contained in $K$
and let $Q'$ be the set of finitely supported measures in $Q$. 
Identify $Q$ with a subset of $C(K)^*$ and note that $Q'$ is weak* dense in $Q$.
Observe that $Q*f$ is a subset of $C(K')$.
I claim that $Q'*f$ is weakly dense in $Q'*f$ within $C(K')$.
Assume not. 
Then there exists $\nu\in Q$ such that $\nu*f$ is not in the weak closure of $Q'*f$.
Find a (signed) measure $\lambda$ which separates $\nu* f$ from $Q'*f$ in $C(K')$
and observe that the continuous function $\lambda*\check{f}|_K$ separates $\nu$ from $Q'$ in $C(K)^*$. But this is absurd, as $Q'$ is weak*-dense in $Q$.
This proves the claim.
Recall that for convex sets the weak closure is the same as the norm closure.
We deduce that $Q'*f$ is dense in $Q*f$ wrt the sup norm of $C(K')$.
Observe that $\phi'\in Q$. Thus $\phi'*f\in Q*f$
and there exists a finitely supported measure $\mu\in Q'$ such that 
$\|\mu*f-\phi'*f\|_\infty<\epsilon/2$.
It follows that $\|\mu*f-\phi'\|_\infty<\epsilon$.
Since $\phi'-\phi=\epsilon\psi$ equals $\epsilon$ on the support of $\phi'$ and $\mu*f\geq 0$ everywhere we get that $\mu*f\geq \phi$ everywhere.
Writing $\mu=\sum_{j=1}^n c_j\delta_{s_j}$ we get that for every $x\in G$, $\sum c_jf_\alpha(s_jx) \geq \phi(x)$.
Thus $[\phi,f]\leq \sum c_j=m$.
