Bridges

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Internal Parent-L2 Bounds for Coarse Caccioppoli with RHS

This file is split mechanically out of CoarseCaccioppoliRHS.lean.

Audit tag

Claim: prove the parent-L² estimate for the zero-trace corrector and expose only the raw bound consumed by the public theorem package.

Downstream target: CoarseCaccioppoliRHS/Theory.lean. This file should not spawn public bridge packages or parallel theorem theories.

theorem HCPolySupport.Book.Ch03.zeroTraceCorrectorParentL2_le_forceScale {d : ℕ} [NeZero d] : ∃ (K : ℝ), 0 < K ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g), 0 < t → t < 1 / 2 → ForceBesovRegularity Q (2 * t) g → Ch02.lambdaS Q t a * Real.rpow 3 (-2 * ↑Q.scale) * normalizedL2SqOnSet (openCubeSet Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toFun ≤ K * (t.rpow (-8) / (1 - 2 * t) * (Ch02.lambdaS Q t a).rpow (-1) * scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2)

Proved coarse parent L² bound for the zero-trace corrector.