Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.AveragingScale

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.SmoothOverlapPartition.exists_gradientCoordL2NormSum_averagingCompetitor_le_volume_invScale_sqrt_depthAverage {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (hloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S)) : ∃ (C : ℝ), 0 ≤ C ∧ (P.averagingCompetitor h).gradientCoordL2NormSum ≤ cubeVolume Q ^ (1 / 2) * (C / (cubeScaleFactor Q / 3 ^ j)) * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

Raw parent-cube coordinate-summed gradient bound for the overlap averaging competitor. This is still unnormalized by the parent scale.

theorem HCPolySupport.SmoothOverlapPartition.exists_rpow_neg_mul_relativeGradientCoordL2NormSum_averagingCompetitor_le_sqrt_depthAverage {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (hloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S)) : ∃ (C : ℝ), 0 ≤ C ∧ Real.rpow 3 (-↑j) * (P.averagingCompetitor h).relativeGradientCoordL2NormSum ≤ C * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

Scale-correct relative-gradient estimate for the overlap averaging competitor. The factor 3^{-j} cancels the inverse overlap scale in the raw gradient bound.