Coarse-graining support: Support.Besov.Duality.CaccioppoliVectorization #

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

(cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)) = ∑ i : Fin d, cubeBesovPairing Q (fun (x : Vec d) => u x i) fun (x : Vec d) => g x i

|cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, |cubeBesovPairing Q (fun (x : Vec d) => u x i) fun (x : Vec d) => g x i|

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sum_note_rhs_mul_of_uniform_component_bounds_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) :

|cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, ((3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 1 fun (x : Vec d) => u x i) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * B i

theorem HCPolySupport.absCubeAverage_dot_le_componentBounds_twoOne {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 ≤ B i) (hnorm : ∀ (i : Fin d) (N : ℕ), (cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) => g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) :

theorem HCPolySupport.absCubeAverage_dot_le_componentBounds_twoOne_noMeanTerm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 ≤ B i) (hnorm : ∀ (i : Fin d) (N : ℕ), (cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) => g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) :

|cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, (3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 1 fun (x : Vec d) => u x i) * B i

Sharp vectorized two-one pairing bound without the redundant average tail in the flux dual norm.

theorem HCPolySupport.sum_abs_cubeBesovPairing_le_sum_dualFullNorm_mul_of_uniform_component_bounds_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) :

∑ i : Fin d, |cubeBesovPairing Q (fun (x : Vec d) => u x i) fun (x : Vec d) => g x i| ≤ ∑ i : Fin d, (cubeBesovDualFullNorm Q s 2 1 fun (x : Vec d) => u x i) * B i

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sum_dualFullNorm_mul_of_uniform_component_bounds_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) :

|cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, (cubeBesovDualFullNorm Q s 2 1 fun (x : Vec d) => u x i) * B i

theorem HCPolySupport.sum_abs_cubeBesovPairing_le_sum_dualFullNorm_mul_sum_bounds_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) (hdualNonneg : ∀ (i : Fin d), 0 ≤ cubeBesovDualFullNorm Q s 2 1 fun (x : Vec d) => u x i) :

∑ i : Fin d, |cubeBesovPairing Q (fun (x : Vec d) => u x i) fun (x : Vec d) => g x i| ≤ (∑ i : Fin d, cubeBesovDualFullNorm Q s 2 1 fun (x : Vec d) => u x i) * ∑ i : Fin d, B i

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sum_dualFullNorm_mul_sum_bounds_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) (hdualNonneg : ∀ (i : Fin d), 0 ≤ cubeBesovDualFullNorm Q s 2 1 fun (x : Vec d) => u x i) :

|cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ (∑ i : Fin d, cubeBesovDualFullNorm Q s 2 1 fun (x : Vec d) => u x i) * ∑ i : Fin d, B i

theorem HCPolySupport.abs_cubeAverage_vecDot_le_sum_note_rhs_mul_of_uniform_component_bounds_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) :

|cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, ((3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 2 fun (x : Vec d) => u x i) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * B i

theorem HCPolySupport.absCubeAverage_dot_le_componentBounds_twoTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 ≤ B i) (hnorm : ∀ (i : Fin d) (N : ℕ), (cubeBesovDualTestNorm Q s 2 2 N fun (x : Vec d) => g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) :

Documentation