StepSevenWireEmbedding

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

t.regularity Step 7d: wiring the mean-zero fractional Sobolev embedding

The gap this module closes

The Step-7d oscillation endpoint carries a second conditional input hembed : oscLoc ≤ Cemb · besovP1 — the mean-zero fractional Sobolev embedding e.fractional.Sobolev.embedding, read at (s,p,q) = (1,2,1) (the zero-trace twin is the wrong one: u carries the boundary datum h, not 0). The producer is cubeBesovOscillation_le_oscillationMultiscalePoincareConstant_mul_sum_cubeBesovCircNorm, whose left side is ‖u - (u)_Q‖_{L²(Q)}, whose binder is H1Function with no zero-trace hypothesis, and whose constant is dimension-only. Two carrier residues remain, and both are closed here.

Residue (a): the coordinate aggregation — the constant is d, not √d

The Section-3 producer's right-hand side is the coordinate sum Σ_i [∂_i u]_{B^{-1}_{2,1}} of scalar circ norms, while the besovP1 slot is a single vector object. The bridge is proved upstream, per coordinate, at constant one: CoarseGraining's

  cubeBesovCircNorm_two_one_component_le_scaleWeight_neg_mul_of_negativeVectorPartialBound

says that whenever B dominates every finite-depth vector partial seminorm cubeBesovNegativeVectorPartialSeminorm Q s N F, each coordinate's circ norm is at most 3^{s·scale}·B. Summing the d coordinates gives the factor d.

The factor is d, not √d: √d is the Cauchy--Schwarz constant at the depth level, and it is attainable, but the available upstream bridge is the per-coordinate one at constant 1, so the honest aggregation in the proved carriers costs d. Both are C(d); the printed constant is C(d). Nothing else moves.

Residue (b): the off-grid cube z'+□_{m'-1}

z' is the clamped, off-lattice centre, so z'+□_{m'-1} is not a TriadicCube and the Section-3 producer does not apply to it directly. normalizedL2On_image_add_sub_average_le_cubeBesovOscillation performs exactly that recovery, from three proved ingredients and no new analysis:

• image_add_eq_translateSet — z'+□ = translateSet z' □;
• normalizedL2On_sub_volumeAverage_le — the mean minimizes the deviation, so the §4.4 window's own mean may be replaced by the origin-cube average (u(·+z'))_{□} for free;

together with the Section-3 identity normalizedL2SqOnSet_openCubeSet_centred_eq_cubeBesovOscillation_sq.

The scale normalization (one factor of 3)

Everything here is stated at the scale normalization of Q: the oscillation carries (cubeScaleFactor Q)⁻¹ = 3^{-Q.scale} and the negative Besov carrier cubeBesovNegativeVectorSeminorm Q 1 F is 3^{-Q.scale}‖F‖_{B^{-1}_{2,1}(Q)} already. At Q.scale = m'-1 the printed display weights the oscillation by 3^{-(m'-1)} (matching) and the Besov leg by 3^{-m'} (one factor 3 smaller); that single 3 is inside the printed C, and no exponent moves.

References

• ABK26, e.fractional.Sobolev.embedding; Step 7d.
• Algsuperdiff/Section3/Provider/Besov/OscillationPoincare.lean.
• CoarseGraining, Homogenization/Deterministic/WeakNormInterfacesComponentwise.lean.

1. The embedding constant

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenEmbeddingConst (d : ℕ) : ℝ

The Step-7d embedding constant: the Section-3 multiscale Poincaré constant times the coordinate count d. Both factors are dimension-only — no ellipticity object of any kind occurs.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenEmbeddingConst d = ↑d * Algsuperdiff.Section3.Provider.Besov.oscillationMultiscalePoincareConstant d

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenEmbeddingConst_nonneg (d : ℕ) : 0 ≤ stepSevenEmbeddingConst d

2. Residue: the coordinate aggregation

theorem Algsuperdiff.Section4.Provider.Regularity.sum_cubeBesovCircNorm_le_dim_mul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hB : ∀ (N : ℕ), HCPolySupport.cubeBesovNegativeVectorPartialSeminorm Q s N F ≤ B) : (∑ i : Fin d, HCPolySupport.cubeBesovCircNorm Q s 2 1 fun (x : HCPolySupport.Vec d) => F x i) ≤ ↑d * (HCPolySupport.cubeBesovScaleWeight (-s) Q * B)

The coordinate aggregation, at the proved constant d. If B dominates every finite-depth vector partial seminorm of F on Q, then the coordinate sum of the scalar negative circ norms is at most d · 3^{s·scale} · B.

The per-coordinate step is CoarseGraining's own bridge at constant 1; the d is the plain coordinate count.

3. The embedding at the note normalization

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenEmbedding_of_partialBound {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) {B : ℝ} (hB : ∀ (N : ℕ), HCPolySupport.cubeBesovNegativeVectorPartialSeminorm Q 1 N u.grad ≤ B) : ((HCPolySupport.cubeScaleFactor Q)⁻¹ * HCPolySupport.cubeBesovOscillation Q 2 fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ stepSevenEmbeddingConst d * B

e.fractional.Sobolev.embedding at the §4.4 cube, from a uniform partial bound. For every H¹(Q) function u and every B dominating the finite-depth vector partial seminorms of ∇u at index 1,

  3^{-scale}‖u - (u)_Q‖_{L²(Q)}  ≤  d · C_osc(d) · B .

This is the hembed slot: oscLoc ≤ Cemb · besov, at the scale normalization, with a coefficient-free C(d). Unconditional beyond the printed embedding's own binders.

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenEmbedding {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (hbdd : BddAbove (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminorm Q 1 N u.grad)) : ((HCPolySupport.cubeScaleFactor Q)⁻¹ * HCPolySupport.cubeBesovOscillation Q 2 fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ stepSevenEmbeddingConst d * HCPolySupport.cubeBesovNegativeVectorSeminorm Q 1 u.grad

e.fractional.Sobolev.embedding at the §4.4 cube, at the negative Besov q = 1 carrier. The BddAbove binder is the printed membership ∇u ∈ B^{-1}_{2,1}(Q) in the upstream interface's own form.

4. Residue (b): the off-grid window, by translating the sample

theorem Algsuperdiff.Section4.Provider.Regularity.normalizedL2On_image_add_sub_average_le_cubeBesovOscillation {d : ℕ} {Q : HCPolySupport.TriadicCube d} {c : HCPolySupport.Vec d} {w : HCPolySupport.Vec d → ℝ} (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)) (hv : ∀ (y : HCPolySupport.Vec d), v.toFun y = w (y + c)) (hTm : MeasurableSet ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet Q)) (hTpos : 0 < (MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet Q)).toReal) (hTfin : MeasureTheory.volume ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet Q) ≠ ⊤) (hw : MeasureTheory.IntegrableOn w ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet Q) MeasureTheory.volume) (hw2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => w x ^ 2) ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet Q) MeasureTheory.volume) : (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet Q) fun (x : HCPolySupport.Vec d) => w x - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet Q) w) ≤ HCPolySupport.cubeBesovOscillation Q 2 fun (x : HCPolySupport.Vec d) => v.toFun x

The off-grid recovery, by translating the sample.

For an off-lattice centre c and a triadic cube Q, the §4.4 mean-subtracted L² oscillation on the translated window c+□_Q is at most the origin-cube oscillation of the translated sample:

  ‖u - (u)_{c+□_Q}‖_{L²(c+□_Q)}  ≤  ‖v - (v)_{□_Q}‖_{L²(□_Q)} ,
                                      v = u(·+c) .

The mean is replaced for free (it minimizes the deviation) and the normalized L² square transports under translation — no constant, no new analysis.