Coarse-graining support:

Support.Deterministic.MultiscaleQuantitiesBasic.Foundation.CoefficientBounds

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

theorem HCPolySupport.thetaRatio_eq_div {d : ℕ} (Q : TriadicCube d) (s t : ℝ) (a : CoeffField d) : ThetaRatio Q s t a = LambdaSq Q s (MultiscaleExponent.finite 1) a / lambdaSq Q t (MultiscaleExponent.finite 1) a

@[simp]

theorem HCPolySupport.homogenizationError_finite_eq {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (q : ℝ) (a : CoeffField d) (a0 : Mat d) : HomogenizationError Q n s p (MultiscaleExponent.finite q) a a0 = HomogenizationErrorFinite Q n s p q a a0

@[simp]

theorem HCPolySupport.homogenizationError_infinity_eq {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (p : MultiscaleExponent) (a : CoeffField d) (a0 : Mat d) : HomogenizationError Q n s p MultiscaleExponent.infinity a a0 = HomogenizationErrorInfinity Q n s p a a0

theorem HCPolySupport.homogenizationErrorOnCube_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : MultiscaleExponent) (a : CoeffField d) (a0 : Mat d) : HomogenizationErrorOnCube Q s p q a a0 = HomogenizationError Q Q.scale s p q a a0

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_one_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) : LambdaSq Q s (MultiscaleExponent.finite 1) a = LambdaSqFinite Q s 1 a

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_one_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) : lambdaSq Q s (MultiscaleExponent.finite 1) a = lambdaSqFinite Q s 1 a

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem HCPolySupport.thetaRatio_eq_div_finite_one {d : ℕ} (Q : TriadicCube d) (s t : ℝ) (a : CoeffField d) : ThetaRatio Q s t a = LambdaSqFinite Q s 1 a / lambdaSqFinite Q t 1 a

theorem HCPolySupport.homogenizationError_infinity_one_eq {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (a : CoeffField d) (a0 : Mat d) : HomogenizationError Q n s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 = HomogenizationErrorFinite Q n s MultiscaleExponent.infinity 1 a a0

@[simp]

theorem HCPolySupport.homogenizationErrorFinite_infinity_one_eq_tsum {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (a : CoeffField d) (a0 : Mat d) : HomogenizationErrorFinite Q n s MultiscaleExponent.infinity 1 a a0 = ∑' (l : ℕ), geometricWeight s 1 l * scaleResponseAtScale Q (n - ↑l) MultiscaleExponent.infinity a a0

theorem HCPolySupport.homogenizationErrorFinite_infinity_one_formula {d : ℕ} (Q : TriadicCube d) (n : ℤ) (s : ℝ) (a : CoeffField d) (a0 : Mat d) : HomogenizationErrorFinite Q n s MultiscaleExponent.infinity 1 a a0 = ∑' (l : ℕ), geometricWeight s 1 l * (maxDescendantNormalizedBlockResponseAtScale Q (n - ↑l) a a0).rpow (1 / 2)

@[simp]

theorem HCPolySupport.homogenizationErrorOnCube_infinity_one_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (a0 : Mat d) : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 = HomogenizationErrorFinite Q Q.scale s MultiscaleExponent.infinity 1 a a0

theorem HCPolySupport.homogenizationErrorOnCube_infinity_one_eq_tsum {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (a0 : Mat d) : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 = ∑' (l : ℕ), geometricWeight s 1 l * scaleResponseAtScale Q (Q.scale - ↑l) MultiscaleExponent.infinity a a0

theorem HCPolySupport.homogenizationErrorOnCube_infinity_one_formula {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) (a0 : Mat d) : HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) a a0 = ∑' (l : ℕ), geometricWeight s 1 l * (maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑l) a a0).rpow (1 / 2)

theorem HCPolySupport.coarseBBlockNorm_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : 0 ≤ coarseBBlockNorm Q a

theorem HCPolySupport.coarseSigmaStarInvBlockNorm_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : 0 ≤ coarseSigmaStarInvBlockNorm Q a

theorem HCPolySupport.coarseBBlockNorm_le_maxDescendantBBlockNormAtScale_of_isEllipticFieldOn_of_isSigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) : coarseBBlockNorm Q a ≤ maxDescendantBBlockNormAtScale Q k a

theorem HCPolySupport.coarseSigmaStarInvBlockNorm_le_maxDescendantSigmaStarInvNorm {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) : coarseSigmaStarInvBlockNorm Q a ≤ maxDescendantSigmaStarInvNormAtScale Q k a

@[simp]

theorem HCPolySupport.maxDescendantBBlockNormAtScale_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : maxDescendantBBlockNormAtScale Q Q.scale a = coarseBBlockNorm Q a

@[simp]

theorem HCPolySupport.maxDescendantNormalizedBlockResponseAtScale_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) : maxDescendantNormalizedBlockResponseAtScale Q Q.scale a a0 = normalizedBlockResponseMax Q a a0

theorem HCPolySupport.scaleResponseAtScale_finite_self_eq {d : ℕ} (Q : TriadicCube d) (p : ℝ) (a : CoeffField d) (a0 : Mat d) : scaleResponseAtScale Q Q.scale (MultiscaleExponent.finite p) a a0 = ((normalizedBlockResponseMax Q a a0).rpow (p / 2)).rpow (1 / p)

theorem HCPolySupport.scaleResponseAtScale_infinity_self_eq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) : scaleResponseAtScale Q Q.scale MultiscaleExponent.infinity a a0 = (normalizedBlockResponseMax Q a a0).rpow (1 / 2)

@[simp]

theorem HCPolySupport.maxDescendantSigmaStarInvNormAtScale_self {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) : maxDescendantSigmaStarInvNormAtScale Q Q.scale a = coarseSigmaStarInvBlockNorm Q a

theorem HCPolySupport.coarseBBlockNorm_le_maxDescendantBBlockNormAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (hR : R ∈ descendantsAtScale Q k) : coarseBBlockNorm R a ≤ maxDescendantBBlockNormAtScale Q k a

theorem HCPolySupport.coarseSigmaStarInvBlockNorm_le_maxDescendantSigmaStarInvNormAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (a : CoeffField d) (hR : R ∈ descendantsAtScale Q k) : coarseSigmaStarInvBlockNorm R a ≤ maxDescendantSigmaStarInvNormAtScale Q k a