Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.CutoffProduct.LocalPairing #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_collapsed_average_note_terms_of_partialBounds
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu Bg Bavg : ℝ}
(hs : 0 < s)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x • ξ x) ≤ Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (Bavg * (cubeLpNorm Q ⊤ ξ * cubeLpNorm Q 2 u)) + ↑d * ((3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * Bavg) * (cubeBesovScaleWeight s Q * Bg))
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_collapsed_sharp_average_note_terms_of_partialBounds
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu Bg Bavg : ℝ}
(hs : 0 < s)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x • ξ x) ≤ Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (Bavg * (cubeLpNorm Q ⊤ ξ * cubeLpNorm Q 2 u)) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))
Sharp local pairing estimate. This is the same average/fluctuation split
as abs_cubeAverage_vecDot_scalar_smul_le_collapsed_average_note_terms_of_partialBounds,
but the fluctuation piece uses the circ-only negative Besov duality bound, so
no positive-average tail is present in the Besov term.
theorem
HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_collapsed_sharp_average_note_terms_of_dualTestBounds
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu Bg Bavg : ℝ}
(hs : 0 < s)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hdual :
∀ (i : Fin d) (N : ℕ),
(cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) => cubeFluctuationVec Q (fun (y : Vec d) => u y • ξ y) x i) ≤ cubeBesovScaleWeight s Q * Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * (Bavg * (cubeLpNorm Q ⊤ ξ * cubeLpNorm Q 2 u)) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))
Sharp local pairing estimate with the positive cutoff-product control stated directly as componentwise dual-test bounds.
theorem
HCPolySupport.abs_cubeAverage_vecDot_const_scalar_smul_le_collapsed_note_terms_of_componentDualBounds
{d : ℕ}
(Q : TriadicCube d)
(flux ξ : Vec d → Vec d)
(c : ℝ)
{Bu Bg Bavg : ℝ}
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu)
(hnorm : ∀ (i : Fin d) (N : ℕ), (cubeBesovDualTestNorm Q 1 2 1 N fun (x : Vec d) => c * ξ x i) ≤ Bg)
(hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => c * ξ x i)
:
theorem
HCPolySupport.abs_cubeAverage_vecDot_const_scalar_smul_le_collapsed_sharp_note_terms_of_componentDualBounds
{d : ℕ}
(Q : TriadicCube d)
(flux ξ : Vec d → Vec d)
(c : ℝ)
{Bu Bg : ℝ}
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu)
(hnorm : ∀ (i : Fin d) (N : ℕ), (cubeBesovDualTestNorm Q 1 2 1 N fun (x : Vec d) => c * ξ x i) ≤ Bg)
(hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => c * ξ x i)
:
Sharp constant-piece pairing estimate. This is the LaTeX
[a∇u]_{B^{-1}} line: the full negative Besov dual norm is controlled by the
negative circ norm alone, so the flux side contributes only the
cubeBesovScaleWeight (-1) factor.
theorem
HCPolySupport.abs_cubeAverage_fluxMeanCutoff_le_collapsedNote_of_smoothBound
{d : ℕ}
(Q : TriadicCube d)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu Bavg B Bg : ℝ}
(hB : 0 ≤ B)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu)
(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)
(hBg_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (cubeAverage Q u • ξ x)| ≤ ↑d * ((3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * Bu) + cubeBesovScaleWeight 1 Q * Bavg) * Bg)
theorem
HCPolySupport.abs_cubeAverage_vectorDot_cubeAverage_scalar_smul_le_collapsed_sharp_note_terms
{d : ℕ}
(Q : TriadicCube d)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(ξ : Vec d → Vec d)
{Bu B Bg : ℝ}
(hB : 0 ≤ B)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu)
(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)
(hBg_bound : cubeLpNorm Q 2 u * (B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ) ≤ Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) (cubeAverage Q u • ξ x)| ≤ ↑d * (3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * Bu) * Bg)
Sharp constant-piece estimate after bounding the cutoff dual-test norm by
the quantitative derivative bound. This is the direct Lean counterpart of
the LaTeX bound
C 3^k Λ_1(R)^{1/2} |u_R| E_R, before the local mean is bounded by the
local L² norm.
theorem
HCPolySupport.cubeLpNorm_two_le_note_rhs_of_meanZero_projectedDualMeanZeroPoincareEstimate
{d : ℕ}
(Q : TriadicCube d)
(N : ℕ)
(v g : Vec d → ℝ)
{C : ℝ}
(hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q))
(hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C v g N)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(havg : cubeAverage Q v = 0)
(hC : 0 ≤ C)
: