LocalCoarseGrainingNegativeAssembly

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Exact negative-Besov assembly for local coarse graining

This module flattens the nested normalized descendant average in the source-facing local negative Besov carrier into its physical-scale series.

theorem HCPolySupport.Book.Ch03.ABK26.localFluxDefectNegativeBesovLpAverage_rpow_eq_tsum_descendantsAtScale {d : ℕ} (Q : TriadicCube d) (n : ℤ) (hn : n ≤ Q.scale) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (sigma0 : ℝ) (u : H1Function (openCubeSet Q)) (s : ↑FractionalOrder) (p : FiniteLpExponent) : localFluxDefectNegativeBesovLpAverage Q n hn a sigma0 u s p ^ p.exponent.toReal = ∑' (j : ℕ), ENNReal.ofReal (Real.rpow 3 (-(↑s * p.exponent.toReal * ↑j))) * descendantsAtScaleENNAverage Q (n - ↑j) fun (R : TriadicCube d) => ENNReal.ofReal ‖cubeAverageVec R fun (x : Vec d) => matVecMul (a.toCoeffField x - scalarMatrix sigma0) (u.grad x)‖ ^ p.exponent.toReal

Raising the local finite-p flux-defect negative Besov average exposes the exact physical-scale depth series.