PublicRHSScalar

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

Public RHS Scalar Bounds for Coarse Caccioppoli with RHS

This file is split mechanically out of CoarseCaccioppoliRHS.lean.

Audit tag

Claim: prove nonnegativity and scalar monotonicity facts for the public boundaryCaccioppoliWithRHSRHS terms.

Downstream target: CoarseCaccioppoliRHS/FinalBounds.lean. This file should contain scalar RHS bounds only; public theorem packages belong in CoarseCaccioppoliRHS/Theory.lean.

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliWithRHS_forceTerm_nonneg {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (ht : 0 < t) (ht_lt : t < 1 / 2) : 0 ≤ t.rpow (-8) / (1 - 2 * t) * (Ch02.lambdaS Q t a).rpow (-1) * scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2

The forcing-only term inside boundaryCaccioppoliWithRHSRHS is nonnegative.

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliWithRHSRHS_nonneg {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) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) : 0 ≤ boundaryCaccioppoliWithRHSRHS C s t u

The displayed forced boundary Caccioppoli RHS is nonnegative in the theorem range.

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliWithRHS_forceTerm_le_RHS {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) (hC : 1 ≤ C) (hs : 0 < s) (hs_lt : s < 1) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) : t.rpow (-8) / (1 - 2 * t) * (Ch02.lambdaS Q t a).rpow (-1) * scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2 ≤ boundaryCaccioppoliWithRHSRHS C s t u

The forcing-only summand is contained in the displayed RHS once the prefactor constant is at least 1.

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliWithRHS_const_mul_forceTerm_le_RHS {d : ℕ} [NeZero d] {K C : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (hKC : K ≤ C ^ 2) (hC : 1 ≤ C) (hs : 0 < s) (hs_lt : s < 1) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) : K * (t.rpow (-8) / (1 - 2 * t) * (Ch02.lambdaS Q t a).rpow (-1) * scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2) ≤ boundaryCaccioppoliWithRHSRHS C s t u

Any dimension-only multiple already bounded by C^2 of the forcing summand is contained in the displayed RHS. This is the scalar absorption hook used after the corrector estimates have been reduced to the forcing summand.

theorem HCPolySupport.Book.Ch03.zeroDirichletEnergyWithRHSRHS_sq_le_const_mul_forceTerm {d : ℕ} [NeZero d] {C₀ : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (ht : 0 < t) (ht_lt : t < 1 / 2) : zeroDirichletEnergyWithRHSRHS C₀ Q a t g ^ 2 ≤ 25 * Real.exp 4 * C₀ ^ 2 * (t.rpow (-8) / (1 - 2 * t) * (Ch02.lambdaS Q t a).rpow (-1) * scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2)

The squared zero-Dirichlet RHS is controlled by the forcing summand used in the boundary Caccioppoli-with-RHS statement. This is the scalar q = 2 to q = 1 lower-ellipticity conversion plus the t^{-8} buffer.

theorem HCPolySupport.Book.Ch03.lambdaS_mul_tpow_lambdaSqTwo_inv_sq_le_forceTime {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffFamily d} {t B : ℝ} (ht : 0 < t) (ht_lt : t < 1 / 2) : Ch02.lambdaS Q t a * (t.rpow (-3) * (Ch02.lambdaSq Q t (Ch02.MultiscaleExponent.finite 2) a).rpow (-1) * B) ^ 2 ≤ (25 * Real.exp 4) ^ 2 * (t.rpow (-8) * (Ch02.lambdaS Q t a).rpow (-1) * B ^ 2)

Squared lower-ellipticity conversion used for the corrector parent L² bridge.

The public RHS Poincare estimate gives the corrector gradient with a lambda_{t,2}^{-1} factor. After squaring and multiplying by lambdaS this lemma converts the two q = 2 lower-ellipticity factors to the displayed q = 1 factor, spending exactly the t^{-8} buffer.

theorem HCPolySupport.Book.Ch03.coarsePoincareWithRHSGradientRHS_le_corrector_forceScale {d : ℕ} [NeZero d] {C : ℝ} (hC_nonneg : 0 ≤ C) {Q : TriadicCube d} {a : CoeffFamily d} {t : ℝ} {g : Vec d → Vec d} (u : ForcedCubeSolution Q a g) (ht : 0 < t) (_ht_lt : t < 1 / 2) (hg : ForceBesovRegularity Q (2 * t) g) (henergy : forcedSolutionEnergyNorm Q a u ≤ zeroDirichletEnergyWithRHSRHS C Q a t g) : coarsePoincareWithRHSGradientRHS C Q a (2 * t) g u ≤ (C ^ 2 + C) * (t.rpow (-3) * (Ch02.lambdaSq Q t (Ch02.MultiscaleExponent.finite 2) a).rpow (-1) * scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g)

Once the zero-Dirichlet energy estimate is inserted, the public RHS Poincare gradient bound for the zero-trace corrector has the exact force scale needed by the Caccioppoli parent L² bridge.

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliWithRHS_zeroDirichletSqTerm_le_RHS {d : ℕ} [NeZero d] {C C₀ : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} {x : Vec d} {g : Vec d → Vec d} (u : BoundaryForcedCaccioppoliDatum Q a x g) (hKC : 2 * 18 ^ d * (25 * Real.exp 4 * C₀ ^ 2) ≤ C ^ 2) (hC : 1 ≤ C) (hs : 0 < s) (hs_lt : s < 1) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) : 2 * (18 ^ d * zeroDirichletEnergyWithRHSRHS C₀ Q a t g ^ 2) ≤ boundaryCaccioppoliWithRHSRHS C s t u

The corrector core-energy scalar term produced by the zero-Dirichlet estimate is absorbed by the forcing part of the final RHS once the final constant is large enough.

theorem HCPolySupport.Book.Ch03.caccioppoliPrefactor_mul_forcedParentL2_le_boundaryCaccioppoliWithRHSRHS {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) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (ht_lt : t < 1 / 2) (hst : s + t < 1) : caccioppoliPrefactor C Q a s t * boundaryForcedCaccioppoliParentL2Sq u ≤ boundaryCaccioppoliWithRHSRHS C s t u

The first term of the forced boundary Caccioppoli RHS contains the homogeneous parent-L² contribution with the same displayed prefactor.