Coarse-graining support:

Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletWeakFluxScalarAdequacy

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

Weak-flux scalar adequacy for the zero-Dirichlet RHS apex

This leaf continues the weak-flux displayed scalar calculation after the Poincare scalar adequacy discharge. It closes the weak-flux energy scale and composes it with the force-scale coefficient comparison, leaving only the separate tail allocations.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletWeakFluxDisplayedForceScale_le_compact_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s AweakForce : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hAweakForce : 2500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ AweakForce) : 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ AweakForce * (s.rpow (-(5 / 2)) ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹)

Corrected weak-flux force-scale adequacy with manuscript Lambda * lambda^{-1} units.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletWeakFluxDisplayedEnergyScale_le_compact_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hs_le : s ≤ 1) (hG_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s g) : 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * zeroTraceDirichletEnergyEnvelope Q a s g ≤ 32500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * (s.rpow (-(5 / 2)) ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)

Weak-flux energy component adequacy after expanding the zero-Dirichlet envelope.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletGradientTailBudget_mul_five_inv_le_raw_lambdaInv_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hG_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s g) : 5 * s⁻¹ * zeroTraceDirichletGradientTailBudget Q a s g ≤ 887500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * (s.rpow (-(5 / 2)) ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)

Zero-trace gradient-tail adequacy at the raw scale produced by the zero-Dirichlet energy envelope.

This is the complete tail algebra before the final coefficient conversion from lambda^{-2} to the manuscript Lambda * lambda^{-1} scale.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletWeakFluxDisplayedBVTailScale_le_compact_sq_of_averaged_budget_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (g : Vec d → Vec d) {Brho BomegaNeg BomegaForce Arho AomegaNeg AomegaForce : ℝ} (hs : 0 < s) (hBrho : Brho ≤ Arho * (s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)) (hBomegaNeg : BomegaNeg ≤ AomegaNeg * (s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)) (hBomegaForce : BomegaForce ≤ AomegaForce * (s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)) : 5 * s⁻¹ * (Brho + (BomegaNeg + BomegaForce)) ≤ 5 * (Arho + (AomegaNeg + AomegaForce)) * (s.rpow (-(5 / 2)) ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)

Weak-flux BV tail adequacy for the tight averaged-budget choice. This is the algebraic allocation used when the harmonic-remainder BV constant is chosen as the sum of the three averaged budget pieces.