Coarse-graining support:

Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletScalarAdequacy

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

Scalar adequacy for the zero-Dirichlet RHS flux-response apex

This leaf records the Poincare displayed scalar comparison in the form used by the manuscript constant absorption. The weak-flux displayed comparison now lives in RHSConstantApexZeroDirichletWeakFluxScalarAdequacy, where the manuscript Lambda * lambda^{-1} force units are used directly.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedScalarAdequacyBase_pos {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (g : Vec d → Vec d) (hs : 0 < s) (hmat_pos : 0 < matNorm a0) (hlambda_pos : 0 < lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a) (hG_pos : 0 < cubeBesovPositiveVectorSeminormTwo Q s g) : 0 < s.rpow (-3) ^ 2 * matNorm a0 ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

Positivity of the compact Poincare correction-square base in the nondegenerate case.

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

Sharp zero-Dirichlet energy envelope control after expanding the square-root force term.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedEnergyScale_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) : 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * zeroTraceDirichletEnergyEnvelope Q a s g ≤ 162500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * (s.rpow (-3) ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)

Poincare energy component adequacy after expanding the zero-Dirichlet envelope.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedForceScale_le_compact_sq {d : ℕ} {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : 15000 * s⁻¹ ^ 4 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ 15000 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * s.rpow (-3) ^ 2

Poincare force component adequacy: the s^{-4} term is absorbed by the compact s^{-6} scale.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedScalarBudget_le_const_mul_correctionBound_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (g : Vec d → Vec d) {APoincareEnergy APoincareForce : ℝ} (hPoincareEnergy : 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * zeroTraceDirichletEnergyEnvelope Q a s g ≤ APoincareEnergy * (s.rpow (-3) ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)) (hPoincareForceScale : 15000 * s⁻¹ ^ 4 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ APoincareForce * s.rpow (-3) ^ 2) (halloc : APoincareEnergy + APoincareForce ≤ C ^ 2) : zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2

Poincare scalar adequacy from the energy-envelope and force-scale estimates.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose_of_energyEnvelope_and_force_scale_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (g : Vec d → Vec d) {APoincareEnergy APoincareForce : ℝ} (hPoincareEnergy : 250 * s⁻¹ ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ * zeroTraceDirichletEnergyEnvelope Q a s g ≤ APoincareEnergy * (s.rpow (-3) ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2)) (hPoincareForceScale : 15000 * s⁻¹ ^ 4 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ APoincareForce * s.rpow (-3) ^ 2) (halloc : APoincareEnergy + APoincareForce ≤ C ^ 2) : zeroTraceDirichletPoincareDisplayedComponentBoundsClose Q a a0 C s g

Poincare component target from the energy-envelope and force-scale estimates.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedScalarBudget_le_const_mul_correctionBound_sq_of_const_ge {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C : ℝ) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hs_le : s ≤ 1) (hG_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s g) (hC_sq : 177500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ C ^ 2) : zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2

Poincare scalar adequacy with the analytic estimates discharged into one constant bound.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose_of_const_ge {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C : ℝ) {s : ℝ} (g : Vec d → Vec d) (hs : 0 < s) (hs_le : s ≤ 1) (hG_nonneg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s g) (hC_sq : 177500 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 ≤ C ^ 2) : zeroTraceDirichletPoincareDisplayedComponentBoundsClose Q a a0 C s g

Poincare component target with scalar adequacy discharged into one constant bound.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedScalarBudget_le_const_mul_correctionBound_sq_of_div_le_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (g : Vec d → Vec d) (hbase_pos : 0 < s.rpow (-3) ^ 2 * matNorm a0 ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) (hC_sq : zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g / (s.rpow (-3) ^ 2 * matNorm a0 ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ C ^ 2) : zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g ≤ (C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ^ 2

Poincare displayed scalar adequacy in normalized C^2 form.

theorem HCPolySupport.ZeroTraceDirichletCorrectorData.zeroTraceDirichletPoincareDisplayedComponentBoundsClose_of_div_le_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (g : Vec d → Vec d) (hbase_pos : 0 < s.rpow (-3) ^ 2 * matNorm a0 ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) (hC_sq : zeroTraceDirichletPoincareDisplayedScalarBudget Q a a0 s g / (s.rpow (-3) ^ 2 * matNorm a0 ^ 2 * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹ ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2) ≤ C ^ 2) : zeroTraceDirichletPoincareDisplayedComponentBoundsClose Q a a0 C s g

The Poincare displayed component target follows from the normalized scalar adequacy inequality.