PublicRHSMonotonicity

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

Public RHS monotonicity for coarse Caccioppoli with RHS

This file contains the scalar constant-enlargement lemmas for the public boundary Caccioppoli RHS with forcing.

Audit tag

Claim: increasing the displayed public RHS constants increases the homogeneous and forced Caccioppoli prefactors, and therefore the full public with-RHS boundary quantity.

Downstream target: CoarseCaccioppoliRHS/FinalBounds.lean. This is scalar bridge plumbing only and introduces no public *Theory package.

theorem HCPolySupport.Book.Ch03.caccioppoliPrefactor_nonneg {d : ℕ} [NeZero d] {C : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} (hC_nonneg : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : 0 ≤ caccioppoliPrefactor C Q a s t

The homogeneous Caccioppoli prefactor is nonnegative in the theorem range.

theorem HCPolySupport.Book.Ch03.rhs_const_mul_rpow_le_rpow_of_mul_le {M x y p : ℝ} (hM : 1 ≤ M) (hx : 0 ≤ x) (hMxy : M * x ≤ y) (hp : 1 ≤ p) : M * x.rpow p ≤ y.rpow p

If the base constant is enlarged by a multiplicative factor, then the corresponding real-power factor absorbs one copy of that factor.

theorem HCPolySupport.Book.Ch03.caccioppoliPrefactor_mul_const_le_of_mul_constant_le {d : ℕ} {M C₁ C₂ : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} (hM : 1 ≤ M) (hC₁ : 0 ≤ C₁) (hMC₁C₂ : M * C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : M * caccioppoliPrefactor C₁ Q a s t ≤ caccioppoliPrefactor C₂ Q a s t

Multiplicative enlargement of the dimension constant absorbs the same constant multiple of the homogeneous Caccioppoli prefactor.

theorem HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor_mul_const_le_of_mul_constant_le {d : ℕ} {M C₁ C₂ : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} (hM : 1 ≤ M) (hC₁ : 0 ≤ C₁) (hMC₁C₂ : M * C₁ ≤ C₂) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : M * caccioppoliWithRHSPrefactor C₁ Q a s t ≤ caccioppoliWithRHSPrefactor C₂ Q a s t

Multiplicative enlargement also absorbs the same constant multiple of the forced Caccioppoli prefactor.

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliWithRHSRHS_mul_const_le_of_mul_constant_le {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 * boundaryCaccioppoliWithRHSRHS C₁ s t u ≤ boundaryCaccioppoliWithRHSRHS C₂ s t u

Multiplicative enlargement of the public constant absorbs the same constant multiple of the entire displayed forced RHS.