Coarse-graining support: Support.Deterministic.CoarsePoincare.Setup.UniformBounds

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

theorem HCPolySupport.maxDescendantBBlockNorm_le_uniform_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (n : ℕ) : maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a ≤ 4 * ↑(Fintype.card (Fin d)) * lam⁻¹ * Lam ^ 2

theorem HCPolySupport.maxDescendantSigmaStarInvNorm_le_uniform_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (n : ℕ) : maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a ≤ 4 * ↑(Fintype.card (Fin d)) * lam⁻¹

theorem HCPolySupport.maxDescendantBBlockNorm_le_uniform_of_ellipticField_openCubeSet {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (n : ℕ) : maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a ≤ 4 * ↑(Fintype.card (Fin d)) * lam⁻¹ * Lam ^ 2

theorem HCPolySupport.maxDescendantSigmaStarInvNorm_le_uniform_of_ellipticField_openCubeSet {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (n : ℕ) : maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a ≤ 4 * ↑(Fintype.card (Fin d)) * lam⁻¹

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

theorem HCPolySupport.summable_qone_maxDescendantSigmaStarInvNorm_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_qone_maxDescendantBBlockNorm_of_ellipticField_openCubeSet {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) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_qone_maxDescendantSigmaStarInvNorm_of_ellipticField_openCubeSet {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) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_qtwo_maxDescendantBBlockNorm_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a

theorem HCPolySupport.summable_qtwo_maxDescendantSigmaStarInvNorm_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a

theorem HCPolySupport.summable_qone_maxDescendantBBlockNorm_of_ellipticField_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_exponentOne_maxDescendantBBlockNorm_of_cubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_qone_maxDescendantSigmaStarInvNorm_of_ellipticField_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_exponentOne_maxDescendantSigmaStarInverseNorm_of_cubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

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

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

theorem HCPolySupport.summable_qone_maxDescendantSigmaStarInvNorm_of_ellipticField_of_openCubeSet {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_exponentOne_maxDescendantSigmaStarInverseNorm_of_openCubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)

theorem HCPolySupport.summable_qtwo_maxDescendantBBlockNorm_of_ellipticField_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a

theorem HCPolySupport.summable_exponentTwo_maxDescendantBBlockNorm_of_cubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a

theorem HCPolySupport.summable_qtwo_maxDescendantSigmaStarInvNorm_of_ellipticField_of_ellipticField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a

theorem HCPolySupport.summable_exponentTwo_maxDescendantSigmaStarInverseNorm_of_cubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a

theorem HCPolySupport.cubeAverage_nonneg_of_nonneg_on {d : ℕ} {Q : TriadicCube d} {f : Vec d → ℝ} (hf : ∀ x ∈ cubeSet Q, 0 ≤ f x) : 0 ≤ cubeAverage Q f

theorem HCPolySupport.volumeAverage_cubeSet_eq_cubeAverage {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : volumeAverage (cubeSet Q) f = cubeAverage Q f

theorem HCPolySupport.cubeAverage_eq_of_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f g : Vec d → ℝ} (hfg : ∀ x ∈ cubeSet Q, f x = g x) : cubeAverage Q f = cubeAverage Q g

theorem HCPolySupport.cubeAverageVec_eq_of_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f g : Vec d → Vec d} (hfg : ∀ x ∈ cubeSet Q, f x = g x) : cubeAverageVec Q f = cubeAverageVec Q g