Coarse-graining support: Support.CoarseGraining.OriginCubeEllipticRecovery.Translate

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

Origin-cube elliptic recovery -- translated and descendant variants

Quadraticity / coarse-block-matrix existence on translateSet variants of the centered open cube and on openCubeSet / cubeSet of an arbitrary TriadicCube, produced by transporting recovery data through translations.

theorem HCPolySupport.hasQuadraticMu_translateSet_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} {n : ℤ} (z : Vec d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R (translateCoeffField z a)) : HasQuadraticMu (translateSet z (openCubeSet (originCube d n))) a

Translate origin-cube elliptic recovery data for the shifted field translateCoeffField z a into quadraticity of Mu on the translated open cube.

theorem HCPolySupport.exists_coarseBlockMatrix_translateSet_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} {n : ℤ} (z : Vec d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R (translateCoeffField z a)) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (translateSet z (openCubeSet (originCube d n))) a Abar

Translate origin-cube elliptic recovery data for the shifted field translateCoeffField z a into existence of the coarse block matrix on the translated open cube.

theorem HCPolySupport.openCubeSet_eq_translateSet_originCube_of_nonneg_scale {d : ℕ} {Q : TriadicCube d} (hQ : 0 ≤ Q.scale) : openCubeSet Q = translateSet (intVecToRealVec (originCubeScaleTranslationShift Q.scale Q)) (openCubeSet (originCube d Q.scale))

A nonnegative-scale triadic open cube is an integer translate of the origin open cube at the same scale.

theorem HCPolySupport.hasQuadraticMu_openCubeSet_of_triadicCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) : HasQuadraticMu (openCubeSet Q) a

Triadic-cube version of hasQuadraticMu_translateSet_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData.

theorem HCPolySupport.exists_coarseBlockMatrix_openCubeSet_of_triadicCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (openCubeSet Q) a Abar

Triadic-cube version of exists_coarseBlockMatrix_translateSet_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData.

theorem HCPolySupport.isCoarseBlockMatrix_of_triadicCube_openRecoveryData {d : ℕ} (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) : IsCoarseBlockMatrix (openCubeSet Q) a (coarseBlockMatrix (openCubeSet Q) a)

Canonical coarse block matrix witness on an arbitrary triadic open cube, packaged from translated origin-cube recovery data.

theorem HCPolySupport.Mu_eq_half_blockVecDot_coarseMatrix_cube_of_triadicCube {d : ℕ} (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) (P : BlockVec d) : Mu (openCubeSet Q) P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) P)

Quadratic formula for Mu on an arbitrary triadic open cube, packaged from translated origin-cube recovery data.

theorem HCPolySupport.hasQuadraticMu_cubeSet_of_triadicCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} [NeZero d] (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) : HasQuadraticMu (cubeSet Q) a

Quadraticity of Mu on an arbitrary triadic half-open cube, transported from the open-cube recovery data across the null boundary.

theorem HCPolySupport.exists_coarseBlockMatrix_cubeSet_of_triadicCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} [NeZero d] (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) : ∃ (Abar : BlockMat d), IsCoarseBlockMatrix (cubeSet Q) a Abar

Coarse block matrix existence on an arbitrary triadic half-open cube, transported from translated origin-cube recovery data.

theorem HCPolySupport.isCoarseBlockMatrix_coarseBlockMatrix_cubeSet_of_triadicCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} [NeZero d] (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) : IsCoarseBlockMatrix (cubeSet Q) a (coarseBlockMatrix (cubeSet Q) a)

Canonical coarse block matrix witness on an arbitrary triadic half-open cube, transported from translated origin-cube recovery data.

theorem HCPolySupport.Mu_eq_half_blockVecPairing_coarseMatrix_of_triadicRecovery {d : ℕ} [NeZero d] (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) (P : BlockVec d) : Mu (cubeSet Q) P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet Q) a) P)

Quadratic formula for Mu on an arbitrary triadic half-open cube, transported from translated origin-cube recovery data.