Coarse-graining support: #
Support.Deterministic.CoarseFluxResponse.RHSConstantApexZeroDirichletHomogeneous
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Homogeneous response discharge for the zero-Dirichlet RHS apex #
This leaf proves the scalar comparison that replaces the harmonic-response
energy of the remainder w by the manuscript's homogeneous split bound. The
proof uses the zero-trace energy envelope for the correction field and keeps the
constant requirements explicit so the apex file can close them from its fixed
dimension scale.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coarseFluxResponseQOneBound_le_const_mul_RHSHomogeneousSplitBound_of_zeroTraceDirichlet
{d : ℕ}
[NeZero d]
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(a0 : Mat d)
(s : ℝ)
(gradU : Vec d → Vec d)
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam C : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hgrad : ∀ x ∈ cubeSet Q, gradU x = w.toH1.grad x + ρ.toH10.grad x)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(hC_energy : 20 ≤ C)
(hC_response : 520 * (↑d * (3 ^ (↑d + s) * √2)) ≤ C)
:
coarseFluxResponseQOneBound Q a a0 s w ≤ C * coarseFluxResponseRHSHomogeneousSplitBound Q a a0 s gradU g
Discharge of the homogeneous scalar comparison in the zero-Dirichlet RHS
route. The two size assumptions on C are pure scalar constant checks; the
apex supplies them from 1000 times the displayed dimensional scale.