Coarse-graining support:

Support.Deterministic.MultiscaleQuantitiesBasic.EllipticityFiniteQ.ChangeOfQ

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

theorem HCPolySupport.le_rpow_factor_mul_of_rpow_q_div_two_le {A B F q : ℝ} (hq : 0 < q) (hA : 0 ≤ A) (hB : 0 ≤ B) (hF : 0 ≤ F) (hAB : A.rpow (q / 2) ≤ F * B.rpow (q / 2)) : A ≤ F.rpow (2 / q) * B

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_finite_rpow_q_div_two_le_changeOfQ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s p q : ℝ} (hs : 0 < s) (hp1 : 1 ≤ p) (hpq : p ≤ q) (hsum_p : Summable fun (n : ℕ) => geometricWeight s p n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (p / 2)) : (LambdaSq Q s (MultiscaleExponent.finite q) a).rpow (q / 2) ≤ geometricDiscount s q * (geometricDiscount s p).rpow (-q / p) * (LambdaSq Q s (MultiscaleExponent.finite p) a).rpow (q / 2)

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_finite_le_changeOfQ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s p q : ℝ} (hs : 0 < s) (hp1 : 1 ≤ p) (hpq : p ≤ q) (hsum_p : Summable fun (n : ℕ) => geometricWeight s p n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (p / 2)) : 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.multiscale_ellipticity_lambdaSq_finite_rpow_neg_q_div_two_le_changeOfQ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s p q : ℝ} (hs : 0 < s) (hp1 : 1 ≤ p) (hpq : p ≤ q) (hsum_p : Summable fun (n : ℕ) => geometricWeight s p n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (p / 2)) : (lambdaSq Q s (MultiscaleExponent.finite q) a).rpow (-q / 2) ≤ geometricDiscount s q * (geometricDiscount s p).rpow (-q / p) * (lambdaSq Q s (MultiscaleExponent.finite p) a).rpow (-q / 2)

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_finite_inv_le_changeOfQ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s p q : ℝ} (hs : 0 < s) (hp1 : 1 ≤ p) (hpq : p ≤ q) (hsum_p : Summable fun (n : ℕ) => geometricWeight s p n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (p / 2)) : (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)⁻¹