Coarse-graining support:

Support.Book.Ch02.Theorems.MultiscaleEllipticity.Finite.ChangeExponentDiscount

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

Finite-exponent multiscale ellipticity: discount change of exponent

theorem HCPolySupport.Book.Ch02.LambdaSqFinite_le_change_exponent_geometricDiscount {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s p q : ℝ} (hs : 0 < s) (hp1 : 1 ≤ p) (hpq : p ≤ q) : LambdaSq Q s (MultiscaleExponent.finite q) a ≤ (geometricDiscount s q).rpow (2 / q) * (geometricDiscount s p).rpow (-2 / p) * LambdaSq Q s (MultiscaleExponent.finite p) a

theorem HCPolySupport.Book.Ch02.lambdaSqFinite_inv_le_change_exponent_geometricDiscount {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s p q : ℝ} (hs : 0 < s) (hp1 : 1 ≤ p) (hpq : p ≤ q) : (lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹ ≤ (geometricDiscount s q).rpow (2 / q) * (geometricDiscount s p).rpow (-2 / p) * (lambdaSq Q s (MultiscaleExponent.finite p) a)⁻¹