Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.AveragedLocal.DescendantsAverage

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

theorem HCPolySupport.descendantAverage_sq_negativeVectorSeminorm_le_discountNext_error {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) (E : TriadicCube d → ℝ) (hlocal : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => cubeBesovNegativeVectorSeminormTwo S s u ^ 2) + E R) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovNegativeVectorSeminormTwo R s u ^ 2) ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q (j + 1) fun (R : TriadicCube d) => cubeBesovNegativeVectorSeminormTwo R s u ^ 2) + descendantsAverage Q j E