Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Ellipticity.QOneRoot

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

q = 1 ellipticity and localization

theorem HCPolySupport.sqrt_coarseBBlockNorm_le_sqrt_maxDescendantBBlockNormAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (hR : R ∈ descendantsAtScale Q k) : (coarseBBlockNorm R a).rpow (1 / 2) ≤ (maxDescendantBBlockNormAtScale Q k a).rpow (1 / 2)

theorem HCPolySupport.sqrt_coarseSigmaStarInvBlockNorm_le_sqrt_maxDescendantSigmaStarInvNormAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (hR : R ∈ descendantsAtScale Q k) : (coarseSigmaStarInvBlockNorm R a).rpow (1 / 2) ≤ (maxDescendantSigmaStarInvNormAtScale Q k a).rpow (1 / 2)

theorem HCPolySupport.geometricWeight_mul_sqrt_coarseBBlockNorm_le {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (s q : ℝ) (n : ℕ) (hsq : 0 ≤ s * q) (hR : R ∈ descendantsAtScale Q k) : geometricWeight s q n * (coarseBBlockNorm R a).rpow (1 / 2) ≤ geometricWeight s q n * (maxDescendantBBlockNormAtScale Q k a).rpow (1 / 2)

theorem HCPolySupport.geometricWeight_mul_sqrt_coarseSigmaStarInvBlockNorm_le {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (s q : ℝ) (n : ℕ) (hsq : 0 ≤ s * q) (hR : R ∈ descendantsAtScale Q k) : geometricWeight s q n * (coarseSigmaStarInvBlockNorm R a).rpow (1 / 2) ≤ geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q k a).rpow (1 / 2)

theorem HCPolySupport.weighted_sqrt_coarseBBlockNorm_le_LambdaSqFinite_one_series {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hR : R ∈ descendantsAtScale Q k) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricWeight s 1 (Q.scale - k).toNat * (coarseBBlockNorm R a).rpow (1 / 2) ≤ ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.weighted_sqrt_coarseSigmaStarInvBlockNorm_le_lambdaSqFinite_one_series {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hR : R ∈ descendantsAtScale Q k) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricWeight s 1 (Q.scale - k).toNat * (coarseSigmaStarInvBlockNorm R a).rpow (1 / 2) ≤ ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.weighted_sqrt_coarseBBlockNorm_le_LambdaSq_one_rpow_half {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hR : R ∈ descendantsAtScale Q k) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricWeight s 1 (Q.scale - k).toNat * (coarseBBlockNorm R a).rpow (1 / 2) ≤ (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2)

theorem HCPolySupport.weighted_sqrt_coarseSigmaStarInvBlockNorm_le_lambdaSq_one_rpow_neg_half {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hR : R ∈ descendantsAtScale Q k) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricWeight s 1 (Q.scale - k).toNat * (coarseSigmaStarInvBlockNorm R a).rpow (1 / 2) ≤ (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2)

theorem HCPolySupport.geometricDiscount_mul_sqrt_coarseBBlockNorm_le_LambdaSqFinite_one_series {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricDiscount s 1 * (coarseBBlockNorm Q a).rpow (1 / 2) ≤ ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.geometricDiscount_mul_sqrt_coarseSigmaStarInvBlockNorm_le_lambdaSqFinite_one_series {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricDiscount s 1 * (coarseSigmaStarInvBlockNorm Q a).rpow (1 / 2) ≤ ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.geometricDiscount_mul_sqrt_coarseBBlockNorm_le_LambdaSq_one_rpow_half {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricDiscount s 1 * (coarseBBlockNorm Q a).rpow (1 / 2) ≤ (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2)

theorem HCPolySupport.geometricDiscount_mul_sqrt_coarseSigmaStarInvBlockNorm_le_lambdaSq_one_rpow_neg_half {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 ≤ s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricDiscount s 1 * (coarseSigmaStarInvBlockNorm Q a).rpow (1 / 2) ≤ (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2)

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_series_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (hs : 0 ≤ s) : 0 ≤ ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_series_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (hs : 0 ≤ s) : 0 ≤ ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (hs : 0 ≤ s) : 0 ≤ LambdaSq Q s (MultiscaleExponent.finite 1) a

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (hs : 0 ≤ s) : 0 ≤ lambdaSq Q s (MultiscaleExponent.finite 1) a

theorem HCPolySupport.matNorm_pos_of_posDef {d : ℕ} [NeZero d] {A : Mat d} (hA : Matrix.PosDef A) : 0 < matNorm A

theorem HCPolySupport.coarseBBlockNorm_pos_of_isEllipticFieldOn_of_openCubeData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDeterministicCoarseData Q a) : 0 < coarseBBlockNorm Q a

theorem HCPolySupport.coarseSigmaStarInvBlockNorm_pos_of_openCubeData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (hData : OpenCubeDeterministicCoarseData Q a) : 0 < coarseSigmaStarInvBlockNorm Q a

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_series_pos_of_isEllipticFieldOn_of_openCubeData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : 0 < ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_series_pos_of_openCubeData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 < s) (hData : OpenCubeDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : 0 < ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_pos_of_isEllipticFieldOn_of_openCubeData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : 0 < LambdaSq Q s (MultiscaleExponent.finite 1) a

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_pos_of_openCubeData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 < s) (hData : OpenCubeDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : 0 < lambdaSq Q s (MultiscaleExponent.finite 1) a

theorem HCPolySupport.thetaRatio_pos_of_isEllipticFieldOn_of_openCubeData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s t lam Lam : ℝ} (hs : 0 < s) (ht : 0 < t) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDeterministicCoarseData Q a) (hBsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : 0 < ThetaRatio Q s t a

theorem HCPolySupport.sq_rpow_half_eq_self_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x.rpow (1 / 2) ^ 2 = x

theorem HCPolySupport.sq_rpow_neg_half_eq_inv_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x.rpow (-1 / 2) ^ 2 = x⁻¹

theorem HCPolySupport.geometricDiscount_sq_mul_coarseBBlockNorm_le_LambdaSq_one {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricDiscount s 1 ^ 2 * coarseBBlockNorm Q a ≤ LambdaSq Q s (MultiscaleExponent.finite 1) a

theorem HCPolySupport.geometricDiscount_sq_mul_coarseSigmaStarInvBlockNorm_le_lambdaSq_one_inv {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : geometricDiscount s 1 ^ 2 * coarseSigmaStarInvBlockNorm Q a ≤ (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹

theorem HCPolySupport.coarseBBlockNorm_le_LambdaSq_one_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : coarseBBlockNorm Q a ≤ LambdaSq Q s (MultiscaleExponent.finite 1) a

theorem HCPolySupport.coarseSigmaStarInvBlockNorm_le_lambdaSq_one_inv_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : coarseSigmaStarInvBlockNorm Q a ≤ (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_rpow_half_eq_tsum {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (hs : 0 ≤ s) : (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) = ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_rpow_neg_half_eq_tsum {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (hs : 0 ≤ s) : (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) = ∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_rpow_half_le_of_lt_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {t s lam Lam : ℝ} (ht : 0 < t) (hts : t < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ (LambdaSq Q t (MultiscaleExponent.finite 1) a).rpow (1 / 2)

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_le_of_lt_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {t s lam Lam : ℝ} (ht : 0 < t) (hts : t < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : LambdaSq Q s (MultiscaleExponent.finite 1) a ≤ LambdaSq Q t (MultiscaleExponent.finite 1) a

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_rpow_neg_half_le_of_lt_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {t s lam Lam : ℝ} (ht : 0 < t) (hts : t < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) ≤ (lambdaSq Q t (MultiscaleExponent.finite 1) a).rpow (-1 / 2)

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_inv_le_of_lt_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {t s lam Lam : ℝ} (ht : 0 < t) (hts : t < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹ ≤ (lambdaSq Q t (MultiscaleExponent.finite 1) a)⁻¹