Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.CutoffProduct.SplitPairing.Vector

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

theorem HCPolySupport.abs_cubeAverage_fluxCutoff_le_collapsedNote_of_smoothComponents {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) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate 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) + cubeBesovScaleWeight 1 Q * Bavg) * 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 * Bavg) * (cubeBesovScaleWeight s Q * BgCent)))

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_split_collapsed_sharp_note_terms {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) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate 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)))

Vector projected-Poincare version of the sharp split pairing estimate.

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_split_collapsed_note_terms {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) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate 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) + cubeBesovScaleWeight 1 Q * Bavg) * 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 * Bavg) * (cubeBesovScaleWeight s Q * BgCent)))

theorem HCPolySupport.abs_cubeAverage_vectorDot_scalarMultiply_le_split_collapsed_sharp_note_of_vector {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) (hBcircS : 0 ≤ BcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Bavg) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Bu1) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ BuS) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate 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 sharp vector split estimate.

theorem HCPolySupport.abs_cubeAverage_vecDot_scalar_smul_le_split_energy_coefficients_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {Aflux1 AfluxS Aavg Acirc1 AcircS E 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) (hAavg : 0 ≤ Aavg) (hE : 0 ≤ E) (hC : 0 ≤ C) (havg : ‖cubeAverageVec Q flux‖ ≤ Aavg * E) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Aflux1 * E) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ AfluxS * E) (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 ≤ Acirc1 * E) (hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ AcircS * E) (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) * (Acirc1 * E))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (AcircS * E)))) ≤ BgCent) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * ((3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) + cubeBesovScaleWeight 1 Q * (Aavg * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * C * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * ((3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) + cubeBesovScaleWeight s Q * (Aavg * E)) * (cubeBesovScaleWeight s Q * BgCent)))

Energy-coefficient form of the split local Caccioppoli pairing.

The previous theorem keeps the five Besov/average bounds as raw constants. This wrapper records the next downstream shape: each of those bounds is a coefficient times one common local energy scale E. The radius/coefficient bookkeeping can now substitute the Chapter-2/coarse-Poincare coefficients without reopening the cutoff-product proof.

theorem HCPolySupport.abs_cubeAverage_fluxCutoff_le_energyCoeffSplit_of_smoothVector {d : ℕ} (Q : TriadicCube d) (s : ℝ) (flux : Vec d → Vec d) (u : Vec d → ℝ) (G ξ : Vec d → Vec d) {Aflux1 AfluxS Aavg Acirc1 AcircS E 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) (hAavg : 0 ≤ Aavg) (hE : 0 ≤ E) (hC : 0 ≤ C) (hAcircS : 0 ≤ AcircS) (havg : ‖cubeAverageVec Q flux‖ ≤ Aavg * E) (hfluxNeg1 : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q 1 N flux ≤ Aflux1 * E) (hfluxNegS : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N flux ≤ AfluxS * E) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate 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) ≤ Acirc1 * E) (hGcircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * E) (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) * (Acirc1 * E))) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * (AcircS * E)))) ≤ BgCent) : |cubeAverage Q fun (x : Vec d) => vecDot (flux x) (u x • ξ x)| ≤ ↑d * ((3 ^ (↑d + 1) * (cubeBesovScaleWeight (-1) Q * (Aflux1 * E)) + cubeBesovScaleWeight 1 Q * (Aavg * E)) * BgConst) + (↑d * (Aavg * E * (cubeLpNorm Q ⊤ ξ * (3 / 2 * (↑(Fintype.card (Fin d)) * C) * 3 ^ (↑d + 1) * (Acirc1 * E)))) + ↑d * ((3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * (AfluxS * E)) + cubeBesovScaleWeight s Q * (Aavg * E)) * (cubeBesovScaleWeight s Q * BgCent)))

Vector projected-Poincare version of abs_cubeAverage_vecDot_scalar_smul_le_split_energy_coefficients_of_contDiff_component_bound.

This is the coefficient-times-energy wrapper for the descendant/local Caccioppoli pairing used by the harmonic-vector endpoint.