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

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

Scalar absorption for the RHS coarse-flux response

This leaf module keeps the scalar bookkeeping for manuscript §3.2.4 out of the main split/recomposition files. The estimates here turn the expanded §3.2.3/Poincare square-root RHSs into compact correction components once the corresponding square-side adequacy inequalities are supplied, and absorb the sqrt 2 triangle constants into a dimension-constant envelope.

noncomputable def HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedRadicand {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g gradV : Vec d → Vec d) (m : ℕ) (BU BV : ℝ) : ℝ

The square radicand in the expanded weak-flux correction bound.

Equations

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

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedBound_eq_sqrt_radicand {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g gradV : Vec d → Vec d) (m : ℕ) (BU BV : ℝ) : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV m BU BV = √(coarseFluxResponseRHSWeakFluxExpandedRadicand Q a s g gradV m BU BV)

The expanded weak-flux correction bound is the square root of its radicand.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedRadicand_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g gradV : Vec d → Vec d) (m : ℕ) {BU BV : ℝ} (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) : 0 ≤ coarseFluxResponseRHSWeakFluxExpandedRadicand Q a s g gradV m BU BV

Nonnegativity of the expanded weak-flux correction radicand.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedBound_le_correctionBound_of_radicand_le_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g gradV : Vec d → Vec d) (m : ℕ) {BU BV : ℝ} (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 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2) : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV m BU BV ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Square-side scalar absorption for the weak-flux correction component.

The remaining analytic input is the radicand inequality, which is where the zero-Dirichlet energy estimate for the correction field is inserted.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedRadicand_zero_le_correctionBound_sq_of_component_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (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 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2) : coarseFluxResponseRHSWeakFluxExpandedRadicand Q a s g gradV 0 BU BV ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2

Depth-zero weak-flux radicand absorption from four component budgets.

This is the scalar bookkeeping form of the remaining manuscript estimate: the energy, two tail terms, and forcing term may be proved separately and then summed into the compact correction square.

theorem HCPolySupport.coarseFluxResponseRHSWeakFluxExpandedBound_le_correctionBound_of_component_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g gradV : Vec d → Vec d) {BU BV Benergy BUtail BVtail Bforce : ℝ} (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 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2) : coarseFluxResponseRHSWeakFluxExpandedBound Q a s g gradV 0 BU BV ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Weak-flux square-root absorption from component budgets and the standard nonnegativity/boundedness hypotheses.

theorem HCPolySupport.negativeBesovSeminormTwo_matrixFlux_le_weakFluxCorrection_of_componentBudgets {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (gradV g : Vec d → Vec d) {BU BV Benergy BUtail BVtail Bforce : ℝ} (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)) (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) (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 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

Depth-zero weak-flux component bridge with the scalar side supplied as component budgets rather than one opaque expanded-RHS comparison.

theorem HCPolySupport.negativeBesovSeminormTwo_matrixVectorMultiply_grad_le_of_expanded_radicand {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) {lam Lam : ℝ} (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))) (hrad : coarseFluxResponseRHSWeakFluxExpandedRadicand Q a s g v.grad 0 BU BV ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (v.grad x)) ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

H¹ weak-solution weak-flux correction with the scalar side expressed as the square-radicand inequality which remains after inserting the correction-field energy estimate.

theorem HCPolySupport.negativeBesovSeminormTwo_matrixVectorMultiply_grad_le_of_component {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) {lam Lam : ℝ} (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 ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (v.grad x)) ≤ coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g

H¹ weak-solution weak-flux correction with the scalar side supplied as the four component budgets of the expanded depth-zero radicand.

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

The square radicand in the expanded RHS Poincare correction bound.

Equations

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

theorem HCPolySupport.coarseFluxResponseRHSPoincareExpandedBound_eq_sqrt_radicand {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (g gradV : Vec d → Vec d) : coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV = √(coarseFluxResponseRHSPoincareExpandedRadicand Q a s g gradV)

The expanded RHS Poincare correction bound is the square root of its radicand.

theorem HCPolySupport.coarseFluxResponseRHSPoincareExpandedRadicand_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g gradV : Vec d → Vec d) (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) : 0 ≤ coarseFluxResponseRHSPoincareExpandedRadicand Q a s g gradV

Nonnegativity of the expanded RHS Poincare correction radicand.

theorem HCPolySupport.matNorm_mul_coarseFluxResponseRHSPoincareExpandedBound_le_correctionBound_of_radicand_le_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (g gradV : Vec d → Vec d) (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 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2) : matNorm a0 * coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Square-side scalar absorption for the constant-coefficient Poincare correction.

This is shaped to discharge the matNorm a0 * expanded ≤ compact hypothesis in RHSCorrections after proving the manuscript energy-to-force square bound.

theorem HCPolySupport.matNorm_sq_mul_fluxPoincareRadicand_le_correctionBound_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (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 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2) : matNorm a0 ^ 2 * coarseFluxResponseRHSPoincareExpandedRadicand Q a s g gradV ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2

Poincare radicand absorption from separate energy and forcing budgets after multiplying by the constant-coefficient matrix norm.

theorem HCPolySupport.matNorm_mul_coarseFluxResponseRHSPoincareExpandedBound_le_correctionBound_of_component_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (g gradV : Vec d → Vec d) (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 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2) : matNorm a0 * coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare square-root absorption from component budgets and the standard nonnegativity/boundedness hypotheses.

theorem HCPolySupport.negativeBesovSeminormTwo_constMatMul_le_fluxPoincareCorrectionBound_of_component {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradV g : Vec d → Vec d) {Benergy Bforce : ℝ} (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hmat : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ matNorm a0 * cubeBesovNegativeVectorSeminormTwo Q s gradV) (hgrad : cubeBesovNegativeVectorSeminormTwo Q s gradV ≤ coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV) (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 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare component bridge with the compact scalar correction supplied by energy/forcing budgets.

theorem HCPolySupport.negativeBesovSeminormTwo_matrixAction_le_poincareCorrection_of_componentBudgets {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradV g : Vec d → Vec d) {Benergy Bforce : ℝ} (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a gradV)) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hgrad_mem_desc : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) gradV) (hgrad_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N gradV)) (hgrad : cubeBesovNegativeVectorSeminormTwo Q s gradV ≤ coarseFluxResponseRHSPoincareExpandedBound Q a s g gradV) (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 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

Poincare component bridge with constant-matrix action discharged from descendant L² data, and scalar correction supplied by component budgets.

theorem HCPolySupport.negativeBesovMatrixGradient_le_poincareCorrection_of_weakSolution {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) {lam Lam : ℝ} (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)) (hrad : matNorm a0 ^ 2 * coarseFluxResponseRHSPoincareExpandedRadicand Q a s g v.grad ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (v.grad x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

H¹ weak-solution Poincare correction with the scalar side expressed as the square-radicand inequality remaining after the correction-field energy bound.

theorem HCPolySupport.negativeBesovSeminormTwo_constMatMul_grad_le_of_h1DirichletRhsWeakSolutionOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (v : H1Function (cubeSet Q)) {lam Lam : ℝ} (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 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g ^ 2) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (v.grad x)) ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g

H¹ weak-solution Poincare correction with the scalar side supplied as matrix-weighted energy and forcing budgets.

theorem HCPolySupport.coarseFluxResponseRHSSplitEnvelope_le_two_mul_coarseFluxResponseRHSBound_of_poincare_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU g : Vec d → Vec d) (hpoincare_nonneg : 0 ≤ coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) : coarseFluxResponseRHSSplitEnvelope Q a a0 s gradU g ≤ 2 * coarseFluxResponseRHSBound Q a a0 s gradU g

The split-envelope constants are absorbed into a single factor 2. This is the local C(d) bookkeeping for the sqrt 2 triangle inequalities.

theorem HCPolySupport.coarseFluxResponseRHSSplitEnvelope_le_two_mul_coarseFluxResponseRHSBound_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)) : coarseFluxResponseRHSSplitEnvelope Q a a0 s gradU g ≤ 2 * coarseFluxResponseRHSBound Q a a0 s gradU g

Bounded-positive-Besov version of the split-envelope constant absorption.

theorem HCPolySupport.negativeBesovSeminormTwo_fluxDefect_le_two_mul_fluxRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {s : ℝ} (gradU gradW gradV g : Vec d → Vec d) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (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) ≤ 2 * coarseFluxResponseRHSBound Q a a0 s gradU g

Split-component RHS flux-response estimate with the triangle constants absorbed into the factor 2.