Coarse-graining support: Support.Besov.Negative.ExactCircDomination #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Exact circ domination of the dual negative Besov kernels #
This module collects the three source exponent regimes of the Chapter 1
dual-to-circ comparison. It also records that the depth-zero circ weight in
the full-norm bounds is literally the manuscript factor 3^(s m), with
m = Q.scale.
theorem
HCPolySupport.exactCircDepthWeight_zero_eq_sourceRootWeight
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
:
The depth-zero exact circ weight is the manuscript root factor 3^(s m),
where m is the scale of the parent cube.