Coarse-graining support: Support.Sobolev.Foundations.CubeBesovPoincare.W12Aggregation #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Finite positive Besov aggregation #
This is the scale-cancellation step from a local cube Poincare estimate to a
finite B¹_{2,∞} seminorm bound. It contains no analytic input beyond the
explicit local oscillation and normalized descendant-energy hypotheses.
theorem
HCPolySupport.cubeBesovPartialSeminormTop_one_two_le_of_localOscillation
{d : ℕ}
(Q : TriadicCube d)
(N : ℕ)
(f : Vec d → ℝ)
(K G : ℝ)
(E : TriadicCube d → ℝ)
(hK : 0 ≤ K)
(hG : 0 ≤ G)
(hE : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, 0 ≤ E R)
(hosc :
∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, cubeBesovOscillation R 2 f ≤ K * cubeScaleFactor R * E R)
(havg : ∀ j ∈ Finset.range (N + 1), (descendantsAverage Q j fun (R : TriadicCube d) => E R ^ 2) ≤ G ^ 2)
:
A scale-sharp local oscillation bound and uniform normalized descendant
energy control imply the finite triadic-cube B¹_{2,∞} bound.