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

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

Constant-envelope scalar absorption for the RHS coarse-flux response

The scalar absorption hooks in RHSScalarAbsorption target the bare correction components. The manuscript §3.2.4 theorem carries a dimensional constant, so this leaf exposes the same hooks with a caller-supplied nonnegative multiplier.

theorem HCPolySupport.coarseFluxRHSWeakFluxRadicand_zero_le_const_mul_correctionBound_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (C s : ℝ) (g gradV : Vec d → Vec d) {BU BV Benergy BUtail BVtail Bforce : ℝ} (henergy : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a gradV) ≤ Benergy) (hBU : 5 * s⁻¹ * BU ≤ BUtail) (hBV : 5 * s⁻¹ * BV ≤ BVtail) (hforce : 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ Bforce) (hsum : Benergy + BUtail + BVtail + Bforce ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) : coarseFluxResponseRHSWeakFluxExpandedRadicand Q a s g gradV 0 BU BV ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2

Weak-flux radicand component budgets closing into C * correctionBound.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedBound_le_const_mul_correctionBound_of_radicand_le_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {C s : ℝ} (g gradV : Vec d → Vec d) (m : ℕ) {BU BV : ℝ} (hC_nonneg : 0 ≤ C) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hrad : coarseFluxResponseRHSWeakFluxExpandedRadicand Q a s g gradV m BU BV ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV m BU BV ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Weak-flux square-root absorption into C * correctionBound.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedBound_le_const_mul_correctionBound_of_component_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {C s : ℝ} (g gradV : Vec d → Vec d) {BU BV Benergy BUtail BVtail Bforce : ℝ} (hC_nonneg : 0 ≤ C) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (henergy : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a gradV) ≤ Benergy) (hBU : 5 * s⁻¹ * BU ≤ BUtail) (hBV : 5 * s⁻¹ * BV ≤ BVtail) (hforce : 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ Bforce) (hsum : Benergy + BUtail + BVtail + Bforce ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV 0 BU BV ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Weak-flux square-root absorption into C * correctionBound from budgets.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedBound_le_const_mul_correctionBound_of_exact_budget {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {C s : ℝ} (g gradV : Vec d → Vec d) {BU BV : ℝ} (hC_nonneg : 0 ≤ C) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hbudget : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a gradV) + 5 * s⁻¹ * BU + 5 * s⁻¹ * BV + 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV 0 BU BV ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Weak-flux square-root absorption with the scalar side stated as the exact expanded depth-zero budget.

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_matVecMul_le_of_localized_depth_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (gradV g : Vec d → Vec d) {BU BV B : ℝ} (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (hlocalized : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (gradV x)) 0 ≤ coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV 0 BU BV) (hscalar : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV 0 BU BV ≤ B) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ B

Depth-zero weak-flux local handoff to an arbitrary scalar envelope.

theorem HCPolySupport.negativeBesovSeminormTwo_matVecMul_grad_le_const_mul_of_weakFluxCorrectionBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) (C : ℝ) {lam Lam : ℝ} (hCmul_nonneg : 0 ≤ C) (hs : 0 < s) (hs_le : s ≤ 1) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) v.grad) (hg_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) g) (hC_desc : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R)) (hData_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → OpenCubeDescendantDeterministicCoarseData R a) (hsum_desc : ∀ (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) (v.grad x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N v.grad)) (hgBdd_centered_desc : ∀ (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)) {BU BV Benergy BUtail BVtail Bforce : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s v.grad n)) (hEll_open : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1) (havg_parent_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a v.grad)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a v.grad)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a v.grad) (cubeSet Q) MeasureTheory.volume) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hu_tail : ∀ (k : ℕ), coarsePoincareRHSSn Q s v.grad k ≤ BU) (hvConstructed : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, ∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w : AHarmonicFunction a (cubeSet R)), (∀ x ∈ cubeSet R, v.grad 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) => w.toH1.grad x) ^ 2 ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BV) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (v.grad x))) (henergy : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a v.grad) ≤ Benergy) (hBU : 5 * s⁻¹ * BU ≤ BUtail) (hBV : 5 * s⁻¹ * BV ≤ BVtail) (hforce : 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ Bforce) (hbudget : Benergy + BUtail + BVtail + Bforce ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (v.grad x)) ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

H¹ weak-solution weak-flux correction with the scalar side supplied as component budgets closing into a caller-supplied multiple of the compact bound.

theorem HCPolySupport.negativeBesovSeminormTwo_matVecMul_grad_le_const_mul_of_exact_budget {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) (C : ℝ) {lam Lam : ℝ} (hCmul_nonneg : 0 ≤ C) (hs : 0 < s) (hs_le : s ≤ 1) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) v.grad) (hg_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) g) (hC_desc : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R)) (hData_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → OpenCubeDescendantDeterministicCoarseData R a) (hsum_desc : ∀ (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) (v.grad x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N v.grad)) (hgBdd_centered_desc : ∀ (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)) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s v.grad n)) (hEll_open : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1) (havg_parent_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a v.grad)) (havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a v.grad)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a v.grad) (cubeSet Q) MeasureTheory.volume) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hu_tail : ∀ (k : ℕ), coarsePoincareRHSSn Q s v.grad k ≤ BU) (hvConstructed : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, ∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w : AHarmonicFunction a (cubeSet R)), (∀ x ∈ cubeSet R, v.grad 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) => w.toH1.grad x) ^ 2 ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BV) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (v.grad x))) (hbudget : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a v.grad) + 5 * s⁻¹ * BU + 5 * s⁻¹ * BV + 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (v.grad x)) ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

H¹ weak-solution weak-flux correction with the scalar side stated as the exact expanded depth-zero budget.

theorem HCPolySupport.negativeBesovSeminormTwo_matVecMul_grad_le_weakFluxCorrection_of_exactBudget {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) (C : ℝ) {lam Lam : ℝ} (hCmul_nonneg : 0 ≤ C) (hs : 0 < s) (hs_le : s ≤ 1) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (hEll_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → IsEllipticFieldOn lam Lam (cubeSet R) a) (hu_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) v.grad) (hg_mem_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → MemVectorL2 (cubeSet R) g) (hC_desc : (R : TriadicCube d) → (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → H1CoerciveEstimate (cubeSet R)) (hData_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → OpenCubeDescendantDeterministicCoarseData R a) (hsum_desc : ∀ (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) (v.grad x))) (huBdd_desc : ∀ (R : TriadicCube d), (∃ (n : ℕ), R ∈ descendantsAtDepth Q n) → BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N v.grad)) (hgBdd_centered_desc : ∀ (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)) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s v.grad n)) (hEll_open : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a v.grad) (cubeSet Q) MeasureTheory.volume) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hu_tail : ∀ (k : ℕ), coarsePoincareRHSSn Q s v.grad k ≤ BU) (hvConstructed : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, ∀ (ω : MeanZeroNeumannCorrectorData R a fun (x : Vec d) => g x - cubeAverageVec R g) (w : AHarmonicFunction a (cubeSet R)), (∀ x ∈ cubeSet R, v.grad 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) => w.toH1.grad x) ^ 2 ≤ (coarsePoincareRHSDepthWeight s j)⁻¹ * BV) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (v.grad x))) (hbudget : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a v.grad) + 5 * s⁻¹ * BU + 5 * s⁻¹ * BV + 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2 ≤ (C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (v.grad x)) ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Exact-budget weak-flux correction with coefficient-energy average nonnegativity derived from descendant ellipticity.

theorem HCPolySupport.matNorm_sq_mul_fluxPoincareRadicand_le_const_mul_correctionBound_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (g gradV : Vec d → Vec d) {Benergy Bforce : ℝ} (henergy : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a gradV)) ≤ Benergy) (hforce : matNorm a0 ^ 2 * (15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ Bforce) (hsum : Benergy + Bforce ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) : matNorm a0 ^ 2 * coarseFluxResponseRHSPoincareExpandedRadicand Q a s g gradV ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2

Poincare radicand budgets closing into C * correctionBound.

theorem HCPolySupport.matrixNorm_mul_fluxPoincareBound_le_constant_mul_correctionBound_of_radicand {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (g gradV : Vec d → Vec d) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hrad : matNorm a0 ^ 2 * coarseFluxResponseRHSPoincareExpandedRadicand Q a s g gradV ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) : matNorm a0 * coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV ≤ C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare square-root absorption into C * correctionBound.

theorem HCPolySupport.matNorm_mul_fluxPoincareBound_le_const_mul_correctionBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (g gradV : Vec d → Vec d) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) {Benergy Bforce : ℝ} (henergy : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a gradV)) ≤ Benergy) (hforce : matNorm a0 ^ 2 * (15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ Bforce) (hsum : Benergy + Bforce ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) : matNorm a0 * coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV ≤ C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare square-root absorption into C * correctionBound from budgets.

theorem HCPolySupport.matNorm_mul_coarseFluxPoincareBound_le_const_correction_budget {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (g gradV : Vec d → Vec d) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hbudget : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a gradV)) + matNorm a0 ^ 2 * (15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) : matNorm a0 * coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV ≤ C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare square-root absorption with the scalar side stated as the exact matrix-weighted expanded budget.

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_constMatMul_le_of_grad_bound {d : ℕ} (Q : TriadicCube d) (a0 : Mat d) (s : ℝ) (gradV : Vec d → Vec d) {Bgrad B : ℝ} (hmat : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ matNorm a0 * cubeBesovNegativeVectorSeminormTwo Q s gradV) (hgrad : cubeBesovNegativeVectorSeminormTwo Q s gradV ≤ Bgrad) (hscalar : matNorm a0 * Bgrad ≤ B) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ B

Constant-matrix gradient handoff to an arbitrary scalar envelope.

theorem HCPolySupport.negativeBesovSeminormTwo_constMatMul_le_const_mul_fluxPoincareCorrectionBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) (C : ℝ) {lam Lam : ℝ} (hCmul_nonneg : 0 ≤ C) (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hgrad_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) v.grad) (hgrad_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N v.grad)) {Benergy Bforce : ℝ} (henergy : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a v.grad)) ≤ Benergy) (hforce : matNorm a0 ^ 2 * (15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ Bforce) (hbudget : Benergy + Bforce ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (v.grad x)) ≤ C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

H¹ weak-solution Poincare correction with the scalar side supplied as matrix-weighted budgets closing into a caller-supplied multiple.

theorem HCPolySupport.negativeBesovSeminormTwo_constMatMul_le_const_mul_of_fluxPoincareCorrectionBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) (C : ℝ) {lam Lam : ℝ} (hCmul_nonneg : 0 ≤ C) (hs : 0 < s) (hs_le : s ≤ 1) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hweak : IsH1DirichletRhsWeakSolutionOn a (cubeSet Q) v g) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hgrad_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) v.grad) (hgrad_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N v.grad)) (hbudget : matNorm a0 ^ 2 * (250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q (coefficientEnergyDensity a v.grad)) + matNorm a0 ^ 2 * (15000 * s⁻¹ ^ 4 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (v.grad x)) ≤ C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

H¹ weak-solution Poincare correction with the scalar side stated as the exact matrix-weighted expanded budget.