Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseCaccioppoli.CutoffProduct.SplitPairing.VectorFullDual

Coarse-graining support: #

Support.Deterministic.CoarseCaccioppoli.CutoffProduct.SplitPairing.VectorFullDual

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

Full-dual vector split pairing estimates #

This sidecar is the corrected replacement for the projected-vector centered branch in SplitPairing/Vector.lean. The constant branch is unchanged; the centered branch is routed through the full-dual/local-multiscale theorem from CenteredProductFullDual.lean.

source
theorem HCPolySupport.abs_cubeAverage_fluxCutoff_le_sharpNote_of_fullDual_localScales {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : 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 : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hBgConst : 0 ≤ BgConst) (hBgCent : 0 ≤ BgCent) (hBavg : 0 ≤ Bavg) (hC : 0 ≤ C) (hBcirc1 : 0 ≤ Bcirc1) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (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) (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) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * 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) * (↑(Fintype.card (Fin d)) * Bcirc1)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * BuS) * (cubeBesovScaleWeight s Q * BgCent)))

Full-dual/local-multiscale version of the sharp vector split pairing estimate.

source
theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_sharpSplit_of_effectiveConstant {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : 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 : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hBgConst : 0 ≤ BgConst) (hBgCent : 0 ≤ BgCent) (hBavg : 0 ≤ Bavg) (hC : 0 ≤ C) (hBcirc1 : 0 ≤ Bcirc1) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (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) (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 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * Bcirc1)) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * 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 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * Bcirc1))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * BuS) * (cubeBesovScaleWeight s Q * BgCent)))

Effective-constant wrapper for the full-dual/local-multiscale sharp vector split estimate.

source
theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_split_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) {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 : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hBgConst : 0 ≤ BgConst) (hBgCent : 0 ≤ BgCent) (hBavg : 0 ≤ Bavg) (hC : 0 ≤ C) (hBcirc1 : 0 ≤ Bcirc1) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (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) (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) * (↑(Fintype.card (Fin d)) * Bcirc1))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (↑(Fintype.card (Fin d)) * 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) * (↑(Fintype.card (Fin d)) * Bcirc1)))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * BuS) * (cubeBesovScaleWeight s Q * BgCent)))

Full-dual/full-circ version of the sharp vector split pairing estimate.

This is the replacement used by the unconditional Caccioppoli route: the centered cutoff product is controlled directly by full-dual Poincare and the infinite-depth full-circ Besov bounds, with no finite local-multiscale Poincare hypothesis.

source
theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_split_collapsed_sharp_of_constant {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : 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 : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hBgConst : 0 ≤ BgConst) (hBgCent : 0 ≤ BgCent) (hBavg : 0 ≤ Bavg) (hC : 0 ≤ C) (hBcirc1 : 0 ≤ Bcirc1) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (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) (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 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * Bcirc1)) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * 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 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * Bcirc1))) + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * BuS) * (cubeBesovScaleWeight s Q * BgCent)))

Effective-constant wrapper for the full-dual/full-circ sharp vector split estimate.