FinalBounds

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

Final Boundary Bounds for Coarse Caccioppoli with RHS

This file is split mechanically out of CoarseCaccioppoliRHS.lean.

Audit tag

Claim: combine homogeneous Caccioppoli, zero-trace corrector bounds, and scalar absorptions into the final public boundary with-RHS estimate.

Downstream target: CoarseCaccioppoliRHS/Bridges.lean. This file should stay as final-bound assembly, with no extra public *Theory surface.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCorrector_parentL2_term_le_RHS_of_scaled_force_bound {d : ℕ} [NeZero d] {K C_hom C_final : ℝ} (hM : 1 ≤ 4 * K) (hC_hom_nonneg : 0 ≤ C_hom) (hMC : 4 * K * C_hom ≤ C_final) {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hs : 0 < s) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) (hscaled : 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)) : 4 * caccioppoliPrefactor C_hom Q a s t * normalizedL2SqOnSet (openCubeSet Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toFun ≤ boundaryCaccioppoliWithRHSRHS C_final s t u

Coarse-form absorption of the zero-trace corrector parent L² term.

This is the scalar bridge matching the LaTeX proof after the corrector parent L² estimate has been stated with the coarse lower ellipticity: lambdaS * scale^{-2} * ||ρ||² <= K * forceTerm. No uniform ellipticity constant appears in the conclusion.

theorem HCPolySupport.Book.Ch03.caccioppoliPrefactor_const_mul_forcedParentL2_le_boundaryCaccioppoliWithRHSRHS {d : ℕ} [NeZero d] {M C₁ C₂ : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (hM : 1 ≤ M) (hC₁ : 0 ≤ C₁) (hMC₁C₂ : M * C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) : M * caccioppoliPrefactor C₁ Q a s t * boundaryForcedCaccioppoliParentL2Sq u ≤ boundaryCaccioppoliWithRHSRHS C₂ s t u

The first forced RHS summand absorbs a constant multiple of the homogeneous parent contribution after enlarging the public dimension constant.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCoreEnergy_le_split_homogeneous_corrector {d : ℕ} [NeZero d] {C : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hhom : boundaryCaccioppoliCoreEnergy (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem) ≤ boundaryCaccioppoliRHS C s t (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem)) : boundaryForcedCaccioppoliCoreEnergy u ≤ 4 * caccioppoliPrefactor C Q a s t * boundaryForcedCaccioppoliParentL2Sq u + 4 * caccioppoliPrefactor C Q a s t * normalizedL2SqOnSet (openCubeSet Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toFun + 2 * localizedCoeffEnergyValue (caccioppoliCoreSet Q x) (a.coeffOn Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toH1Function

Exact split after subtracting the zero-trace corrector and applying the homogeneous Caccioppoli estimate to the harmonic remainder.

This is the PDE assembly core. The remaining work for the final theorem is pure scalar absorption of the two corrector terms into the displayed forced right-hand side.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCoreEnergy_le_split_homogeneous_zeroDirichlet {d : ℕ} [NeZero d] {C C₀ : ℝ} (hC_nonneg : 0 ≤ C) (hC₀_nonneg : 0 ≤ C₀) (hC₀_zero : √(250 + 2 * √15000 * √2) * (↑d * Real.rpow 3 (↑d + 1)) ≤ C₀) {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) (hs : 0 < s) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) (hx : x ∈ openCubeSet Q) (hg : ForceBesovRegularity Q (2 * t) g) (hhom : boundaryCaccioppoliCoreEnergy (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem) ≤ boundaryCaccioppoliRHS C s t (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem)) : boundaryForcedCaccioppoliCoreEnergy u ≤ 4 * caccioppoliPrefactor C Q a s t * boundaryForcedCaccioppoliParentL2Sq u + 4 * caccioppoliPrefactor C Q a s t * normalizedL2SqOnSet (openCubeSet Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toFun + 2 * (18 ^ d * zeroDirichletEnergyWithRHSRHS (↑d * C₀) Q a t g ^ 2)

Split form with the corrector core energy already bounded by the public zero-Dirichlet RHS estimate. The only analytic term still not absorbed is the corrector parent L² contribution.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCoreEnergy_le_RHS_of_correctorParent_absorption {d : ℕ} [NeZero d] {C_hom C₀ C_inner C_final : ℝ} (hC_hom_nonneg : 0 ≤ C_hom) (hC₀_nonneg : 0 ≤ C₀) (hC₀_zero : √(250 + 2 * √15000 * √2) * (↑d * Real.rpow 3 (↑d + 1)) ≤ C₀) (hC_inner_one : 1 ≤ C_inner) (h4_hom_inner : 4 * C_hom ≤ C_inner) (hzero_inner : 2 * 18 ^ d * (25 * Real.exp 4 * (↑d * C₀) ^ 2) ≤ C_inner ^ 2) (h3_inner_final : 3 * C_inner ≤ C_final) {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) (hs : 0 < s) (hs_lt : s < 1) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) (hx : x ∈ openCubeSet Q) (hg : ForceBesovRegularity Q (2 * t) g) (hhom : boundaryCaccioppoliCoreEnergy (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem) ≤ boundaryCaccioppoliRHS C_hom s t (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem)) (hcorrectorParent : 4 * caccioppoliPrefactor C_hom Q a s t * normalizedL2SqOnSet (openCubeSet Q) (boundaryForcedCaccioppoliCorrectorOpenH10 ρ).toFun ≤ boundaryCaccioppoliWithRHSRHS C_inner s t u) : boundaryForcedCaccioppoliCoreEnergy u ≤ boundaryCaccioppoliWithRHSRHS C_final s t u

Conditional final assembly for the forced boundary Caccioppoli estimate.

All PDE and scalar pieces have been discharged here except the genuinely analytic input controlling the zero-trace corrector's parent L² term. Once that bridge is supplied in the hcorrectorParent hypothesis, the displayed public RHS follows after one last constant enlargement.

theorem HCPolySupport.Book.Ch03.boundaryForcedCaccioppoliCoreEnergy_le_RHS_of_correctorParent_scaled_force_bound {d : ℕ} [NeZero d] {K C_hom C₀ C_inner C_final : ℝ} (hK_enlarge : 1 ≤ 4 * K) (hC_hom_nonneg : 0 ≤ C_hom) (hC₀_nonneg : 0 ≤ C₀) (hC₀_zero : √(250 + 2 * √15000 * √2) * (↑d * Real.rpow 3 (↑d + 1)) ≤ C₀) (hC_inner_one : 1 ≤ C_inner) (h4_hom_inner : 4 * C_hom ≤ C_inner) (hcorrector_inner : 4 * K * C_hom ≤ C_inner) (hzero_inner : 2 * 18 ^ d * (25 * Real.exp 4 * (↑d * C₀) ^ 2) ≤ C_inner ^ 2) (h3_inner_final : 3 * C_inner ≤ C_final) {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (ρ : ZeroTraceDirichletCorrectorData Q (publicCoeffField Q a) g) (hg_mem : MemVectorL2 (cubeSet Q) g) (hs : 0 < s) (hs_lt : s < 1) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) (hx : x ∈ openCubeSet Q) (hg : ForceBesovRegularity Q (2 * t) g) (hhom : boundaryCaccioppoliCoreEnergy (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem) ≤ boundaryCaccioppoliRHS C_hom s t (boundaryForcedCaccioppoliRemainderDatum u ρ hg_mem)) (hcorrectorScaled : 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)) : boundaryForcedCaccioppoliCoreEnergy u ≤ boundaryCaccioppoliWithRHSRHS C_final s t u

Conditional final assembly using the coarse-scaled parent L² estimate for the zero-trace corrector.

Compared with boundaryForcedCaccioppoliCoreEnergy_le_RHS_of_correctorParent_absorption, this is the theorem-shape reduction that remains faithful to the displayed Caccioppoli-with-RHS estimate: the remaining analytic input is precisely a bound for lambdaS * scale^{-2} * ||ρ||²_parent by a dimension-only multiple of the forcing summand.