SuperposedEnvelope

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

The summed collar envelope of the superposed competitor

This module proves a local summed active-component gradient estimate for the superposition presentation of l.piecewise.affine.approx. On a good collar cube nothing identifies the superposed cell slope with the single-mesh kuhnSlope ∘ competitorVertexData, so pricing it needs the summed estimate together with the dimension-only multiplicity bound |𝒜_R| ≤ M(d). That bound is ActiveFamily.ncard_activeComponents_le, with M(d) = 3·11^d, and this module performs the aggregation on top of it.

The summed display, and what is implemented

The correct form of the gradient estimate of e.hat.linear.properties — the printed component-local display is false for the superposed competitor — is

  |∇ℓ̂_p − p|  ≤  C(d) |p| ∑_{𝒞 ∈ 𝒜_R} diam(𝒞) / ρ_𝒞 ,
  𝒜_R = {𝒞 : R ∈ 𝒩(𝒞)} ,   ρ_𝒞 = 3^{m−(j_𝒞+1)−h_{j_𝒞+1}} ,

with the equivalent restatement: after proving the dimension-only Whitney overlap bound |𝒜_R| ≤ M(d), one may use the squared form |∇ℓ̂_p − p|² ≤ C(d)|p|² ∑_{𝒞 ∈ 𝒜_R} diam(𝒞)²/ρ_𝒞².

That squared form is what is implemented, in three steps and with every constant explicit:

1. the sum itself — superposedCompetitorCellSlope_sub_eq_sum collapses the defining finsum to a finite sum over any Finset containing 𝒜_R (inactive components have cell constant p, so they contribute 0);
2. one summand — vecNormSq_globalCompetitorCellSlope_sub_le_diam is exactly d (2 |p|_{ℓ¹} diam(𝒞) / ρ_𝒞)² at the component's own common coarse cell, with ρ_𝒞 = componentInterpolationScale the interpolation scale of that component;
3. the aggregation — vecNormSq_sum_le_card_mul_sum_vecNormSq (finite-vector Cauchy--Schwarz, |∑ v|² ≤ |A| ∑ |v|²) followed by card_le_multiplicityBound_of_forall_mem_activeComponents. This is the "after proving |𝒜_R| ≤ M(d)" clause; M(d) enters twice, once from Cauchy--Schwarz and once from summing the uniform per-component envelope.

The L¹ display is the pre-Cauchy--Schwarz form of the same sum and is not separately stated: the consumers below take squares.

The layer envelope, and the constant

Feeding the proved local cluster-diameter datum into the summand gives the per-component layer envelope at the same constant as the single-mesh envelope of CollarLayerEnvelope.lean,

  |∇ℓ̂_p^𝒞 − p|²  ≤  (648 d)² 3^{2 b (k + h_k)} |p|²    on every cell of a
                                                        layer-`k` Whitney cube,

and the aggregation then gives the deliverable

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

Itemized: 648 d is CollarLayerEnvelope's own constant (2 for the two-vertex oscillation, one d for the Kuhn coordinates, one d for the ℓ¹-to-ℓ² conversion, 324 = 4·3⁴ for the cluster-diameter bound's factor 4 times the scale step), and M(d) = 3·11^d is ActiveFamily.multiplicityBound (three layers times the cubewise per-layer packing). Nothing on the right depends on a component, a layer of a component, or the sample. This is the Cgrad of r.gradient.bound.simplified, discharged here at Cgrad = superposedGradConst d for the superposed competitor.

Why the single-mesh endpoint is not instantiated directly

The single-mesh collar layer envelope prices kuhnSlope 𝔰 (competitorVertexData ℐ p) − p at the final e.SW.def cell 𝔰 and the whole family ℐ. The summand of the superposition is a different object: the cell constant of one component's correction is kuhnSlope U (competitorVertexData 𝒞 p) at the coarse root cell U of that component's own common mesh, whose side is ρ_𝒞 and not the final cell side. So the single-mesh endpoint is not instantiable here, but its proved local route is: this module reuses the public instruments (active_badComponent_finite_and_diam_le, four_mul_three_rpow_layer_envelope_le, closedCubeCarrier_mono) together with CompetitorVertexData's vecNormSq_kuhnSlope_competitorVertexData_sub_le_of_forall_touching, which is already stated at an arbitrary descendantsAtScale Q j and therefore applies verbatim at the coarse cell. The diameter datum is the proved local one, at the single component recovered from its own touching bad cube.

Scope

The estimate is per cell of SW(□_m), which is the level at which e.hat.linear.properties states its gradient estimate, and the level Multiscale.sum_of_a_decomp consumes. It is a statement about the defined field superposedCompetitorSlope, which ActiveFamily.superposedCompetitor_sub_eq_vecDot identifies as the classical per-cell gradient; no a.e./weak-gradient identification, no H¹₀ membership and no solenoidal leg is claimed here. The G-leg of the superposed branch of Multiscale.ConclusionRoot is the same object at the load q, so the deliverable, being stated for every p : Vec d, discharges both legs; the divergence competitor of CollarLayerEnvelopeG.lean is the G-leg of the single-mesh branch and is not used here. No global function, continuity or subordination statement is made (they are ActiveFamily.lean's).

Consumer shape

The conclusion is character-for-character the hFv/hGv binder of

• Multiscale.ConclusionAssemblyFinal.collarCellForm_le_collarEnvelopeConst_mul_layerQuantity_ae,
• Multiscale.ConclusionRoot.tsum_simplexPartition_cutoff_two_leg_le_ofReal_payload_assembled_ae,
• Multiscale.LayerUniform.blockVecDot_coarseBlockMatrix_collar_whitneySimplexCells_le_ae and Multiscale.ConclusionCompetitor.collarCellForm_le_stepOneLayerMajorant_ae,

namely vecNormSq (Fv T − p) ≤ Cgrad² 3^{2(b(n+h_n))} vecNormSq p quantified over n, Q ∈ 𝒲(□_m,n) and T ∈ S(□), at Cgrad := superposedGradConst d (1 ≤ Cgrad is one_le_superposedGradConst). This module does not perform that composition and closes no node.

References

• ABK26: l.piecewise.affine.approx and e.hat.linear.properties; Step 1 with the common coarse mesh and its scale 3^{m−(n_j+1)−h_{n_j+1}}, and Step 2; r.gradient.bound.simplified; e.SW.def; e.neighborhood.def; l.bad.clusters.geometry and e.cluster.diameter.bound; e.hn.gap; e.bounds.on.slopes.when.bad.

The aggregation device

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_sum_le_card_mul_sum_vecNormSq {d : ℕ} {ι : Type u_1} (A : Finset ι) (v : ι → HCPolySupport.Vec d) : HCPolySupport.vecNormSq (∑ C ∈ A, v C) ≤ ↑A.card * ∑ C ∈ A, HCPolySupport.vecNormSq (v C)

Finite-vector Cauchy--Schwarz: |∑_{a ∈ A} v_a|² ≤ |A| ∑_{a ∈ A} |v_a|².

The interpolation scale ρ_𝒞

noncomputable def Algsuperdiff.Section3.Provider.Affine.componentInterpolationScale {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (C : Set (HCPolySupport.TriadicCube d)) : ℝ

ρ_𝒞 = 3^{m−(j_𝒞+1)−h_{j_𝒞+1}}: the side of the common coarse mesh on which the correction belonging to the component 𝒞 is interpolated, with j_𝒞 the least Whitney layer met by 𝒩(𝒞) (represented by componentWindowLayer).

Equations

• One or more equations did not get rendered due to their size.

The cell slope of the superposition is a finite sum over 𝒜_R

theorem Algsuperdiff.Section3.Provider.Affine.superposedCompetitorCellSlope_sub_eq_sum {d : ℕ} [NeZero d] {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) {I : Set (HCPolySupport.TriadicCube d)} (hI : I ⊆ Whitney.whitneyPartition m hn) (hwin : ∀ C ∈ badComponents I, (Whitney.whitneyNeighborhood m hn C).Finite ∧ ∀ R ∈ Whitney.whitneyNeighborhood m hn C, R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C) ∨ R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C + 1)) (p : HCPolySupport.Vec d) {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn n) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m hn n Q) {A : Finset (Set (HCPolySupport.TriadicCube d))} (hAsub : ∀ C ∈ A, C ∈ badComponents I) (hAact : ∀ C ∈ activeComponents m hn I Q, C ∈ A) : superposedCompetitorCellSlope m hn I p T - p = ∑ C ∈ A, (globalCompetitorCellSlope m (Whitney.simplexScale m hn (componentWindowLayer m hn C)) C p T - p)

The superposed cell slope is p plus a finite sum over the active components ('s 𝒜_R). Any finite family A of components containing 𝒜_R may be used: a component inactive at the cell's Whitney cube has cell constant p and contributes 0 (clause 3 of e.hat.linear.properties). This exports, publicly, the collapse proved inside ActiveFamily.superposedCompetitor_sub_eq_vecDot.

One summand: a single component, at its own scale ρ_𝒞

theorem Algsuperdiff.Section3.Provider.Affine.finite_of_mem_activeComponents {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {I : Set (HCPolySupport.TriadicCube d)} (hI : I ⊆ Whitney.whitneyPartition m hn) (hwin : ∀ C ∈ badComponents I, (Whitney.whitneyNeighborhood m hn C).Finite ∧ ∀ R ∈ Whitney.whitneyNeighborhood m hn C, R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C) ∨ R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C + 1)) {Q : HCPolySupport.TriadicCube d} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ activeComponents m hn I Q) : C.Finite

An active component is finite — it sits inside its own touching neighborhood, which the proved cluster geometry makes finite.

theorem Algsuperdiff.Section3.Provider.Affine.exists_mem_cubeTouch_badComponent_eq_of_mem_activeComponents {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {I : Set (HCPolySupport.TriadicCube d)} {R : HCPolySupport.TriadicCube d} {C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ activeComponents m hn I R) : ∃ B ∈ I, Whitney.CubeTouch R B ∧ Whitney.badComponent I B = C

An active component is the component of one of its own bad cubes touching R — the maximality fact isolates, in the form that hands the proved local diameter datum to a single component.

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_globalCompetitorCellSlope_sub_le_diam {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} (hmono : Monotone hn) {I : Set (HCPolySupport.TriadicCube d)} (hI : I ⊆ Whitney.whitneyPartition m hn) (hwin : ∀ C ∈ badComponents I, (Whitney.whitneyNeighborhood m hn C).Finite ∧ ∀ R ∈ Whitney.whitneyNeighborhood m hn C, R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C) ∨ R ∈ Whitney.whitneyLayer m hn (componentWindowLayer m hn C + 1)) (p : HCPolySupport.Vec d) {n : ℕ} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn n) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m hn n Q) {C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ activeComponents m hn I Q) {D : ℝ} (hD0 : 0 ≤ D) (hCdiam : Metric.diam (Whitney.closedCubeCarrier C) ≤ D) : HCPolySupport.vecNormSq (globalCompetitorCellSlope m (Whitney.simplexScale m hn (componentWindowLayer m hn C)) C p T - p) ≤ ↑d * (2 * (vecNormOne p * D) / componentInterpolationScale m hn C) ^ 2

The summand's corrected estimate: the cell constant of one component's correction deviates from p by at most d (2 |p|_{ℓ¹} diam(𝒞) / ρ_𝒞)² in squared Euclidean norm, on every cell of every Whitney cube at which the component is active.

This is Step 2 of l.piecewise.affine.approx read at the component's own common coarse mesh: the final e.SW.def cell sits inside a single cell U of that mesh, U has side ρ_𝒞, and the Step-2 vertex bound applies at U because U is a triadic descendant of the Whitney cube.

The per-component layer envelope

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_globalCompetitorCellSlope_sub_le_layerEnvelope {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ Whitney.whitneyPartition m (Whitney.whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) (p : HCPolySupport.Vec d) {k : ℕ} {R : HCPolySupport.TriadicCube d} (hRlay : R ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) k) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m (Whitney.whitneyScaleSeq b hs k₀) k R) {C : Set (HCPolySupport.TriadicCube d)} (hC : C ∈ activeComponents m (Whitney.whitneyScaleSeq b hs k₀) S R) : HCPolySupport.vecNormSq (globalCompetitorCellSlope m (Whitney.simplexScale m (Whitney.whitneyScaleSeq b hs k₀) (componentWindowLayer m (Whitney.whitneyScaleSeq b hs k₀) C)) C p T - p) ≤ (648 * ↑d) ^ 2 * 3 ^ (2 * (b * (↑k + ↑(Whitney.whitneyScaleSeq b hs k₀ k)))) * HCPolySupport.vecNormSq p

The layer envelope of ONE component's correction: on every cell of a layer-k Whitney cube at which the component 𝒞 is active,

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

This is's summand with the proved local cluster diameter inserted: diam(𝒞) ≤ 4·3^{b(l+h_l)}3^{m−l−h_l} (l.bad.clusters.geometry(2)'s factor 4, via active_badComponent_finite_and_diam_le at the component recovered from its own touching bad cube), divided by ρ_𝒞 = 3^{m−(j_𝒞+1)−h_{j_𝒞+1}}. The constant is the same 648 d as the single-mesh local envelope; the window binder is discharged, not assumed.

The deliverable: the layer envelope of the superposed competitor

def Algsuperdiff.Section3.Provider.Affine.superposedGradConst (d : ℕ) : ℝ

It is the Cgrad of r.gradient.bound.simplified for the superposed competitor.

Equations

• Algsuperdiff.Section3.Provider.Affine.superposedGradConst d = ↑(Algsuperdiff.Section3.Provider.Affine.multiplicityBound d) * (648 * ↑d)

theorem Algsuperdiff.Section3.Provider.Affine.superposedGradConst_eq (d : ℕ) : superposedGradConst d = 1944 * ↑d * 11 ^ d

theorem Algsuperdiff.Section3.Provider.Affine.one_le_superposedGradConst {d : ℕ} (hd : 1 ≤ d) : 1 ≤ superposedGradConst d

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_superposedCompetitorCellSlope_sub_le_layerEnvelope {d : ℕ} [NeZero d] {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ Whitney.whitneyPartition m (Whitney.whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) (p : HCPolySupport.Vec d) {k : ℕ} {R : HCPolySupport.TriadicCube d} (hRlay : R ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) k) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m (Whitney.whitneyScaleSeq b hs k₀) k R) : HCPolySupport.vecNormSq (superposedCompetitorCellSlope m (Whitney.whitneyScaleSeq b hs k₀) S p T - p) ≤ superposedGradConst d ^ 2 * 3 ^ (2 * (b * (↑k + ↑(Whitney.whitneyScaleSeq b hs k₀ k)))) * HCPolySupport.vecNormSq p

's summed active-component estimate, in the layer-envelope form the collar A consumes — the deliverable of this module and the bridge that Multiscale.ConclusionRoot's F-1 leaves open. On every cell of every layer-k Whitney cube,

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

for the superposed competitor ℓ̂_p = ℓ_p + Σ_𝒞 (ℓ̂_p^𝒞 − ℓ_p)'s overlap-safe presentation. The multiplicity M(d) enters twice — once through Cauchy--Schwarz, once through summing the uniform per-component envelope — which is exactly's requirement that the overlap multiplicity be paid "in the gradient and energy constants".

Nothing on the right depends on a component, on a layer of a component or on the sample: the whole random content sits in the binder havoid, the deterministic diameter-avoidance datum the cluster node already runs on. The window binder hwin of the superposition chain is discharged here, not assumed.

theorem Algsuperdiff.Section3.Provider.Affine.badFamily_vecNormSq_superposedCompetitorCellSlope_sub_le_layerEnvelope {d : ℕ} [NeZero d] {M : ABKModel d} {m : ℤ} {E b : ℝ} {k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (hne : (Percolation.hsepSet M m E b omega).Nonempty) (p : HCPolySupport.Vec d) {k : ℕ} {R : HCPolySupport.TriadicCube d} (hRlay : R ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m E b k₀ omega) k) {T : Whitney.KuhnCell d} (hT : T ∈ Whitney.whitneySimplexCells m (Whitney.whitneyScale M m E b k₀ omega) k R) : HCPolySupport.vecNormSq (superposedCompetitorCellSlope m (Whitney.whitneyScale M m E b k₀ omega) (Whitney.badFamily M m (Whitney.whitneyScale M m E b k₀ omega) omega) p T - p) ≤ superposedGradConst d ^ 2 * 3 ^ (2 * (b * (↑k + ↑(Whitney.whitneyScale M m E b k₀ omega k)))) * HCPolySupport.vecNormSq p

The deliverable at the manuscript's own bad family and profile ℐ = badFamily M m h_n omega, h_n = whitneyScale M m E b k₀ omega, with the avoidance binder discharged by the proved e.diameter.deterministic, exactly as in the proved single-mesh envelope's own concrete corollary. Applied at the load q this is also the G-leg of the superposed branch of Multiscale.ConclusionRoot.