Coarse-graining support: Support.Deterministic.WeakNormInterfaces.Bounds

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

theorem HCPolySupport.descendantsAverage_four_mul_sum_vecNormSq_cubeAverageVec_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (u₁ u₂ u₃ u₄ : Vec d → Vec d) : (descendantsAverage Q j fun (R : TriadicCube d) => 4 * (vecNormSq (cubeAverageVec R u₁) + vecNormSq (cubeAverageVec R u₂) + vecNormSq (cubeAverageVec R u₃) + vecNormSq (cubeAverageVec R u₄))) = 4 * (cubeBesovNegativeVectorDepthAverage Q u₁ j + cubeBesovNegativeVectorDepthAverage Q u₂ j + cubeBesovNegativeVectorDepthAverage Q u₃ j + cubeBesovNegativeVectorDepthAverage Q u₄ j)

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_le_two_mul_sum_of_cubeTerms_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) (predictor additivity lowScale tail : TriadicCube d → Vec d) (hdecomp : ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R u = predictor R + additivity R + lowScale R + tail R) : cubeBesovNegativeVectorDepthSeminorm Q s u j ≤ 2 * (Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (predictor R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (additivity R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (lowScale R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (tail R)))

Depthwise weighted weak-norm split for cube-indexed pieces. This is the form used by the Section 5.3 analytic estimates before the predictor, additivity, low-scale, and tail contributions have been represented as global vector fields.

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_le_two_mul_self_add_const_of_cubeAverageVec_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) (w u : Vec d → Vec d) (c : Vec d) (hdecomp : ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = cubeAverageVec R u + c) : cubeBesovNegativeVectorDepthSeminorm Q s w j ≤ 2 * (cubeBesovNegativeVectorDepthSeminorm Q s u j + Real.rpow 3 (-s * ↑j) * √(vecNormSq c))

Low-scale constant-tail split at one depth. If the descendant averages of w are the averages of u plus a fixed vector c, then the depth contribution of w is bounded by the depth contribution of u plus the constant tail.

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_le_two_mul_sum_of_cubeAverageVec_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) (u u₁ u₂ u₃ u₄ : Vec d → Vec d) (hdecomp : ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R u = cubeAverageVec R u₁ + cubeAverageVec R u₂ + cubeAverageVec R u₃ + cubeAverageVec R u₄) : cubeBesovNegativeVectorDepthSeminorm Q s u j ≤ 2 * (cubeBesovNegativeVectorDepthSeminorm Q s u₁ j + cubeBesovNegativeVectorDepthSeminorm Q s u₂ j + cubeBesovNegativeVectorDepthSeminorm Q s u₃ j + cubeBesovNegativeVectorDepthSeminorm Q s u₄ j)

Depthwise weak-norm triangle inequality obtained from a four-term decomposition of descendant cube averages.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : 0 ≤ cubeBesovNegativeVectorPartialSeminorm Q s N u

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_of_depthAverage_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) {A : ℕ → ℝ} (hA : ∀ j ∈ Finset.range (N + 1), cubeBesovNegativeVectorDepthAverage Q u j ≤ A j) : cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) * √(A j)

Finite q = 1 weak-norm control from depthwise descendant-average controls. This is the direct weighted-sum form of the negative Besov estimate: no ellipticity constants or Ch5 packaging enter.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_of_four_term_depthAverage_decomposition {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) (predictor additivity lowScale tail : ℕ → TriadicCube d → Vec d) (hdecomp : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R u = predictor j R + additivity j R + lowScale j R + tail j R) : cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => 4 * (vecNormSq (predictor j R) + vecNormSq (additivity j R) + vecNormSq (lowScale j R) + vecNormSq (tail j R)))

Finite q = 1 negative weak-norm bound from a four-term decomposition of the descendant cube averages at every depth.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_two_mul_sum_of_cubeTerms_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) (predictor additivity lowScale tail : ℕ → TriadicCube d → Vec d) (hdecomp : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R u = predictor j R + additivity j R + lowScale j R + tail j R) : cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ 2 * (∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (predictor j R)) + ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (additivity j R)) + ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (lowScale j R)) + ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (tail j R)))

Finite q = 1 negative weak-norm split for cube-indexed analytic pieces at each depth. This is the note-facing weighted Cauchy/Minkowski step for the four contributions in the Section 5.3 maximizer estimate.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_cubeTerms_on_filter_add_complement {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) (high : ℕ → Prop) [DecidablePred high] (predictor additivity lowScale tail : ℕ → TriadicCube d → Vec d) (hdecomp : ∀ j ∈ Finset.range (N + 1), high j → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R u = predictor j R + additivity j R + lowScale j R + tail j R) : cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ ∑ j ∈ Finset.range (N + 1) with high j, 2 * (Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (predictor j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (additivity j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (lowScale j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (tail j R))) + ∑ j ∈ Finset.range (N + 1) with ¬high j, cubeBesovNegativeVectorDepthSeminorm Q s u j

Finite high/low split for the negative weak norm. On the selected depths high, a four-term cube-indexed decomposition is used; on the complementary depths the original depth contribution is left untouched. This is the finite form of the high-scale/low-scale split in the Section 5.3 maximizer proof.

theorem HCPolySupport.sum_filter_cubeBesovNegativeVectorDepthSeminorm_le_two_mul_self_add_const_of_cubeAverageVec_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (low : ℕ → Prop) [DecidablePred low] (w u : Vec d → Vec d) (c : Vec d) (hdecomp : ∀ j ∈ Finset.range (N + 1), low j → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = cubeAverageVec R u + c) : ∑ j ∈ Finset.range (N + 1) with low j, cubeBesovNegativeVectorDepthSeminorm Q s w j ≤ 2 * (∑ j ∈ Finset.range (N + 1) with low j, cubeBesovNegativeVectorDepthSeminorm Q s u j + ∑ j ∈ Finset.range (N + 1) with low j, Real.rpow 3 (-s * ↑j) * √(vecNormSq c))

Filtered low-scale constant-tail estimate. On a selected set of depths, if the averages of w equal the averages of u plus a fixed vector c, then the filtered contribution of w is controlled by the filtered contribution of u and the weighted constant tail.

theorem HCPolySupport.sum_filter_triadic_weight_mul_const_sqrt_eq {d : ℕ} (s : ℝ) (N : ℕ) (low : ℕ → Prop) [DecidablePred low] (c : Vec d) : ∑ j ∈ Finset.range (N + 1) with low j, Real.rpow 3 (-s * ↑j) * √(vecNormSq c) = (∑ j ∈ Finset.range (N + 1) with low j, Real.rpow 3 (-s * ↑j)) * √(vecNormSq c)

theorem HCPolySupport.sum_filter_triadic_weight_mul_const_sqrt_le_of_weight_sum_le {d : ℕ} (s : ℝ) (N : ℕ) (low : ℕ → Prop) [DecidablePred low] (c : Vec d) {tailWeight : ℝ} (hWeight : ∑ j ∈ Finset.range (N + 1) with low j, Real.rpow 3 (-s * ↑j) ≤ tailWeight) : ∑ j ∈ Finset.range (N + 1) with low j, Real.rpow 3 (-s * ↑j) * √(vecNormSq c) ≤ tailWeight * √(vecNormSq c)

theorem HCPolySupport.sum_range_filter_not_lt_triadic_weight_mul_const_sqrt_le_geometric_tail {d : ℕ} (s : ℝ) (N L : ℕ) (c : Vec d) (hs : 0 < s) : ∑ j ∈ Finset.range (N + 1) with ¬j < L, Real.rpow 3 (-s * ↑j) * √(vecNormSq c) ≤ Real.rpow 3 (-s * ↑L) * (1 - Real.rpow 3 (-s))⁻¹ * √(vecNormSq c)

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_cubeTerms_on_filter_add_low_self_add_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (w lowField : Vec d → Vec d) (c : Vec d) (high : ℕ → Prop) [DecidablePred high] (predictor additivity lowScale tail : ℕ → TriadicCube d → Vec d) (hhigh : ∀ j ∈ Finset.range (N + 1), high j → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = predictor j R + additivity j R + lowScale j R + tail j R) (hlow : ∀ j ∈ Finset.range (N + 1), ¬high j → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = cubeAverageVec R lowField + c) : cubeBesovNegativeVectorPartialSeminorm Q s N w ≤ ∑ j ∈ Finset.range (N + 1) with high j, 2 * (Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (predictor j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (additivity j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (lowScale j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (tail j R))) + 2 * (∑ j ∈ Finset.range (N + 1) with ¬high j, cubeBesovNegativeVectorDepthSeminorm Q s lowField j + ∑ j ∈ Finset.range (N + 1) with ¬high j, Real.rpow 3 (-s * ↑j) * √(vecNormSq c))

Finite high-scale decomposition plus low-scale constant-tail split. This is a closer finite Lean analogue of the first displayed split in the deterministic maximizer proof: high depths get the analytic four-term decomposition, while low depths become a raw low-scale norm plus the p₀/q₀ constant tail.

theorem HCPolySupport.negativeVectorPartial_le_cutoffTerms_and_geometricTail {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N L : ℕ) (w lowField : Vec d → Vec d) (c : Vec d) (predictor additivity lowScale tail : ℕ → TriadicCube d → Vec d) (hs : 0 < s) (hhigh : ∀ j ∈ Finset.range (N + 1), j < L → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = predictor j R + additivity j R + lowScale j R + tail j R) (hlow : ∀ j ∈ Finset.range (N + 1), L ≤ j → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = cubeAverageVec R lowField + c) : cubeBesovNegativeVectorPartialSeminorm Q s N w ≤ ∑ j ∈ Finset.range (N + 1) with j < L, 2 * (Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (predictor j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (additivity j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (lowScale j R)) + Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (tail j R))) + 2 * (∑ j ∈ Finset.range (N + 1) with ¬j < L, cubeBesovNegativeVectorDepthSeminorm Q s lowField j + Real.rpow 3 (-s * ↑L) * (1 - Real.rpow 3 (-s))⁻¹ * √(vecNormSq c))

Cutoff version of the finite maximizer weak-norm split. Depths j < L are controlled by the four analytic cube-indexed pieces, while depths L ≤ j contribute a raw low-scale norm and a geometric constant tail.

theorem HCPolySupport.negativePartialSeminorm_le_shiftedGapSum_add_lowSelf_add_geometricConstant {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N L : ℕ) (w lowField : Vec d → Vec d) (c : Vec d) (predictor additivity lowScale tail : ℕ → TriadicCube d → Vec d) (sPred sAdd sLow sTail Cpred Cadd Clow Ctail : ℝ) (predGap addGap lowGap tailGap : ℕ → ℝ) (hs : 0 < s) (hCpred : 0 ≤ Cpred) (hCadd : 0 ≤ Cadd) (hClow : 0 ≤ Clow) (hCtail : 0 ≤ Ctail) (hhigh : ∀ j ∈ Finset.range (N + 1), j < L → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = predictor j R + additivity j R + lowScale j R + tail j R) (hlow : ∀ j ∈ Finset.range (N + 1), L ≤ j → ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R w = cubeAverageVec R lowField + c) (hPred : ∀ j ∈ {j ∈ Finset.range (N + 1) | j < L}, (descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (predictor j R)) ≤ (Cpred * Real.rpow 3 (sPred * ↑j)) ^ 2 * predGap j) (hAdd : ∀ j ∈ {j ∈ Finset.range (N + 1) | j < L}, (descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (additivity j R)) ≤ (Cadd * Real.rpow 3 (sAdd * ↑j)) ^ 2 * addGap j) (hLow : ∀ j ∈ {j ∈ Finset.range (N + 1) | j < L}, (descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (lowScale j R)) ≤ (Clow * Real.rpow 3 (sLow * ↑j)) ^ 2 * lowGap j) (hTail : ∀ j ∈ {j ∈ Finset.range (N + 1) | j < L}, (descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (tail j R)) ≤ (Ctail * Real.rpow 3 (sTail * ↑j)) ^ 2 * tailGap j) : cubeBesovNegativeVectorPartialSeminorm Q s N w ≤ 2 * (Cpred * ∑ j ∈ Finset.range (N + 1) with j < L, Real.rpow 3 (-(s - sPred) * ↑j) * √(predGap j) + Cadd * ∑ j ∈ Finset.range (N + 1) with j < L, Real.rpow 3 (-(s - sAdd) * ↑j) * √(addGap j) + Clow * ∑ j ∈ Finset.range (N + 1) with j < L, Real.rpow 3 (-(s - sLow) * ↑j) * √(lowGap j) + Ctail * ∑ j ∈ Finset.range (N + 1) with j < L, Real.rpow 3 (-(s - sTail) * ↑j) * √(tailGap j)) + 2 * (∑ j ∈ Finset.range (N + 1) with ¬j < L, cubeBesovNegativeVectorDepthSeminorm Q s lowField j + Real.rpow 3 (-s * ↑L) * (1 - Real.rpow 3 (-s))⁻¹ * √(vecNormSq c))

Finite cutoff maximizer estimate with the high-scale analytic pieces already converted to shifted weak-norm gap sums. This combines the four-term cube-average decomposition, the low-scale constant-tail split, and the depthwise estimates with growth factors 3^{s'j}.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_two_mul_sum_of_cubeAverageVec_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u u₁ u₂ u₃ u₄ : Vec d → Vec d) (hdecomp : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R u = cubeAverageVec R u₁ + cubeAverageVec R u₂ + cubeAverageVec R u₃ + cubeAverageVec R u₄) : cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ 2 * (cubeBesovNegativeVectorPartialSeminorm Q s N u₁ + cubeBesovNegativeVectorPartialSeminorm Q s N u₂ + cubeBesovNegativeVectorPartialSeminorm Q s N u₃ + cubeBesovNegativeVectorPartialSeminorm Q s N u₄)

Finite q = 1 negative weak-norm split from a four-term decomposition of all descendant cube averages. This is the weighted weak-norm Cauchy/Minkowski step needed in the Section 5.3 weak-norm estimate.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : 0 ≤ cubeBesovNegativeVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 = ∑ j ∈ Finset.range (N + 1), cubeBesovNegativeVectorDepthSeminorm Q s u j ^ 2

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_anti_mono_exponent {d : ℕ} (Q : TriadicCube d) {a b : ℝ} (hab : a ≤ b) (N : ℕ) (u : Vec d → Vec d) : cubeBesovNegativeVectorPartialSeminormTwo Q b N u ≤ cubeBesovNegativeVectorPartialSeminormTwo Q a N u

theorem HCPolySupport.finset_sqrt_sum_sq_le_sum_of_nonneg {ι : Type u_1} (s : Finset ι) (A : ι → ℝ) (hA : ∀ i ∈ s, 0 ≤ A i) : √(∑ i ∈ s, A i ^ 2) ≤ ∑ i ∈ s, A i

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_le_partialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ cubeBesovNegativeVectorPartialSeminorm Q s N u

theorem HCPolySupport.cubeBesovNegativeVectorSeminorm_le_of_partialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ B) : cubeBesovNegativeVectorSeminorm Q s u ≤ B

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_seminorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm Q s N u)) (N : ℕ) : cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ cubeBesovNegativeVectorSeminorm Q s u

theorem HCPolySupport.cubeBesovNegativeVectorSeminorm_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm Q s N u)) : 0 ≤ cubeBesovNegativeVectorSeminorm Q s u

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_le_of_partialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ B) : cubeBesovNegativeVectorSeminormTwo Q s u ≤ B

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_anti_mono_exponent_of_bddAbove {d : ℕ} (Q : TriadicCube d) {a b : ℝ} (hab : a ≤ b) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q a N u)) : cubeBesovNegativeVectorSeminormTwo Q b u ≤ cubeBesovNegativeVectorSeminormTwo Q a u

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_le_of_qone_partialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ B) : cubeBesovNegativeVectorSeminormTwo Q s u ≤ B