Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.Theorems.CoarseCaccioppoliRHS.Prefactors

Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliRHS.Prefactors #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Coarse Caccioppoli with RHS Prefactors #

This file is split mechanically out of CoarseCaccioppoliRHS.lean.

Audit tag #

Claim: convert homogeneous Caccioppoli prefactors into the with-RHS prefactor normalization used by the public boundary estimate.

Downstream target: CoarseCaccioppoliRHS/ZeroTraceValue.lean. This file should stay scalar-prefactor algebra, not analytic bridge packaging.

source
theorem HCPolySupport.Book.Ch03.caccioppoliPrefactor_eq_caccioppoliWithRHSPrefactor_mul_lambdaS_scale {d : ℕ} [NeZero d] {C : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) :
caccioppoliPrefactor C Q a s t = caccioppoliWithRHSPrefactor C Q a s t * (Ch02.lambdaS Q t a * Real.rpow 3 (-2 * ↑Q.scale))

Scalar identity converting the homogeneous Caccioppoli prefactor into the first term of the forced Caccioppoli RHS.

source
theorem HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor_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 ≤ caccioppoliWithRHSPrefactor C Q a s t

The forced Caccioppoli scalar prefactor is nonnegative in the theorem range.

source
theorem HCPolySupport.Book.Ch03.one_le_caccioppoliWithRHSPrefactor {d : ℕ} [NeZero d] {C : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} (hC : 1 ≤ C) (hs : 0 < s) (hs_lt : s < 1) (ht : 0 < t) (hst : s + t < 1) :
1 ≤ caccioppoliWithRHSPrefactor C Q a s t

With the displayed constant at least 1, the forced Caccioppoli prefactor is at least 1 throughout the theorem range.

source
theorem HCPolySupport.Book.Ch03.sq_le_caccioppoliWithRHSPrefactor {d : ℕ} [NeZero d] {C : ℝ} {Q : TriadicCube d} {a : CoeffFamily d} {s t : ℝ} (hC : 1 ≤ C) (hs : 0 < s) (hs_lt : s < 1) (ht : 0 < t) (hst : s + t < 1) :
C ^ 2 ≤ caccioppoliWithRHSPrefactor C Q a s t

A slightly stronger lower bound: the forced prefactor contains at least C^2 when C >= 1. This lets a large final dimension constant absorb dimension-only multiples of the forcing summand.