HomSpineCzGridGauge #

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

The grid gauge against `CoarseGraining`'s negative Besov seminorm #

What this file does #

Clause 1 of the transcribed source hypothesis reduces to the Calderón--Zygmund flux comparison lemma read at the multiscale grid gauge, and that reduction comes down to a SINGLE inequality of pure fractional-Sobolev type, with no PDE content and no carrier of this repository in it:

  [F]_{B^{-s}_{p,p}(Q)}  ≤  C(p,d) · ‖F‖_{W_hat^{-s,p}(Q)}          (★)

— the CONVERSE of CoarseGraining's proved cubeEuclideanNegativeWspSmoothDualENorm_le_cubeEuclideanNegativeBesovESeminorm (EuclideanWspSmoothDualBesovBound), on the range s·p' < 1 where p' = p/(p-1) is the conjugate exponent. (★) is not proved in this repository, in CoarseGraining, or in Mathlib.

What this file supplies is the development-carrier identification (§2 below) that the reduction runs on. The analytic halves are elsewhere: the CZ step at the smooth-dual reading is CoarseGraining's proved exists_centeredCubeFluxComparison_cz, the coarse-graining half is its unconditional exists_localCoarseGrainingLp, and the smooth-dual composition is assembled in HomCGDischargeAssembly.

The carrier identification (`§2`) #

The depth-truncated (p,p) grid gauge of HomFinitePGauge is the printed 3^{-ms}[F]_{B^{-s}_{p,p}(□_m)} truncated at depth N, built on the Euclidean magnitude of the cell averages. CoarseGraining's cubeEuclideanNegativeBesovESeminorm is the same lattice sum without the 3^{-ms} normalization and with the sup magnitude of the cell averages. Hence

  negBesovLpPartialNorm Q s p N F  ≤  √d · 3^{-s·Q.scale} · [F]_{B^{-s}_{p,p}(Q)}

by a depth reindexing (descendantsAtScale_eq_descendantsAtDepth) and the Euclidean/sup comparison √(Σ xᵢ²) ≤ √d · sup|xᵢ|. No constant beyond √d is spent; the depth-seminorm form of the comparison is ofReal_negBesovLpDepthSeminorm_rpow_le.

The smoothness question, CLOSED #

The grid gauge's own dual tests are multi-depth grid-piecewise constants, which are not C^∞; the natural worry is that CoarseGraining's smooth-dual carrier does not see them. It does. CoarseGraining proves, unconditionally,

  ennreal_ofReal_abs_cubeEuclideanNormalizedFieldPairing_le:
    |⟨F, G⟩|  ≤  ‖F‖_{W_hat^{-s,p}(Q)} · ‖G‖_{W^{s,p'}(Q)}

for EVERY G ∈ W^{s,p'}(Q) ∩ L²(Q) (EuclideanWspSmoothDualFieldPairing; the mechanism is the completed-graph extension of EuclideanWspCompletedDualExtension, built on the smooth density theorem exists_cubeEuclideanWspSmoothTest_fullENorm_and_l2_sub_lt). So (★) carries no smoothness obligation whatsoever, and the existence of normalized W^{s,p'} ∩ L² tests that see the truncated grid mass is the exact and only remaining analytic content of the multiscale clause.

1. The Euclidean magnitude against the carrier's sup norm #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_vecNormSq_le_sqrt_dim_mul_norm {d : ℕ} (x : HCPolySupport.Vec d) :

√(HCPolySupport.vecNormSq x) ≤ √↑d * ‖x‖

√(Σ xᵢ²) ≤ √d · sup|xᵢ|. Vec d carries the product (sup) norm; the gauge of this repository is built on the Euclidean magnitude. This is the only constant the identification of the two gauges costs.