Coarse-graining support: Support.Book.Ch03.ABK26.LocalCoarseGrainingResponseOrder #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Order lowering for the local coarse-graining response #
The frozen local theorem uses a q = 2 response at the local order and the
parent-truncated response at a smaller order. This module supplies that
order-lowering step before the existing exact descendant localization.
theorem
HCPolySupport.Book.Ch03.ABK26.homogenizationErrorOnCube_infinity_two_le_of_lt
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : Ch02.TriadicCoeffFamily d)
(a0 : Mat d)
{t s : ℝ}
(ht : 0 < t)
(hts : t < s)
:
For the finite q = 2 homogenization error, lowering the fractional
order can only increase the on-cube error.
theorem
HCPolySupport.Book.Ch03.ABK26.rootPointwise_descendant_infinity_two_le_parent_of_lt
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(n : ℤ)
(hn : n ≤ Q.scale)
(a : Ch02.CoeffOn (Ch02.cubeDomain Q))
(sigma0 : ℝ)
(hsigma0 : 0 < sigma0)
{R : TriadicCube d}
{k : ℤ}
(hkn : k ≤ n)
(hR : R ∈ descendantsAtScale Q k)
(t s : ↑FractionalOrder)
(hts : ↑t < ↑s)
:
ENNReal.ofReal
(Ch02.HomogenizationErrorOnCube R (↑s) Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 2)
(rootPointwiseCoeffFamily Q a) (scalarMatrix sigma0)) ≤ ENNReal.ofReal (Real.rpow 3 (↑t * ↑(n - k).toNat)) * Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar Q n hn a sigma0 hsigma0 t
A descendant's local finite-q = 2 response at order s is controlled
by the canonical parent-truncated response at every smaller positive order
t, with the existing exact triadic localization factor evaluated at t.