Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.ResponseIdentities.Homogeneity

Coarse-graining support: Support.CoarseGraining.ResponseIdentities.Homogeneity #

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

Homogeneity statements for deterministic coarse scalar objects.

source
theorem HCPolySupport.isSigmaStarInvCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) {lam : ℝ} (hlam : 0 < lam) :
IsSigmaStarInvCoarse U (lam • a) (lam⁻¹ • sigmaStar⁻¹)
source
theorem HCPolySupport.sigmaStarInvCoarse_homogeneous_coeffField_of_isSigmaStarCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) {lam : ℝ} (hlam : 0 < lam) :
sigmaStarInvCoarse U (lam • a) = lam⁻¹ • sigmaStarInvCoarse U a
source
theorem HCPolySupport.sigmaStarInvCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) {lam : ℝ} (hlam : 0 < lam) :
sigmaStarInvCoarse U (lam • a) = lam⁻¹ • sigmaStarInvCoarse U a

Note-facing homogeneity for \sigma_*^{-1}(U; a) under coefficient rescaling.

source
theorem HCPolySupport.isSigmaStarInvKappaCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hK : IsKappaCoarse U a sigmaStar kappa) {lam : ℝ} (hlam : 0 < lam) :
IsSigmaStarInvKappaCoarse U (lam • a) (sigmaStar⁻¹ * kappa)
source
theorem HCPolySupport.sigmaStarInvKappaCoarse_homogeneous_coeffField_of_isKappaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hK : IsKappaCoarse U a sigmaStar kappa) {lam : ℝ} (hlam : 0 < lam) :
sigmaStarInvKappaCoarse U (lam • a) = sigmaStarInvKappaCoarse U a
source
theorem HCPolySupport.sigmaStarInvKappaCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hK : IsKappaCoarse U a sigmaStar kappa) {lam : ℝ} (hlam : 0 < lam) :
sigmaStarInvKappaCoarse U (lam • a) = sigmaStarInvKappaCoarse U a

Note-facing homogeneity for \sigma_*^{-1}(U; a)\kappa(U; a) under coefficient rescaling.

source
theorem HCPolySupport.isSigmaStarCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
IsSigmaStarCoarse U (lam • a) (lam • sigmaStar)
source
theorem HCPolySupport.sigmaStarCoarse_homogeneous_coeffField_of_isSigmaStarCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
sigmaStarCoarse U (lam • a) = lam • sigmaStarCoarse U a
source
theorem HCPolySupport.sigmaStarCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
sigmaStarCoarse U (lam • a) = lam • sigmaStarCoarse U a

Note-facing homogeneity for \sigma_*(U; a) under coefficient rescaling.

source
theorem HCPolySupport.isKappaCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
IsKappaCoarse U (lam • a) (lam • sigmaStar) (lam • kappa)
source
theorem HCPolySupport.kappaCoarse_homogeneous_coeffField_of_isKappaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
kappaCoarse U (lam • a) = lam • kappaCoarse U a
source
theorem HCPolySupport.kappaCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
kappaCoarse U (lam • a) = lam • kappaCoarse U a

Note-facing homogeneity for \kappa(U; a) under coefficient rescaling.

source
theorem HCPolySupport.isSigmaCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
IsSigmaCoarse U (lam • a) (lam • sigma) (lam • sigmaStar) (lam • kappa)
source
theorem HCPolySupport.sigmaCoarse_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
sigmaCoarse U (lam • a) = lam • sigmaCoarse U a
source
theorem HCPolySupport.sigmaCoarse_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
sigmaCoarse U (lam • a) = lam • sigmaCoarse U a

Note-facing homogeneity for \sigma(U; a) under coefficient rescaling.

source
theorem HCPolySupport.cg_matrices_homogeneous_coeffField {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
sigmaCoarse U (lam • a) = lam • sigmaCoarse U a ∧ sigmaStarCoarse U (lam • a) = lam • sigmaStarCoarse U a ∧ kappaCoarse U (lam • a) = lam • kappaCoarse U a

Bundled note-facing homogeneity for the deterministic coarse matrices σ(U; a), σ_*(U; a), and κ(U; a) under coefficient rescaling.

source
theorem HCPolySupport.deterministicCoarseBlockMatrix_upperLeft_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicCoarseBlockMatrix U (lam • a)).upperLeft = lam • (deterministicCoarseBlockMatrix U a).upperLeft
source
theorem HCPolySupport.deterministicCoarseBlockMatrix_upperRight_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicCoarseBlockMatrix U (lam • a)).upperRight = (deterministicCoarseBlockMatrix U a).upperRight
source
theorem HCPolySupport.deterministicCoarseBlockMatrix_lowerLeft_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicCoarseBlockMatrix U (lam • a)).lowerLeft = (deterministicCoarseBlockMatrix U a).lowerLeft
source
theorem HCPolySupport.deterministicCoarseBlockMatrix_lowerRight_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicCoarseBlockMatrix U (lam • a)).lowerRight = lam⁻¹ • (deterministicCoarseBlockMatrix U a).lowerRight
source
theorem HCPolySupport.deterministicStarredBlockMatrixInv_upperLeft_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicStarredBlockMatrixInv U (lam • a)).upperLeft = lam⁻¹ • (deterministicStarredBlockMatrixInv U a).upperLeft
source
theorem HCPolySupport.deterministicStarredBlockMatrixInv_upperRight_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicStarredBlockMatrixInv U (lam • a)).upperRight = (deterministicStarredBlockMatrixInv U a).upperRight
source
theorem HCPolySupport.deterministicStarredBlockMatrixInv_lowerLeft_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicStarredBlockMatrixInv U (lam • a)).lowerLeft = (deterministicStarredBlockMatrixInv U a).lowerLeft
source
theorem HCPolySupport.deterministicStarredBlockMatrixInv_lowerRight_homogeneous_coeffField_of_isSigmaCoarse {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) {sigma sigmaStar kappa : Mat d} (hS : IsSigmaStarCoarse U a sigmaStar) (hK : IsKappaCoarse U a sigmaStar kappa) (hSigma : IsSigmaCoarse U a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) {lam : ℝ} (hlam : 0 < lam) :
(deterministicStarredBlockMatrixInv U (lam • a)).lowerRight = lam • (deterministicStarredBlockMatrixInv U a).lowerRight