Coarse-graining support: Support.Deterministic.WeakNormInterfacesQTwo

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

q = 2 deterministic weak-norm recursion lemmas

This file records the first note-facing scale-splitting identities for the vector-valued negative Besov wrappers used in the deterministic Chapter-3 right- hand-side argument.

@[simp]

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_depth_zero {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) : cubeBesovNegativeVectorDepthAverage Q u 0 = vecNormSq (cubeAverageVec Q u)

theorem HCPolySupport.sq_cubeBesovNegativeVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q s u j ^ 2 = Real.rpow 3 (-s * ↑j) ^ 2 * cubeBesovNegativeVectorDepthAverage Q u j

theorem HCPolySupport.sq_cubeBesovNegativeVectorDepthSeminorm_le_of_depthAverage_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) {A : ℝ} (hA : cubeBesovNegativeVectorDepthAverage Q u j ≤ A) : cubeBesovNegativeVectorDepthSeminorm Q s u j ^ 2 ≤ Real.rpow 3 (-s * ↑j) ^ 2 * A

Squared depth contribution controlled by a descendant-average upper bound. This is the weighted q = 2 analogue of the finite q = 1 estimate in WeakNormInterfaces.

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_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) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 ≤ ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) ^ 2 * A j

Finite q = 2 weak-norm control from depthwise descendant-average controls, kept in squared form to match the Cauchy/energy estimates used in Section 5.3.

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_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) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 ≤ ∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-s * ↑j) ^ 2 * descendantsAverage Q j fun (R : TriadicCube d) => 4 * (vecNormSq (predictor j R) + vecNormSq (additivity j R) + vecNormSq (lowScale j R) + vecNormSq (tail j R))

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

@[simp]

theorem HCPolySupport.sq_cubeBesovNegativeVectorDepthSeminorm_depth_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) : cubeBesovNegativeVectorDepthSeminorm Q s u 0 ^ 2 = vecNormSq (cubeAverageVec Q u)

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_succ_eq_descendantsAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q u (j + 1) = descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorDepthAverage R u j

theorem HCPolySupport.sq_cubeBesovNegativeVectorDepthSeminorm_succ_eq_discount_mul_descendantsAverage {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q s u (j + 1) ^ 2 = Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorDepthSeminorm R s u j ^ 2

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_succ_eq_top_add_descendantsAverage {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 = vecNormSq (cubeAverageVec Q u) + Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2