Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Finite.OneCubeBounds

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

Finite-exponent multiscale ellipticity: one-cube bounds

theorem HCPolySupport.Book.Ch02.LambdaSq_one_rpow_half_le_old_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ (HCPolySupport.LambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 1) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (1 / 2)

theorem HCPolySupport.Book.Ch02.lambdaSq_one_rpow_neg_half_le_old_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) ≤ (HCPolySupport.lambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 1) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (-1 / 2)

theorem HCPolySupport.Book.Ch02.old_LambdaSq_one_rpow_half_le_dim_mul_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (HCPolySupport.LambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 1) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (1 / 2) ≤ ↑d * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2)

theorem HCPolySupport.Book.Ch02.old_lambdaSq_one_rpow_neg_half_le_dim_mul_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (HCPolySupport.lambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 1) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (-1 / 2) ≤ ↑d * (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2)

theorem HCPolySupport.Book.Ch02.old_LambdaSq_two_le_dim_mul_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : HCPolySupport.LambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 2) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q)) ≤ ↑d * LambdaSq Q s (MultiscaleExponent.finite 2) a

theorem HCPolySupport.Book.Ch02.old_LambdaSq_two_rpow_half_le_dim_mul_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (HCPolySupport.LambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 2) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (1 / 2) ≤ ↑d * (LambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (1 / 2)

theorem HCPolySupport.Book.Ch02.old_lambdaSq_two_inv_le_dim_mul_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (HCPolySupport.lambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 2) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q)))⁻¹ ≤ ↑d * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹

theorem HCPolySupport.Book.Ch02.old_lambdaSq_two_rpow_neg_half_le_dim_mul_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (HCPolySupport.lambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 2) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (-1 / 2) ≤ ↑d * (lambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (-1 / 2)