Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliScaleZeroRHS.Monotonicity #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Scale-zero Caccioppoli RHS monotonicity helpers #
This child file contains the scalar monotonicity lemmas which let the scale-zero bridge enlarge public Caccioppoli RHS constants.
Audit tag #
Claim: if a public RHS constant is enlarged after multiplication by a dimension-only factor, the boundary and centered-interior scale-zero RHS terms enlarge accordingly.
Downstream target: CoarseCaccioppoliScaleZeroBridge.lean. This file is
internal bridge plumbing only and introduces no public *Theory surface.
theorem
HCPolySupport.Book.Ch03.boundaryCaccioppoliRHS_mul_const_le_of_mul_constant_le
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
{x : Vec d}
(u : BoundaryCaccioppoliDatum Q a x)
{s t M C₁ C₂ : ℝ}
(hM : 1 ≤ M)
(hC₁ : 0 ≤ C₁)
(hMC₁C₂ : M * C₁ ≤ C₂)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
:
theorem
HCPolySupport.Book.Ch03.interiorCaccioppoliRHS_mul_const_le_of_mul_constant_le
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffFamily d}
(u : CubeSolution Q a)
{s t M C₁ C₂ : ℝ}
(hM : 1 ≤ M)
(hC₁ : 0 ≤ C₁)
(hMC₁C₂ : M * C₁ ≤ C₂)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
: