Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.CutoffProduct.CenteredProductFullDual
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Full-dual centered cutoff-product estimates #
This sidecar keeps CenteredProduct.lean under the preferred size ceiling while
recording the corrected full-dual replacement for the L² half of the centered
cutoff-product estimate. The local-multiscale theorem below also discharges
the positive-Besov scalar tail from the matching finite-depth Poincare estimate,
which is the analytic input needed by the Section 3.1 small-cube bridge.
theorem
HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_centered_scalar_smul_le_fullDualL2_cutoff_terms
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(N : ℕ)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{B C Bcirc1 Bpos : ℝ}
(hB : 0 ≤ B)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hfull : CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(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)
(hs1 : s < 1)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(hGcirc1 : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc1)
(hpos : cubeBesovPositiveScalarPartialSeminormTwo Q s N (cubeFluctuation Q u) ≤ Bpos)
:
theorem
HCPolySupport.positivePartialSeminormTwo_centeredScalarMultiply_le_fullDual_multiscaleCutoff
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(N : ℕ)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{B C Bcirc1 BcircS : ℝ}
(hB : 0 ≤ B)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hfull : CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hlocal : CubeLocalMultiscalePoincareVectorEstimate Q (3 / 2 * C * 3 ^ (↑d + 1)) (cubeFluctuation Q u) G N)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(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)
(hs0 : 0 < s)
(hs1 : s < 1)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(hBcircS : 0 ≤ BcircS)
(hGcirc1 : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc1)
(hGcircS : ∀ (i : Fin d), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ BcircS)
:
(cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * BcircS))))
theorem
HCPolySupport.cubeBesovDualTestNorm_component_centered_smul_le_dualCutoff
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(N : ℕ)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
(i : Fin d)
{B C Bcirc1 BcircS : ℝ}
(hB : 0 ≤ B)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hfull : ∀ (M : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G M)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(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)
(hs0 : 0 < s)
(hs1 : s < 1)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(hBcircS : 0 ≤ BcircS)
(hGcirc1 : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc1)
(hGcircS : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 M fun (x : Vec d) => G x i) ≤ BcircS)
:
(cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) =>
cubeFluctuationVec Q (fun (y : Vec d) => (u y - cubeAverage Q u) • ξ y) x i) ≤ cubeBesovScaleWeight s Q * (2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * BcircS)))))
Componentwise dual-test bound for the centered cutoff product, using the full-dual Poincare estimate and the full-circ infinite-depth positive Poincare route.
theorem
HCPolySupport.cubeBesovPositiveVectorSeminormTwo_centered_scalar_smul_le_fullDualL2_cutoff_terms
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{B C Bcirc1 Bpos : ℝ}
(hB : 0 ≤ B)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(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)
(hs1 : s < 1)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(hGcirc1 : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc1)
(hpos : ∀ (N : ℕ), cubeBesovPositiveScalarPartialSeminormTwo Q s N (cubeFluctuation Q u) ≤ Bpos)
:
theorem
HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_noteTerms
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{Bu Bg Bavg Bcirc1 C : ℝ}
(hs : 0 < s)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(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 - cubeAverage Q u) • ξ x) ≤ Bg)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hGcirc1 : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc1)
:
|cubeAverage Q fun (x : Vec d) => vecDot (flux x) ((u x - cubeAverage Q u) • ξ x)| ≤ ↑d * (Bavg * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1)))) + ↑d * ((3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * Bavg) * (cubeBesovScaleWeight s Q * Bg))
theorem
HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_sharpNoteTerms
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{Bu Bg Bavg Bcirc1 C : ℝ}
(hs : 0 < s)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(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 - cubeAverage Q u) • ξ x) ≤ Bg)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hGcirc1 : ∀ (i : Fin d) (M : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 M fun (x : Vec d) => G x i) ≤ Bcirc1)
:
theorem
HCPolySupport.abs_cubeAverage_vecDot_centered_scalar_smul_le_collapsed_sharp_note_terms_of_dualFull_fullCirc
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{Bu Bg Bavg Bcirc1 BcircS B C : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(hBcircS : 0 ≤ BcircS)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate 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 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc1)
(hGcircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ BcircS)
(hBg_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * BcircS)))) ≤ Bg)
:
theorem
HCPolySupport.abs_cubeAverage_vectorDot_centered_scalar_smul_le_collapsed_sharp_of_dualFull
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(flux : Vec d → Vec d)
(u : Vec d → ℝ)
(G ξ : Vec d → Vec d)
{Bu Bavg Bcirc1 BcircS B C Bg : ℝ}
(hB : 0 ≤ B)
(hs0 : 0 < s)
(hs1 : s < 1)
(hflux : MeasureTheory.MemLp flux 2 (normalizedCubeMeasure Q))
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q))
(hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hBavg : 0 ≤ Bavg)
(hC : 0 ≤ C)
(hBcirc1 : 0 ≤ Bcirc1)
(hBcircS : 0 ≤ BcircS)
(havg : ‖cubeAverageVec Q flux‖ ≤ Bavg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ Bu)
(hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hlocal : ∀ (N : ℕ), CubeLocalMultiscalePoincareVectorEstimate Q (3 / 2 * C * 3 ^ (↑d + 1)) (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 : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Bcirc1)
(hGcircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ BcircS)
(hBg_bound :
2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * C * 3 ^ (↑d + 1) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * BcircS)))) ≤ Bg)
: