CollarLayerEnvelopeG

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

The collar layer envelope of the G-leg (∇·D̂_q)

CollarLayerEnvelope proves a local F-leg estimate associated with l.piecewise.affine.approx: on every cell of every layer-k Whitney cube

|∇ℓ̂_p − p|²  ≤  (648 d)² · 3^{2 b (k + h_k)} · |p|² .

This module proves the corresponding local p ↦ q estimate, the G-leg: the constant value on the cell of the divergence ∇·D̂_q of the antisymmetric matrix D̂_q of e.hatdq, at the same constant 648 d, the same exponent 3^{2 b (k + h_k)} and |q|² on the right. Together the two are the pair hFv, hGv that Multiscale.LayerUniform and the Step-3 assembly carry as a collar A antecedent's |∇·D̂_q(𝔰)|²/|q|² + |∇ℓ̂_p(𝔰)|²/|p|² ≤^{2b(k+h_k)} is their sum.

The object

e.hatdq reads, for the family {ℓ̂_p} of e.hat.linear.1,

(D̂_q)_{ij} := (d−1)⁻¹ ( q_j ℓ̂_{e_i} − q_i ℓ̂_{e_j} ) ,

and the manuscript's divergence convention (the footnote) is (∇·A)_j = ∑_i ∂_{x_i} A_{ij}. competitorAntisymDatum is the vertex datum of the (i,j) entry at the repository's competitor family ℓ̂_p = competitorVertexData ℐ p and competitorDivergence is the resulting cell-constant divergence, i.e. ABK26's (∇·D̂_q)(𝔰). Only the d basis slopes ℓ̂_{e_i} enter, exactly as printed, so no linearity of p ↦ ℓ̂_p is assumed anywhere: e.hat.linear.linearity is used only through kuhnSlope's own unconditional linearity in the datum, which kuhnSlope_competitorAntisymDatum records.

The route

The F-leg's Euclidean conclusion is not strong enough to feed the G-leg at the same constant — it has already paid the ℓ¹ → ℓ² factor d, and re-paying it inside the divergence would cost a further factor. What the G-leg needs is the coordinatewise Step-2 estimate, one level below:

1. abs_kuhnSlope_competitorVertexData_sub_le_of_forall_touching is KuhnInterpolation.abs_kuhnSlope_sub_le_of_vertex_oscillation fed by the Step-2 vertex bound of CompetitorVertexData: every coordinate of ∇ℓ̂_p − p on the cell is at most 2 |p|_{ℓ¹} D / (cell side), with D the active-component diameter bound. At p = e_i the ℓ¹ size is 1, so all d² entries of the deviation matrix u_i := ∇ℓ̂_{e_i} − e_i obey the one bound η = 2 D / (cell side).
2. competitorDivergence_sub_eq is the exact algebraic identity (∇·D̂_q)_j − q_j = (d−1)⁻¹ ((∑_i (u_i)_i) q_j − ∑_i q_i (u_j)_i); the d and the q_j of the two sums cancel against the (d−1) precisely because ∇·D_q = q for the exact family (the display and the sentence).
3. vecNormSq_divergenceDeviation_le is the pure ℓ^∞-to-ℓ² core: the i = j term of that sum vanishes identically, so each coordinate is a sum of d − 1 terms, giving |·|_j ≤ η ((d−2)|q_j| + |q|_{ℓ¹}) and, with |q|_{ℓ¹}² ≤ d |q|² and (d−2)² + 2d(d−2) + d² = (2d−2)², the bound |(∇·D̂_q) − q|² ≤ (2η)² |q|². It is here that 2 ≤ d is used, twice: (d−1)⁻¹ must be finite and (d−2) nonnegative.
4. The scale step is the F-leg's own four_mul_three_rpow_layer_envelope_le (shared directly; de-privatized): D / (cell side) ≤ 324 · 3^{b(k+h_k)}, so 2η ≤ 1296 · 3^{b(k+h_k)}.

The constant, itemized

2η ≤ 4 · 324 · 3^{b(k+h_k)} = 1296 · 3^{b(k+h_k)} = 648 · 2 · 3^{b(k+h_k)}, and 648 · 2 ≤ 648 d exactly because d ≥ 2. So the G-leg meets the F-leg's constant 648 d with equality at d = 2 and with slack for d > 2: the F-leg spends its second d on ℓ¹ → ℓ² for a general slope p, while the G-leg spends 2 on the divergence's own (2d−2)/(d−1) and inherits ℓ¹-size 1 from the basis slopes. Nothing is optimized; as in the F-leg, no random quantity, no layer index and no component enters the constant.

Scope

This module is the per-cell estimate only, at the level e.sum-of-a-decomp consumes. It constructs no global field: nothing is claimed about ∇·D̂_q ∈ q + L²_{sol,0}(□_m) (e.hat.D.bc), about divergence-freeness of the assembled piecewise-constant field (: the face jumps cancel only because D̂_q ∈ W^{1,∞}, which needs the global continuity of ℓ̂_{e_i} that CompetitorVertexData explicitly does not supply), or about e.hat.linear.1. Those remain the open obligations recorded in CompetitorVertexData's scope section/-c. No overlap count is consumed (as in the F-leg: the hact binder is the max over the active components, and max ≤ sum), and no layer window is assumed.

References

• ABK26, (e.dq), (the divergence convention footnote), (e.hatdq), (e.hat.D.bc), (the cell-constant values), (e.hat.linear.linearity), (Step 2), (label, r.gradient.bound.simplified), (e.bounds.on.slopes.when.bad).

The ℓ^∞-to-ℓ² core

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_divergenceDeviation_le {d : ℕ} (hd : 2 ≤ d) (q : HCPolySupport.Vec d) (u : Fin d → HCPolySupport.Vec d) {eta : ℝ} (hu : ∀ (i l : Fin d), |u i l| ≤ eta) : (HCPolySupport.vecNormSq fun (j : Fin d) => (↑d - 1)⁻¹ * ((∑ i : Fin d, u i i) * q j - ∑ i : Fin d, q i * u j i)) ≤ (2 * eta) ^ 2 * HCPolySupport.vecNormSq q

The pure algebra of the G-leg. If every entry of the deviation family u is at most η in absolute value, then

| (d−1)⁻¹ ( (∑_i (u_i)_i) q − (u_·ᵀ q) ) |²  ≤  (2 η)² |q|² .

The i = j term of the inner sum vanishes identically, so each coordinate is a sum of d − 1 terms and obeys η ((d−2)|q_j| + |q|_{ℓ¹}); squaring, summing and using |q|_{ℓ¹}² ≤ d |q|² gives (d−2)² + 2d(d−2) + d² = (2d−2)², which is exactly cancelled by the (d−1)⁻¹. This is the only place 2 ≤ d is consumed, and it is consumed sharply: at d = 2 the bound is (2η)².