Coarse-graining support: Support.Sobolev.Fractional.ExactOverlapFinitePHomogeneity

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

Scalar homogeneity of exact overlap depth energies

The normalized overlap average and the resulting one-depth energy commute exactly with multiplication by a real scalar.

theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapDepthENorm_const_smul_rpow {d : ℕ} (Q : TriadicCube d) (q : FiniteLpExponent) (F : Vec d → Vec d) (c : ℝ) (hF : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) q.exponent (normalizedCubeMeasure Q)) (j : ℕ) : cubeEuclideanPositiveBesovOverlapDepthENorm Q q (fun (x : Vec d) => c • F x) j ^ q.exponent.toReal = ‖c‖ₑ ^ q.exponent.toReal * cubeEuclideanPositiveBesovOverlapDepthENorm Q q F j ^ q.exponent.toReal

The exact powered overlap energy at a fixed depth is homogeneous under real scalar multiplication, without a depth or cardinality loss.