Coarse-graining support: Support.Deterministic.CoarseCaccioppoliLocalBridge

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

theorem HCPolySupport.cubeAverage_vecDot_eq_vecDot_cubeAverageVec_add_cubeAverage_vecDot_fluctuationVec {d : ℕ} (Q : TriadicCube d) (u g : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) : (cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)) = vecDot (cubeAverageVec Q u) (cubeAverageVec Q g) + cubeAverage Q fun (x : Vec d) => vecDot (u x) (cubeFluctuationVec Q g x)

theorem HCPolySupport.abs_vecDot_cubeAverageVec_le_sum_norm_mul_norm {d : ℕ} (Q : TriadicCube d) (u g : Vec d → Vec d) : |vecDot (cubeAverageVec Q u) (cubeAverageVec Q g)| ≤ ∑ i : Fin d, ‖cubeAverage Q fun (x : Vec d) => u x i‖ * ‖cubeAverage Q fun (x : Vec d) => g x i‖

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sum_average_terms_add_note_terms_of_partialBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, ‖cubeAverage Q fun (x : Vec d) => u x i‖ * ‖cubeAverage Q fun (x : Vec d) => g x i‖ + ∑ i : Fin d, (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sum_average_terms_add_sharp_note_terms_of_partialBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, ‖cubeAverage Q fun (x : Vec d) => u x i‖ * ‖cubeAverage Q fun (x : Vec d) => g x i‖ + ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))

Sharp average/fluctuation split for the vector product. Compared with abs_cubeAverage_vecDot_le_sum_average_terms_add_note_terms_of_partialBounds, the fluctuation piece uses the sharp Besov duality bound and therefore does not carry the extra positive average tail on the flux side.

theorem HCPolySupport.abs_cubeAverage_vecDot_le_note_terms_of_partialBounds_of_cubeAverageVec_eq_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (havg : cubeAverageVec Q g = 0) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sum_average_terms_add_note_terms_of_partialBounds_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, ‖cubeAverage Q fun (x : Vec d) => u x i‖ * ‖cubeAverage Q fun (x : Vec d) => g x i‖ + ∑ i : Fin d, (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)

theorem HCPolySupport.abs_cubeAverage_vecDot_le_note_terms_of_partialBounds_of_cubeAverageVec_eq_zero_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (havg : cubeAverageVec Q g = 0) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sharp_note_terms_of_partialBounds_of_cubeAverageVec_eq_zero_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (havg : cubeAverageVec Q g = 0) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))

Sharp centered q = 2 vector pairing bound. The depth-zero negative seminorm absorbs the average contribution, so no separate average tail remains when the second field has zero cube average.