Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHS

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

theorem HCPolySupport.Real.sqrt_le_of_le_sq {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAB : A ≤ B ^ 2) : √A ≤ B

Square-root comparison from a nonnegative square-side bound.

Coarse-flux response with right-hand side

This file starts the Lean surface for manuscript §3.2.4, l.coarse.grained.flux.response.RHS.deterministic.theory.

The key distinction from §3.2.3 is the field being controlled: §3.2.3 estimates a∇u, while §3.2.4 estimates the actual coarse flux defect (a-a₀)∇u. The first lemmas here package the homogeneous response contribution in the q = 2 negative seminorm used by the downstream §3.3 duality lemma.

noncomputable def HCPolySupport.coarseFluxResponseQOneBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (u : AHarmonicFunction a (cubeSet Q)) : ℝ

The q=1 homogeneous coarse-flux response bound from §3.1.3.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseFluxResponseRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) : ℝ

The one-cube §3.2.4 RHS flux-response bound, before the descendant-depth inflation used in §3.3.B.

This mirrors the manuscript display e.coarse.grained.flux.response.RHS.deterministic.theory on one cube.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseFluxResponseRHSEnergyBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU : Vec d → Vec d) : ℝ

The ∇u-energy part of the §3.2.4 RHS flux-response bound.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseFluxResponseRHSResponseCorrectionBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) : ℝ

The forcing contribution in the homogeneous-response part of the §3.2.4 split. It comes from replacing the harmonic energy of w = u - v by the energy of u plus the zero-Dirichlet RHS energy estimate for v.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseFluxResponseRHSWeakFluxCorrectionBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) : ℝ

The weak-flux estimate contribution for the correction field a∇v.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseFluxResponseRHSPoincareCorrectionBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) : ℝ

The RHS Poincare contribution for the constant-coefficient correction a₀∇v.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseFluxResponseRHSHomogeneousSplitBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) : ℝ

The homogeneous split component after the zero-Dirichlet energy correction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.coarseFluxResponseRHSSplitEnvelope {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) : ℝ

The explicit split-envelope produced by the Lean q=2 triangle wrappers before absorbing harmless dimensional constants into the manuscript's C(d).

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.coarseFluxResponseRHSBound_eq_component_sum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) : coarseFluxResponseRHSBound Q a a0 s gradU g = coarseFluxResponseRHSEnergyBound Q a a0 s gradU + coarseFluxResponseRHSResponseCorrectionBound Q a a0 s g + coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g + coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

theorem HCPolySupport.isEllipticFieldOn_self_of_descendant_isEllipticFieldOn {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) : IsEllipticFieldOn lam Lam (cubeSet Q) a

The descendant ellipticity hypothesis includes the parent cube itself at depth zero.

theorem HCPolySupport.cubeAverage_coefficientEnergyDensity_nonneg_of_isEllipticFieldOn {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (F : Vec d → Vec d) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) : 0 ≤ cubeAverage Q (coefficientEnergyDensity a F)

Coefficient-energy cube averages are nonnegative under ellipticity.

theorem HCPolySupport.cubeAverage_coefficientEnergyDensity_nonneg_of_descendant_isEllipticFieldOn {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (F : Vec d → Vec d) (hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) (n : ℕ) (R : TriadicCube d) : R ∈ descendantsAtDepth Q n → 0 ≤ cubeAverage R (coefficientEnergyDensity a F)

Descendant version of coefficient-energy average nonnegativity from a descendant ellipticity hypothesis.

theorem HCPolySupport.coarseFluxResponseRHSEnergyBound_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradU : Vec d → Vec d) (hs : 0 < s) : 0 ≤ coarseFluxResponseRHSEnergyBound Q a a0 s gradU

theorem HCPolySupport.coarseFluxResponseRHSResponseCorrectionBound_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : 0 ≤ coarseFluxResponseRHSResponseCorrectionBound Q a a0 s g

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxCorrectionBound_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : 0 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

theorem HCPolySupport.coarseFluxResponseRHSPoincareCorrectionBound_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

theorem HCPolySupport.coarseFluxResponseRHSBound_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradU g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : 0 ≤ coarseFluxResponseRHSBound Q a a0 s gradU g

theorem HCPolySupport.negativeVectorSeminorm_fluxDefect_le_coarseFluxResponseQOne {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) {lam Lam lam0 Lam0 : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (u : AHarmonicFunction a (cubeSet Q)) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 u.toH1.grad) ≤ coarseFluxResponseQOneBound Q a a0 s u

Homogeneous §3.2.4 component: the q=1 coarse-flux response theorem for an a-harmonic field supplies the q=2 flux-defect control required by the inhomogeneous split.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_bddAbove_of_partialSeminorm_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hpartialBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminorm Q s N u)) : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)

A bounded q=1 finite-depth family gives a bounded q=2 finite-depth family.

theorem HCPolySupport.fluxDefect_eq_add_sub_of_eq_add_on_cubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (gradU gradW gradV : Vec d → Vec d) (hgrad : ∀ x ∈ cubeSet Q, gradU x = gradW x + gradV x) (x : Vec d) : x ∈ cubeSet Q → fluxDefect a a0 gradU x = fluxDefect a a0 gradW x + matVecMul (a x) (gradV x) - matVecMul a0 (gradV x)

Pointwise algebra behind the §3.2.4 split (a - a₀)∇u = (a - a₀)∇w + a∇v - a₀∇v.

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_fluxDefect_le_split_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU gradW gradV : Vec d → Vec d) (hgrad : ∀ x ∈ cubeSet Q, gradU x = gradW x + gradV x) (hdefectW_mem : MemVectorL2 (cubeSet Q) (fluxDefect a a0 gradW)) (hfluxV_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectW_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 gradW))) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (gradV x))) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ √2 * (√2 * (cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradW) + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x))

Recompose the three §3.2.4 split components in the note-normalized negative q = 2 seminorm.

This is the Lean form of the triangle-inequality step in e.cg.flux.response.RHS.split.deterministic.theory.

theorem HCPolySupport.negativeBesovSeminormTwo_fluxDefect_le_coarseFluxRHSSplitEnvelope_of_component {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU gradW gradV g : Vec d → Vec d) (hgrad : ∀ x ∈ cubeSet Q, gradU x = gradW x + gradV x) (hdefectW_mem : MemVectorL2 (cubeSet Q) (fluxDefect a a0 gradW)) (hfluxV_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectW_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 gradW))) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradW) ≤ coarseFluxResponseRHSHomogeneousSplitBound Q a a0 s gradU g) (hfluxV : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) (ha0V : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSSplitEnvelope Q a a0 s gradU g

Component-facing §3.2.4 split theorem. The hypotheses are exactly the three estimates produced by the manuscript proof after splitting u = w + v:

• homogeneous response for (a-a₀)∇w, including the RHS energy correction;
• weak-flux RHS control of a∇v;
• RHS Poincare control of a₀∇v.

theorem HCPolySupport.negativeBesovSeminormTwo_fluxDefect_le_coarseFluxRHSSplitEnvelope {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) {lam Lam lam0 Lam0 : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (ha0symm : Matrix.IsSymm a0) (gradU gradV g : Vec d → Vec d) (w : AHarmonicFunction a (cubeSet Q)) (hgrad : ∀ x ∈ cubeSet Q, gradU x = w.toH1.grad x + gradV x) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity a a0) (hhomogeneousEnergy : coarseFluxResponseQOneBound Q a a0 s w ≤ coarseFluxResponseRHSHomogeneousSplitBound Q a a0 s gradU g) (hfluxV_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradV x)) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hfluxV : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) (ha0V : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSSplitEnvelope Q a a0 s gradU g

The same split-envelope theorem with the homogeneous component discharged by the already-formalized q=1 coarse-flux response for an a-harmonic remainder.

The remaining hypotheses are the two correction estimates (a∇v and a₀∇v) and the scalar comparison which replaces the harmonic-response energy of w by the §3.2.4 homogeneous split bound.

theorem HCPolySupport.negativeBesovSeminormTwo_fluxDefect_le_fluxRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU gradW gradV g : Vec d → Vec d) {BdefectW BfluxV Ba0V : ℝ} (hgrad : ∀ x ∈ cubeSet Q, gradU x = gradW x + gradV x) (hdefectW_mem : MemVectorL2 (cubeSet Q) (fluxDefect a a0 gradW)) (hfluxV_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectW_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 gradW))) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradW) ≤ BdefectW) (hfluxV : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ BfluxV) (ha0V : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ Ba0V) (hcomponents : √2 * (√2 * (BdefectW + BfluxV) + Ba0V) ≤ coarseFluxResponseRHSBound Q a a0 s gradU g) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound Q a a0 s gradU g

Note-facing recomposition wrapper for §3.2.4: once the harmonic defect, corrector flux, and constant-coefficient corrector-gradient components have been bounded by the manuscript RHS, the split theorem yields the desired coarse-flux-response bound for (a - a₀)∇u.

noncomputable def HCPolySupport.localizedCoarseFluxResponseRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) : ℝ

Descendant L² average of the one-cube §3.2.4 RHS flux-response bound. This is the scalar localization target that §3.3 has to compare with coarseGrainingL2FluxDefectBound.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) : localizedCoarseFluxResponseRHSBound Q a a0 s 0 gradU g = |coarseFluxResponseRHSBound Q a a0 s gradU g|

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_zero_of_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) (hbound_nonneg : 0 ≤ coarseFluxResponseRHSBound Q a a0 s gradU g) : localizedCoarseFluxResponseRHSBound Q a a0 s 0 gradU g = coarseFluxResponseRHSBound Q a a0 s gradU g

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_zero_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradU g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : localizedCoarseFluxResponseRHSBound Q a a0 s 0 gradU g = coarseFluxResponseRHSBound Q a a0 s gradU g

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_le_of_descendant_bound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (j : ℕ) (gradU g : Vec d → Vec d) {B : ℝ} (hB_nonneg : 0 ≤ B) (hbound_nonneg : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ coarseFluxResponseRHSBound R a a0 s gradU g) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSBound R a a0 s gradU g ≤ B) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ B

If each descendant one-cube RHS bound is nonnegative and pointwise bounded by a single scalar B, then its descendant L² average is bounded by B.

theorem HCPolySupport.localizedCoarseFluxResponseRHSBound_le_of_descendant_bound_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (j : ℕ) (gradU g : Vec d → Vec d) {B : ℝ} (hs : 0 < s) (hB_nonneg : 0 ≤ B) (hgBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hpoint : ∀ R ∈ descendantsAtDepth Q j, coarseFluxResponseRHSBound R a a0 s gradU g ≤ B) : localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g ≤ B

Bounded-positive-Besov version of localizedCoarseFluxResponseRHSBound_le_of_descendant_bound.

theorem HCPolySupport.negativeBesovFluxAverage_le_sqrt_descendantMean_fluxRHSBound_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) (j : ℕ) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hbound : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => coarseFluxResponseRHSBound R a a0 s gradU g ^ 2)

Descendant-localized §3.2.4 RHS handoff from pointwise one-cube coarse-flux-response bounds.

This is the averaging wrapper needed by the downstream §3.3.B duality surface: if every depth-j descendant has the one-cube RHS bound, then the localized q = 2 average is bounded by the descendant ℓ² average of those RHS values.

theorem HCPolySupport.negativeBesovFluxAverage_le_coarseFluxRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) (j : ℕ) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hbound : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g

Named localized §3.2.4 RHS handoff from pointwise one-cube bounds.

theorem HCPolySupport.negativeBesovFluxAverage_le_sqrt_descendantMean_fluxRHSBound_sq_of_component {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU gradW gradV g : Vec d → Vec d) (j : ℕ) {BdefectW BfluxV Ba0V : TriadicCube d → ℝ} (hgrad : ∀ R ∈ descendantsAtDepth Q j, ∀ x ∈ cubeSet R, gradU x = gradW x + gradV x) (hdefectW_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) (fluxDefect a a0 gradW)) (hfluxV_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectU_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hdefectW_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradW))) (hfluxV_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradW) ≤ BdefectW R) (hfluxV : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ BfluxV R) (ha0V : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ Ba0V R) (hcomponents : ∀ R ∈ descendantsAtDepth Q j, √2 * (√2 * (BdefectW R + BfluxV R) + Ba0V R) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => coarseFluxResponseRHSBound R a a0 s gradU g ^ 2)

Descendant-localized §3.2.4 RHS handoff with the split components exposed on each descendant cube.

theorem HCPolySupport.negativeBesovFluxAverage_le_coarseFluxRHSBound_of_descendant_split_component {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU gradW gradV g : Vec d → Vec d) (j : ℕ) {BdefectW BfluxV Ba0V : TriadicCube d → ℝ} (hgrad : ∀ R ∈ descendantsAtDepth Q j, ∀ x ∈ cubeSet R, gradU x = gradW x + gradV x) (hdefectW_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) (fluxDefect a a0 gradW)) (hfluxV_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectU_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hdefectW_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradW))) (hfluxV_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradW) ≤ BdefectW R) (hfluxV : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ BfluxV R) (ha0V : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ Ba0V R) (hcomponents : ∀ R ∈ descendantsAtDepth Q j, √2 * (√2 * (BdefectW R + BfluxV R) + Ba0V R) ≤ coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g

Named localized §3.2.4 RHS handoff with the split components exposed on each descendant cube.