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

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

Exact scalar overlap Besov–Gagliardo comparison

This module identifies the square of the exact ENNReal overlap Besov seminorm at p = q = 2 with the supremum of the established finite-depth scalar overlap seminorm squares. It then transports the two existing finite-depth Besov–Gagliardo comparisons to the exact infinite-depth kernel.

The only analytic input used by the identification is concrete parent-cube L² membership. It supplies both the root integrability and every enlarged overlap-cube integrability certificate required by the exact kernel.

noncomputable def HCPolySupport.exactOverlapScalarTwoParameters (s : ↑(Set.Ioo 0 1)) : ExactOverlapFiniteParameters

Exact scalar overlap parameters at p = q = 2 and fractional order 0 < s < 1.

Equations

• HCPolySupport.exactOverlapScalarTwoParameters s = { s := ↑s, p := 2, q := 2, admissible := ⋯ }

theorem HCPolySupport.exactOverlapScalarSeminormTwo_sq_eq_iSup_partialSeminorm {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (hmem : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : exactOverlapFiniteSeminorm (exactOverlapScalarTwoParameters s) Q u hu ^ 2 = ⨆ (N : ℕ), ENNReal.ofReal (cubeBesovOverlapPartialSeminorm Q (↑s) 2 2 N u) ^ 2

Under concrete parent-cube L² membership, the square of the exact p = q = 2 scalar overlap seminorm is the supremum of the embedded squares of all finite-depth scalar overlap seminorms.

theorem HCPolySupport.exactOverlapScalarSeminormTwo_sq_le_gagliardo {d : ℕ} [NeZero d] (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (humeas : Measurable u) (hmem : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : exactOverlapFiniteSeminorm (exactOverlapScalarTwoParameters s) Q u hu ^ 2 ≤ 2 * 3 ^ d * Gagliardo.cubeGagliardoESeminorm Q (↑s) 2 u ^ 2

Exact scalar overlap Besov-to-Gagliardo comparison at p = q = 2, with the finite dimensional constant from the established finite-depth estimate.

theorem HCPolySupport.gagliardo_sq_le_exactOverlapScalarSeminormTwo {d : ℕ} [NeZero d] (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (u : Vec d → ℝ) (hu : ExactOverlapIntegrable Q u) (humeas : Measurable u) (hmem : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : Gagliardo.cubeGagliardoESeminorm Q (↑s) 2 u ^ 2 ≤ Gagliardo.gagliardoBesovLowerConstant d ^ 2 * exactOverlapFiniteSeminorm (exactOverlapScalarTwoParameters s) Q u hu ^ 2

Gagliardo-to-exact-scalar-overlap comparison at p = q = 2, with the finite dimensional constant from the established shell estimate.