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

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

Overlap-counting integral bound (U3)

Summing set-lintegrals over the enlarged cubes of a depth-j center family costs at most the bounded-overlap constant 3^d times one set-lintegral over the parent product cube.

theorem HCPolySupport.Gagliardo.measurableSet_overlap_prod {d : ℕ} (S : TriadicCube d) : MeasurableSet (ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S)

The product E_S ×ˢ E_S of an enlarged center cube is measurable.

theorem HCPolySupport.Gagliardo.sum_indicator_overlap_prod_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (z : Vec d × Vec d) : ∑ S ∈ ScalarOverlap.centersAtDepth Q j, (ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S).indicator (fun (x : Vec d × Vec d) => 1) z ≤ 3 ^ d * (cubeSet Q ×ˢ cubeSet Q).indicator (fun (x : Vec d × Vec d) => 1) z

Pointwise overlap count on pairs: a pair lies in at most 3^d of the products E_S ×ˢ E_S, and only when it lies in Q ×ˢ Q.

theorem HCPolySupport.Gagliardo.sum_setLIntegral_overlap_prod_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (ν : MeasureTheory.Measure (Vec d × Vec d)) {f : Vec d × Vec d → ENNReal} (hf : Measurable f) : ∑ S ∈ ScalarOverlap.centersAtDepth Q j, ∫⁻ (z : Vec d × Vec d) in ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S, f z ∂ν ≤ 3 ^ d * ∫⁻ (z : Vec d × Vec d) in cubeSet Q ×ˢ cubeSet Q, f z ∂ν

U3 (overlap-counting integral bound): for any measure ν on pairs and any measurable integrand, the depth-j family of product cubes is summable at the cost of the overlap constant 3^d.