SubadditiveDecomposition #

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

The conditional trimming kernel for the subadditive decomposition #

It does not by itself realize or close that step of p.bfA.multiscalebound: its main theorem keeps the competitor fields and their structural clauses as explicit premises. The target display is e.sum-of-a-decomp of ABK26:

| 𝐀hom_{n-1}^{-1/2} P . 𝐀_L(□_n) 𝐀hom_{n-1}^{-1/2} P |
  ≤ ∑_{𝔰 ∈ 𝒮𝒲(□_n)} (|𝔰|/|□_n|) | 𝐀_L^{1/2}(𝔰) 𝐀hom_{n-1}^{-1/2} P |² 1_{¬𝓑(𝔰)}
  + ∑_{𝔰 ∈ 𝒮𝒲(□_n)} (|𝔰|/|□_n|)
        | 𝐀_L^{1/2}(𝔰) 𝐀hom_{n-1}^{-1/2} (∇ℓ̂_p(𝔰), (∇·D̂_q)(𝔰)) |²
        1_{¬𝓑(𝔰)} 1_{𝔰 ∈ 𝒩(ℐ)} .

The route (/: varying slope, never `csInf_le`) #

The engine is the per-cell varying-slope gluing of l.subadd.betterer, proved in Provider/Whitney/SubadditivityCountable.lean (ofReal_bfA_quadratic_le_simplex_weighted_tsum): exact cell minimizers at the cell's own slope (∇ℓ̂_p(𝔰), ∇·D̂_q(𝔰)) are pasted into a single admissible competitor by zero-extension of their L²_pot,0/L²_sol,0 corrections. Every term of the right-hand side below is therefore a genuine coarse-grained 𝐀_L(𝔰) quadratic form, which is what bounds.

This module supplies the two things the gluing lemma still needs at the manuscript's own partition, and then performs the manuscript's trimming:

the cells of SW(□_m) as a countable family of Chapter 2 domains covering the root cube up to a null set (SimplexDomains.lean);
the split of the resulting single sum into the two printed sums, using the two structural clauses of e.hat.linear.properties.

The load is a general block vector #

The manuscript's left-hand side is loaded at 𝐀hom_{n-1}^{-1/2} P and every right-hand cell term at 𝐀hom_{n-1}^{-1/2} P̂(𝔰). By e.homs.defs.U.diag ( an verified node) 𝐀hom_{n-1} is block diagonal with scalar blocks, 𝐀hom_{n-1}^{-1/2} (p,q) = (σ_{n-1}^{-1/2} p, σ_{n-1}^{1/2} q), and the two legs are rescaled independently. Since L²_pot,0 and L²_sol,0 are linear spaces, the frame commutes with every hypothesis and with every conclusion below. The theorem is therefore stated at a general load (p, q) and a general competitor pair; the manuscript's display is the instantiation

p ↦ σ_{n-1}^{-1/2} p ,  q ↦ σ_{n-1}^{1/2} q ,
F ↦ σ_{n-1}^{-1/2} ∇ℓ̂_p ,  G ↦ σ_{n-1}^{1/2} ∇·D̂_q .

This is strictly more general than the printed display; nothing is assumed about 𝐀hom.

The competitor is an explicit local interface #

The theorem in this low-level module is deliberately generic in the competitor pair. It therefore carries the relevant conclusions of l.piecewise.affine.approx as explicit hypotheses, in the exact shape e.hat.linear.properties delivers and at the same carrier at which l.subadd.betterer already reads it (the two fields F = ∇ℓ̂_p and G = ∇·D̂_q, see SubadditivityBetter.lean):

hF, hG: e.hat.linear.1 and e.hat.D.bc, each read at its label and content;
hFc, hGc: e.hat.linear.2, the subordination of the competitor to SW(□_m), with Fc/Gc the manuscript's own notation ∇ℓ̂_p(𝔰), ∇·D̂_q(𝔰);
hbadF, hbadG: clause 1 of e.hat.linear.properties, ∇ℓ̂_p = 0 in every □ ∈ ℐ;
hoffF, hoffG: clause 3 of e.hat.linear.properties ((clause 3; the cases-end line asserts nothing —, format)), ∇ℓ̂_p = p in every 𝔰 ∈ SW(□_m) ∖ 𝒩(ℐ).

Clauses 1 and 3 are printed for the potential leg only. Their algebraic transfer to the solenoidal leg is recorded below as hatDDivergenceValue_zero and hatDDivergenceValue_id, but the generic theorem sum_of_a_decomp still takes hbadG and hoffG explicitly because its abstract field G is not definitionally hatDDivergenceValue. The concrete superposed route later discharges these premises. Clause 2 of e.hat.linear.properties (the collar gradient bound) is not used by this node — it is spent by #conclusion through r.gradient.bound.simplified — and is not assumed.

The node's inputs, and where each is consumed #

d.whitney.bad-set.definitions and d.simplex.partition are consumed directly: simplexPartition, whitneyPartition, badFamily, whitneyNeighborhood, and the exactness/disjointness theorems of the proved Whitney layer.
l.subadd.betterer is consumed directly, in its countable [0,∞] form.
l.bad.clusters.geometry is not consumed by sum_of_a_decomp itself. In the manuscript it checks the hypotheses of l.piecewise.affine.approx ("each 𝒞_j satisfies the hypotheses of Lemma."). Its proved geometry feeds the downstream affine/superposition construction, which now supplies the concrete cellwise clauses; none of that downstream discharge is credited to this conditional kernel.

Scope notes #

No face-to-face or simplicial-complex property of SW(□_m) is used: the gluing pastes measurable L² corrections supported in single cells, never continuous ones, so no cross-cell compatibility is needed. The two-layer common-coarse property --- that cells of adjacent layers sit in a common coarse simplex --- is an obligation of l.piecewise.affine.approx, not of this node, and nothing below needs it.
concern Steps 3 of p.bfA.multiscalebound; they touch the consumption of this display, not its derivation, and nothing below depends on them.

References #

ABK26, (e.sum-of-a-decomp), (e.hat.linear.1, e.hatdq, e.hat.D.bc), (l.piecewise.affine.approx), (e.homs.defs.U.diag).

`e.hatdq`: the solenoidal leg of the two structural clauses #

(D̂_q)_{ij} = (d-1)^{-1} (q_j ℓ̂_{e_i} - q_i ℓ̂_{e_j}) and (∇ · A)_j = ∑_i ∂_{x_i} A_{ij} (footnote), so on a cell where every ∇ℓ̂_{e_k} is the constant vector A k,

(∇ · D̂_q)_j = (d-1)^{-1} ∑_i (q_j (A i) i - q_i (A j) i).

The two clauses of e.hat.linear.properties used by this node fix A completely — A = 0 inside a bad cube, A k = e_k off the collar — so the solenoidal leg is determined, and no separate hypothesis about ∇ · D̂_q is needed.

SubadditiveDecomposition #

The conditional trimming kernel for the subadditive decomposition #

The route (/: varying slope, never csInf_le) #

The load is a general block vector #

The competitor is an explicit local interface #

The node's inputs, and where each is consumed #

Scope notes #

References #

e.hatdq: the solenoidal leg of the two structural clauses #

The Whitney cube containing a cell of SW(□_m) #

The two indicators of e.sum-of-a-decomp #

SW(□_m) as an admissible dissection #

The conditional trimming statement #

The route (/: varying slope, never `csInf_le`) #

`e.hatdq`: the solenoidal leg of the two structural clauses #

The Whitney cube containing a cell of `SW(□_m)` #

The two indicators of `e.sum-of-a-decomp` #

`SW(□_m)` as an admissible dissection #