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

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

theorem HCPolySupport.MeanZeroNeumannCorrectorData.sq_negativeBesovSeminormTwo_flux_le_descendantMean_add_correctorError {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {u : Vec d → Vec d} (w : AHarmonicFunction a (cubeSet Q)) (s : ℝ) (hs : 0 < s) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu_mem : MemVectorL2 (cubeSet Q) u) (hg : MemVectorL2 (cubeSet Q) g) (hflux : CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x)) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x))) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSCorrectorEnergyLocalError Q a u (fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) s

Local weak-flux recurrence packaged with the explicit corrector-energy local-error envelope.

theorem HCPolySupport.MeanZeroNeumannCorrectorData.sq_negativeBesovSeminormTwo_flux_le_descendantMean_add_absorbedError {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {g : Vec d → Vec d} (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) {u : Vec d → Vec d} (w : AHarmonicFunction a (cubeSet Q)) (s : ℝ) {η : ℝ} (hs : 0 < s) (hη : 0 < η) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu_mem : MemVectorL2 (cubeSet Q) u) (hg_mem : MemVectorL2 (cubeSet Q) g) (hflux : CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) (coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x)) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (hwBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSAbsorbedLocalError Q a g u (fun (x : Vec d) => w.toH1.grad x) s η

Local absorbed weak-flux recurrence packaged with the explicit absorbed local-error envelope.

theorem HCPolySupport.exists_centeredCorrector_aHarmonicRemainder_fluxSeminormStepCorrectorEnergyError {d : ℕ} [NeZero d] {P R : TriadicCube d} (a : CoeffField d) {n : ℕ} {lam Lam s : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (hu_potential : IsPotentialOn (cubeSet P) u) (hu_residual : IsSolenoidalOn (cubeSet P) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hR : R ∈ descendantsAtDepth P n) (hEllR : IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_memR : MemVectorL2 (cubeSet R) u) (hg_memR : MemVectorL2 (cubeSet R) g) (hC : H1CoerciveEstimate (cubeSet R)) (hDataR : OpenCubeDescendantDeterministicCoarseData R a) (hsum : Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) : ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w : AHarmonicFunction a (cubeSet R)), (∀ x ∈ cubeSet R, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (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) + weakFluxRHSCorrectorEnergyLocalError R a u (fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) s

Descendant-cube coefficient-energy recurrence with the explicit corrector-energy local-error envelope.

theorem HCPolySupport.exists_correctorGradientSelector_fluxSeminormStepCorrectorEnergyError {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s lam Lam : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hEll : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_mem : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) u) (hg_mem : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) g) (hC : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R)) (hData : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → OpenCubeDescendantDeterministicCoarseData R a) (hsum : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) : ∃ (z : TriadicCube d → Vec d → Vec d), (∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g), z R = fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) ∧ ∀ (j : ℕ), ∀ 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) + weakFluxRHSCorrectorEnergyLocalError R a u (z R) s

Choose Neumann-corrector gradients on all descendants of a parent cube and package the local corrected-energy weak-flux recurrence in the global-selector shape consumed by the public corrected route.

theorem HCPolySupport.exists_centeredCorrector_aHarmonicRemainder_fluxSeminormStepAbsorbedError {d : ℕ} [NeZero d] {P R : TriadicCube d} (a : CoeffField d) {n : ℕ} {lam Lam s η : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (hη : 0 < η) (hu_potential : IsPotentialOn (cubeSet P) u) (hu_residual : IsSolenoidalOn (cubeSet P) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hR : R ∈ descendantsAtDepth P n) (hEllR : IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_memR : MemVectorL2 (cubeSet R) u) (hg_memR : MemVectorL2 (cubeSet R) g) (hC : H1CoerciveEstimate (cubeSet R)) (hDataR : OpenCubeDescendantDeterministicCoarseData R a) (hsum : Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g)) : ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w : AHarmonicFunction a (cubeSet R)), (∀ x ∈ cubeSet R, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => w.toH1.grad x) → (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) + weakFluxRHSAbsorbedLocalError R a g u (fun (x : Vec d) => w.toH1.grad x) s η)

Descendant-cube absorbed recurrence with the explicit absorbed local-error envelope.

theorem HCPolySupport.exists_harmonicRemainder_fluxSeminormStepAbsorbedError_of_coarseData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s η lam Lam : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (hη : 0 < η) (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hEll : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_mem : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) u) (hg_mem : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) g) (hC : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R)) (hData : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → OpenCubeDescendantDeterministicCoarseData R a) (hsum : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (hgBdd : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g)) : ∃ (v : TriadicCube d → Vec d → Vec d), (∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (v R))) → ∀ (j : ℕ), ∀ 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) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η

Choose harmonic remainders on all descendants of a parent cube and package the absorbed weak-flux local recurrence in the global-iteration shape.

The only remaining local assumption after the selector is chosen is boundedness of the selected harmonic remainder's finite negative Besov partials, exactly the boundedness input required by the local absorbed step.

theorem HCPolySupport.exists_harmonicRemainder_fluxSeminormStepAbsorbedError_and_decomposition {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s η lam Lam : ℝ} {u g : Vec d → Vec d} (hs : 0 < s) (hη : 0 < η) (hu_potential : IsPotentialOn (cubeSet Q) u) (hu_residual : IsSolenoidalOn (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (u x) - g x) (hEll : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_mem : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) u) (hg_mem : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) g) (hC : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R)) (hData : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → OpenCubeDescendantDeterministicCoarseData R a) (hsum : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → Summable fun (m : ℕ) => geometricWeight s 2 m * maxDescendantBBlockNormAtScale R (R.scale - ↑m) a) (hchildBdd : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → ∀ S ∈ descendantsAtDepth R 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo S s N fun (x : Vec d) => matVecMul (a x) (u x))) (huBdd : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N u)) (hgBdd : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g)) : ∃ (v : TriadicCube d → Vec d → Vec d), (∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → ∃ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w : AHarmonicFunction a (cubeSet R)), (v R = fun (x : Vec d) => w.toH1.grad x) ∧ ∀ x ∈ cubeSet R, u x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ ((∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (v R))) → ∀ (j : ℕ), ∀ 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) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η)

Choose harmonic remainders on all descendants and also expose that each selected value is the gradient of one of the local harmonic remainders produced by the centered Neumann-corrector construction.

theorem HCPolySupport.exists_centeredCorrector_harmonicRemainder_fluxSeminormStepCorrectorEnergyError {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x))) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + weakFluxRHSCorrectorEnergyLocalError Q a u.grad (fun (x : Vec d) => ω.toH1MeanZero.toH1Function.grad x) s

PDE-facing coefficient-energy recurrence with the explicit corrector-energy local-error envelope.

theorem HCPolySupport.exists_centeredCorrector_harmonicRemainder_fluxSeminormStepAbsorbedError {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (u : H1Function (cubeSet Q)) {s η lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hu : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) u g) (hg : MemVectorL2 (cubeSet Q) g) (hC : H1CoerciveEstimate (cubeSet Q)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) (hchildBdd : ∀ R ∈ descendantsAtDepth Q 1, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (u.grad x))) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u.grad)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g)) : ∃ (ω : MeanZeroNeumannCorrectorData Q a fun (x : Vec d) => g x - cubeAverageVec Q g) (w : AHarmonicFunction a (cubeSet Q)), (∀ x ∈ cubeSet Q, u.grad x = w.toH1.grad x + ω.toH1MeanZero.toH1Function.grad x) ∧ (BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x) → (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u.grad x)) ^ 2) + weakFluxRHSAbsorbedLocalError Q a g u.grad (fun (x : Vec d) => w.toH1.grad x) s η)

PDE-facing absorbed recurrence with the explicit absorbed local-error envelope.