Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.OriginCubeEllipticRecovery.DeterministicCoarseData

Coarse-graining support: Support.CoarseGraining.OriginCubeEllipticRecovery.DeterministicCoarseData #

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

Origin-cube elliptic recovery -- deterministic coarse data output #

Adjoint-free sigma_* <= sigma and sigma <= b orderings on the centered open cube, the packaged openCubeDeterministicCoarseData_of_triadicCube and its descendant-family variant. These are the outputs consumed by the Chapter-3 coarse Poincare wrappers.

source
theorem HCPolySupport.sigmaStarCoarse_le_sigmaCoarse_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa) (p : Vec d) :
vecDot p (matVecMul (sigmaStarCoarse (openCubeSet (originCube d n)) a) p) ≤ vecDot p (matVecMul (sigmaCoarse (openCubeSet (originCube d n)) a) p)

Adjoint-free deterministic ordering σ_*(U; a) ≤ σ(U; a) on the centered open cube, packaged directly from deterministic recovery-plus-ellipticity data.

source
theorem HCPolySupport.sigmaCoarse_le_bCoarse_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa) :
MatLoewnerLE (sigmaCoarse (openCubeSet (originCube d n)) a) (bCoarse (sigmaCoarse (openCubeSet (originCube d n)) a) (sigmaStarCoarse (openCubeSet (originCube d n)) a) (kappaCoarse (openCubeSet (originCube d n)) a))

Deterministic ordering σ(U; a) ≤ b(U; a) on the centered open cube, packaged directly from deterministic recovery-plus-ellipticity data.

source
theorem HCPolySupport.bCoarse_le_averaged_symmPart_plus_correction_cube {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa) (p : Vec d) :
vecDot p (matVecMul (bCoarse (sigmaCoarse (openCubeSet (originCube d n)) a) (sigmaStarCoarse (openCubeSet (originCube d n)) a) (kappaCoarse (openCubeSet (originCube d n)) a)) p) ≤ volumeAverage (openCubeSet (originCube d n)) fun (x : Vec d) => vecDot p (matVecMul (symmPart (a x) + matTranspose (skewPart (a x)) * (symmPart (a x))⁻¹ * skewPart (a x)) p)

Deterministic upper bound b(U; a) ≤ average(symmPart(a) + k(a)ᵀ symmPart(a)⁻¹ k(a)) on the centered open cube, packaged directly from deterministic recovery-plus-ellipticity data.

source
theorem HCPolySupport.bCoarse_le_symmetricAverage_plusCorrection_of_recovery {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet (originCube d n)) a (deterministicCoarseBlockMatrix (openCubeSet (originCube d n)) a)) (hS : IsSigmaStarCoarse (openCubeSet (originCube d n)) a sigmaStar) (hK : IsKappaCoarse (openCubeSet (originCube d n)) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet (originCube d n)) a sigma sigmaStar kappa) :
MatLoewnerLE (bCoarse (sigmaCoarse (openCubeSet (originCube d n)) a) (sigmaStarCoarse (openCubeSet (originCube d n)) a) (kappaCoarse (openCubeSet (originCube d n)) a)) (averagedSymmPartPlusCorrection (openCubeSet (originCube d n)) a)

Deterministic upper-left matrix-order bound b(U; a) ≤ average(symmPart(a) + k(a)ᵀ symmPart(a)⁻¹ k(a)) on the centered open cube, packaged directly from deterministic recovery-plus-ellipticity data.

source
theorem HCPolySupport.sigmaStarInvCoarse_le_averaged_symmPart_inv_cube {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) (q : Vec d) :
vecDot q (matVecMul (sigmaStarInvCoarse (openCubeSet (originCube d n)) a) q) ≤ volumeAverage (openCubeSet (originCube d n)) fun (x : Vec d) => vecDot q (matVecMul (symmPart (a x))⁻¹ q)

Deterministic inverse-side harmonic-mean upper bound σ_*^{-1}(U; a) ≤ average(symmPart(a)⁻¹) on the centered open cube, packaged directly from deterministic recovery-plus-ellipticity data.

source
theorem HCPolySupport.sigmaStarInvCoarse_le_symmetricAverageInverse_of_recovery {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) :
MatLoewnerLE (sigmaStarInvCoarse (openCubeSet (originCube d n)) a) (averagedSymmPartInv (openCubeSet (originCube d n)) a)

Deterministic inverse-side harmonic-mean matrix bound σ_*^{-1}(U; a) ≤ average(symmPart(a)^{-1}) on the centered open cube, packaged directly from deterministic recovery-plus-ellipticity data.

source
theorem HCPolySupport.harmonicMeanSymmPart_le_sigmaStarCoarse_openCubeSet_originCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} {n : ℤ} (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))) {lam Lam : ℝ} {a : CoeffField d} (hData : HasOpenCubeEllipticRecoveryData n R a) :
MatLoewnerLE (averagedSymmPartInv (openCubeSet (originCube d n)) a)⁻¹ (sigmaStarCoarse (openCubeSet (originCube d n)) a)

Deterministic harmonic-mean lower bound (average(symmPart(a)^{-1}))^{-1} ≤ σ_*(U; a) on the centered open cube, packaged directly from deterministic recovery-plus-ellipticity data.

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

Minimal one-cube deterministic coarse-data constructor from translated origin-cube recovery data.

This is the exact upstream theorem needed to start removing the remaining OpenCubeDescendantDeterministicCoarseData burden from the note-facing Chapter 3 coarse Poincare wrappers.

source
theorem HCPolySupport.kappaCoarse_eq_zero_cube_of_triadicCube_of_hasOpenCubeEllipticRecoveryData {d : ℕ} (Q : TriadicCube d) (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d Q.scale))) {lam Lam : ℝ} {a : CoeffField d} (hRec : HasOpenCubeEllipticRecoveryData Q.scale R (translateCoeffField (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) a)) (hAdj : adjointCoeffField a = a) :
kappaCoarse (openCubeSet Q) a = 0

If the coefficient field is self-adjoint, then the canonical coarse \kappa(openCubeSet Q; a) vanishes on any triadic open cube once translated origin-cube elliptic recovery data is available.

source
theorem HCPolySupport.openCubeDescendantDeterministicCoarseData_of_recoveryFamily {d : ℕ} {Q : TriadicCube d} {a : CoeffField d} {lam Lam : ℝ} (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) :
OpenCubeDescendantDeterministicCoarseData Q a

Descendant deterministic coarse data from a descendant family of translated origin-cube recovery witnesses.

This is the packaged upstream theorem that would directly discharge the last honest Chapter-2 burden still visible in the top harmonic Chapter-3 coarse-Poincare wrappers.