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

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

Section 3.2.1: Coarse-grained Poincare inequality with right-hand side

This file assembles the public theorem package for p.coarse.grained.Poincare.RHS.deterministic.theory and the auxiliary zero-Dirichlet energy estimate l.zero.Dirichlet.energy.RHS.deterministic.theory.

Audit tag

Claim: assemble the public coarse Poincare-with-RHS package and the zero-Dirichlet energy RHS estimate from the deterministic RHS endpoints.

Downstream target: InhomogeneousEquationsTheory. This file should remain the single public CoarsePoincareRHSTheory endpoint for Section 3.2.1.

theorem HCPolySupport.Book.Ch03.zeroTraceDirichletEnergyEnvelope_sqrt_le_publicRHS {d : ℕ} [NeZero d] {C : ℝ} (hC_nonneg : 0 ≤ C) (hC_zero : √(250 + 2 * √15000 * √2) * (↑d * Real.rpow 3 (↑d + 1)) ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (ht : 0 < t) (ht_lt : t < 1 / 2) (hg : ForceBesovRegularity Q (2 * t) g) : √(zeroTraceDirichletEnergyEnvelope Q (publicCoeffField Q a) (2 * t) g) ≤ zeroDirichletEnergyWithRHSRHS (↑d * C) Q a t g

The deterministic zero-trace RHS energy envelope is bounded by the note-facing public zero-Dirichlet RHS. This algebraic bridge is reused by the Dirichlet energy consequence, where the zero-boundary auxiliary solution is constructed internally rather than supplied as a public ZeroTraceForcedCubeSolution.

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

Public theorem package for the coarse-grained Poincare estimate with right-hand side, together with the auxiliary zero-Dirichlet energy estimate.

• exists_constant : ∃ (C : ℝ), 0 < C ∧ (∀ {Q : TriadicCube d} {a : CoeffFamily d} {s : ℝ} {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g), 0 < s → s < 1 → ForceBesovRegularity Q s g → scaleNormalizedNegativeBesovVectorNorm Q s (Ch02.MultiscaleExponent.finite 2) (forcedSolutionGradientField u) ≤ coarsePoincareWithRHSGradientRHS C Q a s g u) ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (v : ZeroTraceForcedCubeSolution Q a g), 0 < t → t < 1 / 2 → ForceBesovRegularity Q (2 * t) g → zeroTraceForcedSolutionEnergyNorm Q a v ≤ zeroDirichletEnergyWithRHSRHS C Q a t g

theorem HCPolySupport.Book.Ch03.coarsePoincareRHSTheory {d : ℕ} [NeZero d] : CoarsePoincareRHSTheory d

Public theorem package for the coarse-grained Poincare estimate with right-hand side and the auxiliary zero-Dirichlet energy estimate.