Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.CutoffProduct.SplitPairing.Scalar #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_split_collapsed_note_terms_of_contDiff_component_bound
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u g : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu1 BuS Bavg Bcirc1 BcircS B C BgConst BgCent : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBgConst : 0 ≤ BgConst)
(hBgCent : 0 ≤ BgCent)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1)
(hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hgCirc1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc1)
(hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ BcircS)
(hBgConst_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ BgConst)
(hBgCent_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * Bcirc1)) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * BcircS))) ≤ BgCent)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * ((3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * Bu1) + cubeBesovScaleWeight 1 Q * Bavg) * BgConst) + (↑d * (Bavg * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * Bcirc1))) + ↑d * ((3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * BuS) + cubeBesovScaleWeight s Q * Bavg) * (cubeBesovScaleWeight s Q * BgCent)))
theorem
HCPolySupport.abs_cubeAverage_fluxCutoff_le_sharpNote_of_smoothBound
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u g : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu1 BuS Bavg Bcirc1 BcircS B C BgConst BgCent : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBgConst : 0 ≤ BgConst)
(hBgCent : 0 ≤ BgCent)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1)
(hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N)
(hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i)
(hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B)
(hgCirc1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Bcirc1)
(hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ BcircS)
(hBgConst_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ BgConst)
(hBgCent_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * Bcirc1)) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * BcircS))) ≤ BgCent)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * Bu1) * BgConst) + (↑d * (Bavg * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * Bcirc1))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * BuS) * (cubeBesovScaleWeight s Q * BgCent)))
Sharp split pairing estimate. The constant branch uses only the negative Besov circ norm of the flux, matching the LaTeX small-cube line.