LocalCoarseGrainingAssemblyAlgebra #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
Finite-p algebra for local coarse-graining assembly #
This module records the outer finite descendant-average triangle estimate in
the literal ENNReal carrier used by the local coarse-graining definitions.
It is independent of the PDE and response inputs.
theorem
HCPolySupport.Book.Ch03.ABK26.descendantsAtScaleENNAverage_rpow_add_le
{d : ℕ}
(Q : TriadicCube d)
(k : ℤ)
{r : ℝ}
(hr : 1 ≤ r)
(F G : TriadicCube d → ENNReal)
:
(descendantsAtScaleENNAverage Q k fun (R : TriadicCube d) => (F R + G R) ^ r) ≤ 2 ^ (r - 1) * ((descendantsAtScaleENNAverage Q k fun (R : TriadicCube d) => F R ^ r) + descendantsAtScaleENNAverage Q k fun (R : TriadicCube d) => G R ^ r)
The finite outer descendant average obeys the powered two-term triangle
inequality. This is the algebraic form used before taking the single outer
finite-p root in the local coarse-graining assembly.
theorem
HCPolySupport.Book.Ch03.ABK26.descendantsAtScaleENNAverage_rpow_add_root_le_two_mul
{d : ℕ}
(Q : TriadicCube d)
(k : ℤ)
{r : ℝ}
(hr : 1 ≤ r)
(F G : TriadicCube d → ENNReal)
:
(descendantsAtScaleENNAverage Q k fun (R : TriadicCube d) => (F R + G R) ^ r) ^ r⁻¹ ≤ 2 * ((descendantsAtScaleENNAverage Q k fun (R : TriadicCube d) => F R ^ r) + descendantsAtScaleENNAverage Q k fun (R : TriadicCube d) => G R ^ r) ^ r⁻¹
After the outer finite-p root, the preceding two-term descendant-average
triangle loss is the uniform constant 2.