SubadditivityCountable #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: variational simplex subadditivity over a countable dissection #
This file provides a countable-carrier candidate implementation for Lemma
l.subadd.betterer and its display e.subadd.betterer of ABK26 by removing the
finiteness restriction of
Algsuperdiff.Section3.Provider.Whitney.bfA_quadratic_le_simplex_weighted_sum.
The paper's own Whitney partition W(cu_m), hence its simplicial refinement
SW(cu_m), is countably infinite, and the consumer e.sum-of-a-decomp sums
over that infinite family.
ENNReal.ofReal ((p,q) . bfA(cu_m; a) (p,q))
<= sum'_{s in SW} ENNReal.ofReal ((|s| / |cu_m|)
(grad hat-linear_p (s), div hat-D_q (s))
. bfA(s; a) (grad hat-linear_p (s), div hat-D_q (s))).
No summability hypothesis is carried: when the series diverges the statement is
trivially true, exactly as the tex inequality is. A real-valued corollary
carrying an explicit Summable binder is provided separately as a convenience
for consumers that have already established summability. The [0,∞] theorem
is the principal countable provider here, but neither declaration is an exact
frozen node export.
Proof route #
The paper's one-line variational comparison is proved locally by gluing exact cell
minimizers into a single competitor for Q. With infinitely many cells only
finitely many corrections can be inserted at a time, so the glue is performed
over an arbitrary J : Finset ι and leaves the remainder
|Q|^{-1} ( int_Q E(F,G) - sum_{i in J} int_{S i} E(F,G) )
where E(F,G) is the block energy density of the competitor pair itself — an
integrable function on Q because F - p in L^2_pot,0(Q) and G - q in L^2_sol,0(Q).
Integrability and sign of the block energy density #
The block energy density of a block-L² doubled field is integrable on the
domain. This is the ellipticity-free route already used for the cell energies
in SubadditivityBetter.lean: pass to CoarseGraining's pointwise elliptic
representative of the coefficient field, which is a.e. equal to the given one.
The doubled block energy density is a.e. nonnegative on the domain, because the coefficient field is a.e. elliptic there.
Every admissible energy value is nonnegative.
mu(U,P;a) >= 0.
The glue over a finite subfamily, with remainder #
Variational subadditivity over a finite subfamily of the dissection.
Gluing the exact cell minimizers of the cells indexed by J into the
competitor pair (F, G) produces an admissible competitor for Q whose energy
is the weighted sum of the cell energies plus the energy of (F, G) on the part
of Q not covered by J. The remainder below is exactly
|Q|^{-1} int_{Q \ Union_{i in J} S i} E(F,G).
No covering hypothesis is needed here, and ι is unrestricted.
The mu-form over a countable dissection #
Variational simplex subadditivity over a countable dissection, mu-form.
mu(Q, (p,q)) ≤ ∑' (|S i| / |Q|) mu(S i, (Fc i, Gc i)) in [0, ∞], whenever
the countably many cells S i tile Q up to a null set and the competitor pair
(F, G) is admissible for (p,q) on Q and is constant, with values
(Fc i, Gc i), on each cell.
The countable-carrier provider statement #
Countable-carrier provider for l.subadd.betterer, display
e.subadd.betterer.
For a countable partition of the cube Q into cells S i and a
potential-solenoidal competitor pair (F, G) ∈ (p + L²_pot,0(Q)) × (q + L²_sol,0(Q)) which is constant on each cell with values (Fc i, Gc i),
(p,q) . bfA(Q; a) (p,q) ≤ ∑' (|S i| / |Q|) (Fc i, Gc i) . bfA(S i; a) (Fc i, Gc i)
as an inequality in [0, ∞].