EuclideanWspLegacyCircComparison #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
Legacy scalar circ versus the source negative Besov envelope #
The legacy scalar circ partial norms use real-valued finite sums and include
the depths 0, …, N. The source-aligned scalar envelope uses ENNReal and
the half-open finite range 0, …, N - 1. This module records the literal
finite-depth change of presentation without adding an Lᵖ assumption to the
represented L² field.
theorem
HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarDepthEnergy_eq_legacy
{d : ℕ}
(Q : TriadicCube d)
(s : ↑FractionalOrder)
(p : FiniteLpExponent)
(F : CubeEuclideanLpField Q FiniteLpExponent.two)
(i : Fin d)
(j : ℕ)
:
cubeEuclideanNegativeBesovScalarDepthEnergy Q s p F i j = ENNReal.ofReal (cubeBesovCircDepthSeminorm Q (↑s) p.exponent (fun (x : Vec d) => F.toField x i) j) ^ p.exponent.toReal
theorem
HCPolySupport.Book.Ch03.ABK26.cubeEuclideanNegativeBesovScalarPartialENorm_succ_eq_legacy
{d : ℕ}
(Q : TriadicCube d)
(s : ↑FractionalOrder)
(p : FiniteLpExponent)
(F : CubeEuclideanLpField Q FiniteLpExponent.two)
(i : Fin d)
(N : ℕ)
:
cubeEuclideanNegativeBesovScalarPartialENorm Q s p F i (N + 1) = ENNReal.ofReal (cubeBesovCircPartialNorm Q (↑s) p.exponent p.exponent N fun (x : Vec d) => F.toField x i)
The legacy partial norm at truncation N includes exactly the source
depths in the half-open range N + 1.
theorem
HCPolySupport.Book.Ch03.ABK26.ennreal_ofReal_cubeBesovCircPartialNorm_le_cubeEuclideanNegativeBesovESeminorm
{d : ℕ}
(Q : TriadicCube d)
(s : ↑FractionalOrder)
(p : FiniteLpExponent)
(F : CubeEuclideanLpField Q FiniteLpExponent.two)
(i : Fin d)
(N : ℕ)
:
ENNReal.ofReal (cubeBesovCircPartialNorm Q (↑s) p.exponent p.exponent N fun (x : Vec d) => F.toField x i) ≤ cubeEuclideanNegativeBesovESeminorm Q s p F
Every finite legacy circ partial norm is top-safely controlled by the frozen source-facing vector negative Besov seminorm.