SubadditivityBetter #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: variational simplex subadditivity (`l.subadd.betterer`) #

This file is a finite-carrier candidate/provider implementation for Lemma l.subadd.betterer and its display e.subadd.betterer of ABK26.

for a partition SW of a cube cu_m into (triadic) simplices and a family of piecewise-affine competitors hat-linear_p, hat-D_q satisfying the displayed boundary conditions e.hat.linear.1 and e.hat.D.bc,

  (p,q) . bfA(cu_m; a) (p,q)
    <= sum_{s in SW} (|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)).

Carrier choices #

bfA(U; a) is CoarseGraining's Homogenization.Book.Ch02.coarseBlockMatrix U a, whose defining property Homogenization.Book.Ch02.DoubledMuTheory.doubledMu_eq_coarseBlockMatrix is exactly the paper's e.bigA.def mu(U,P) = 1/2 P . bfA(U) P, with mu(U,P) = doubledMu U a P the paper's e.variational.mu.U.P: the infimum of ⨍_U 1/2 X. bfA X over X ∈ P + L²_pot,0(U) × L²_sol,0(U).
The partition SW is carried by a finite family S : ι → Domain d of subdomains of Q, pairwise disjoint, whose union exhausts Q up to a Lebesgue-null set. Open triadic simplices of a triangulation of cu_m are exactly of this form (an open simplex is an open bounded convex nonempty set, distinct open cells of a triangulation are disjoint, and the union of the closed cells is the cube, so only the faces — a null set — are missed). No simplicial structure is used by the proof and none is assumed. Finite-carrier form. [Fintype ι] restricts this file's statement to finite partitions. The paper's own Whitney partition W(cu_m) and hence its simplicial refinement SW(cu_m) are countably infinite, and the application sums over that infinite family.
The competitor pair is carried at the level of the two fields F = grad hat-linear_p and G = div hat-D_q, through exactly the two displayed boundary properties the paper's proof invokes, F ∈ p + L²_pot,0(cu_m) (e.hat.linear.1) and G ∈ q + L²_sol,0(cu_m) (e.hat.D.bc), together with the paper's e.hat.linear.2, that these fields are constant on each element of the partition, with constant values Fc i and Gc i — the paper's grad hat-linear_p (s) and div hat-D_q (s). This is weaker than the paper's hypotheses (it forgets that the fields come from a linear family of piecewise affine potentials, which the paper's proof never uses), so the theorem below implies the paper's statement.