Coarse-graining support: Support.Book.Ch03.Theorems.CoarseFluxResponseRHS

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

Section 3.2.4: Coarse-grained flux-response estimate with right-hand side

This file assembles the public theorem package for l.coarse.grained.flux.response.RHS.deterministic.theory. The left-hand side uses the genuine dual negative Besov norm, not the concrete negative seminorm from Section 3.1.

Audit tag

Claim: expose the single public coarse flux-response-with-RHS package using the genuine dual negative Besov norm.

Downstream target: InhomogeneousEquationsTheory and the Ch3.3 coarse-graining handoff. This file should not introduce additional RHS package variants.

structure HCPolySupport.Book.Ch03.CoarseFluxResponseRHSTheory (d : ℕ) [NeZero d] : Prop

Public theorem package for the coarse-grained flux-response estimate with right-hand side.

• exists_constant : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (a0 : ConstantCoeffMatrix d) (u : ForcedCubeSolution Q a g), 0 < s → s < 1 → ForceBesovRegularity Q s g → scaleNormalizedDualNegativeBesovVectorNormTwo Q s (forcedSolutionFluxDefectField Q a a0 u) ≤ coarseFluxResponseWithRHSRHS C Q a a0 s g u

theorem HCPolySupport.Book.Ch03.coarseFluxResponseRHS_negativeDual_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} {g : Vec d → Vec d} (a0 : ConstantCoeffMatrix d) (u : ForcedCubeSolution Q a g) (hs : 0 < s) (hs_lt : s < 1) (hg : ForceBesovRegularity Q s g) : scaleNormalizedDualNegativeBesovVectorNormTwo Q s (forcedSolutionFluxDefectField Q a a0 u) ≤ coarseFluxResponseWithRHSRHS (↑d ^ 2 * max 1 (↑d * Real.rpow 3 (↑d + 1) * (2 * ZeroTraceDirichletCorrectorData.zeroTraceFluxApexConstant d 1))) Q a a0 s g u

Fully proved coarse-grained flux-response estimate with right-hand side.

theorem HCPolySupport.Book.Ch03.coarseFluxResponseRHSTheory {d : ℕ} [NeZero d] : CoarseFluxResponseRHSTheory d

Fully proved public coarse-grained flux-response theorem package with RHS.