Coarse-graining support: Support.Deterministic.WeakFluxRHS.AveragedStepping

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

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

Averaged-scale form of the weak-flux local recurrence. This is the Section 3.2.3 Step 4 bookkeeping bridge specialized to the flux field a u.