Coarse-graining support: Support.CoarseGraining.Translation

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

def HCPolySupport.BlockState.translate {d : ℕ} (X : BlockState d) (z : Vec d) : BlockState d

Translate a block state by precomposing both components with x ↦ x - z.

Equations

• X.translate z = { potential := fun (x : HCPolySupport.Vec d) => X.potential (x - z), flux := fun (x : HCPolySupport.Vec d) => X.flux (x - z) }

@[simp]

theorem HCPolySupport.BlockState.potential_translate {d : ℕ} (X : BlockState d) (z x : Vec d) : (X.translate z).potential x = X.potential (x - z)

@[simp]

theorem HCPolySupport.BlockState.flux_translate {d : ℕ} (X : BlockState d) (z x : Vec d) : (X.translate z).flux x = X.flux (x - z)

@[simp]

theorem HCPolySupport.BlockState.eval_translate {d : ℕ} (X : BlockState d) (z x : Vec d) : (X.translate z).eval x = X.eval (x - z)

theorem HCPolySupport.isBlockMuAdmissible_translateSet {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) (z : Vec d) : IsBlockMuAdmissible (translateSet z U) P (X.translate z)

theorem HCPolySupport.blockEnergyDensity_translate_forward {d : ℕ} (a : CoeffField d) (X : BlockState d) (z x : Vec d) : blockEnergyDensity a (X.translate z) (x + z) = blockEnergyDensity (translateCoeffField z a) X x

theorem HCPolySupport.blockEnergyDensity_translate_backward {d : ℕ} (a : CoeffField d) (X : BlockState d) (z x : Vec d) : blockEnergyDensity (translateCoeffField z a) (X.translate (-z)) x = blockEnergyDensity a X (x + z)

theorem HCPolySupport.volumeAverage_blockEnergyDensity_translate_forward {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (X : BlockState d) : volumeAverage (translateSet z U) (blockEnergyDensity a (X.translate z)) = volumeAverage U (blockEnergyDensity (translateCoeffField z a) X)

theorem HCPolySupport.volumeAverage_blockEnergyDensity_translate_backward {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (X : BlockState d) : volumeAverage U (blockEnergyDensity (translateCoeffField z a) (X.translate (-z))) = volumeAverage (translateSet z U) (blockEnergyDensity a X)

theorem HCPolySupport.muValueSet_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : muValueSet (translateSet z U) P a = muValueSet U P (translateCoeffField z a)

theorem HCPolySupport.Mu_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : Mu (translateSet z U) P a = Mu U P (translateCoeffField z a)

theorem HCPolySupport.coarseBlockMatrix_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : coarseBlockMatrix (translateSet z U) a = coarseBlockMatrix U (translateCoeffField z a)

theorem HCPolySupport.isCoarseBlockMatrix_translateSet_iff {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (Abar : BlockMat d) : IsCoarseBlockMatrix (translateSet z U) a Abar ↔ IsCoarseBlockMatrix U (translateCoeffField z a) Abar

theorem HCPolySupport.hasQuadraticMu_translateSet_iff {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : HasQuadraticMu (translateSet z U) a ↔ HasQuadraticMu U (translateCoeffField z a)

theorem HCPolySupport.isBlockPotentialOn_translateSet {d : ℕ} {U : Set (Vec d)} {X : BlockState d} (hX : IsBlockPotentialOn U X) (z : Vec d) : IsBlockPotentialOn (translateSet z U) (X.translate z)

theorem HCPolySupport.isBlockSolenoidalOn_translateSet {d : ℕ} {U : Set (Vec d)} {X : BlockState d} (hX : IsBlockSolenoidalOn U X) (z : Vec d) : IsBlockSolenoidalOn (translateSet z U) (X.translate z)

theorem HCPolySupport.isBlockTestOn_translateSet {d : ℕ} {U : Set (Vec d)} {X : BlockState d} (hX : IsBlockTestOn U X) (z : Vec d) : IsBlockTestOn (translateSet z U) (X.translate z)

theorem HCPolySupport.blockResponseIntegrand_translate_forward {d : ℕ} (a : CoeffField d) (P Q : BlockVec d) (X : BlockState d) (z x : Vec d) : blockResponseIntegrand a P Q (X.translate z) (x + z) = blockResponseIntegrand (translateCoeffField z a) P Q X x

theorem HCPolySupport.volumeAverage_blockResponseIntegrand_translate_forward {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (P Q : BlockVec d) (X : BlockState d) : volumeAverage (translateSet z U) (blockResponseIntegrand a P Q (X.translate z)) = volumeAverage U (blockResponseIntegrand (translateCoeffField z a) P Q X)

theorem HCPolySupport.blockResponseSpace_translateSet {d : ℕ} (z : Vec d) {U : Set (Vec d)} {a : CoeffField d} {X : BlockState d} (hX : BlockResponseSpace (translateCoeffField z a) U X) : BlockResponseSpace a (translateSet z U) (X.translate z)

theorem HCPolySupport.blockResponseIntegrabilityData_translateSet {d : ℕ} (z : Vec d) {U : Set (Vec d)} {a : CoeffField d} {X : BlockState d} (hX : BlockResponseIntegrabilityData U (translateCoeffField z a) X) : BlockResponseIntegrabilityData (translateSet z U) a (X.translate z)

theorem HCPolySupport.blockJValueSet_subset_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) (P Q : BlockVec d) (a : CoeffField d) : blockJValueSet U P Q (translateCoeffField z a) ⊆ blockJValueSet (translateSet z U) P Q a

theorem HCPolySupport.blockJValueSet_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) (P Q : BlockVec d) (a : CoeffField d) : blockJValueSet (translateSet z U) P Q a = blockJValueSet U P Q (translateCoeffField z a)

theorem HCPolySupport.BlockJ_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (P Q : BlockVec d) (a : CoeffField d) : BlockJ (translateSet z U) P Q a = BlockJ U P Q (translateCoeffField z a)

theorem HCPolySupport.scalarResponseIntegrand_translate_forward {d : ℕ} (a : CoeffField d) (p q : Vec d) {U : Set (Vec d)} (z : Vec d) (u : AHarmonicFunction (translateCoeffField z a) U) (x : Vec d) : scalarResponseIntegrand (translateSet z U) a p q (AHarmonicFunction.translate z u) (x + z) = scalarResponseIntegrand U (translateCoeffField z a) p q u x

theorem HCPolySupport.volumeAverage_scalarResponseIntegrand_translate_forward {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (p q : Vec d) (u : AHarmonicFunction (translateCoeffField z a) U) : volumeAverage (translateSet z U) (scalarResponseIntegrand (translateSet z U) a p q (AHarmonicFunction.translate z u)) = volumeAverage U (scalarResponseIntegrand U (translateCoeffField z a) p q u)

theorem HCPolySupport.responseJValueSet_subset_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : responseJValueSet U p q (translateCoeffField z a) ⊆ responseJValueSet (translateSet z U) p q a

theorem HCPolySupport.responseJValueSet_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : responseJValueSet (translateSet z U) p q a = responseJValueSet U p q (translateCoeffField z a)

theorem HCPolySupport.ResponseJ_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (p q : Vec d) (a : CoeffField d) : ResponseJ (translateSet z U) p q a = ResponseJ U p q (translateCoeffField z a)

theorem HCPolySupport.sigmaStarInvCoarse_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : sigmaStarInvCoarse (translateSet z U) a = sigmaStarInvCoarse U (translateCoeffField z a)

theorem HCPolySupport.sigmaStarCoarse_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : sigmaStarCoarse (translateSet z U) a = sigmaStarCoarse U (translateCoeffField z a)

theorem HCPolySupport.sigmaStarInvKappaCoarse_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : sigmaStarInvKappaCoarse (translateSet z U) a = sigmaStarInvKappaCoarse U (translateCoeffField z a)

theorem HCPolySupport.kappaCoarse_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : kappaCoarse (translateSet z U) a = kappaCoarse U (translateCoeffField z a)

theorem HCPolySupport.sigmaCorrectedResponse_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (p : Vec d) : sigmaCorrectedResponse (translateSet z U) a p = sigmaCorrectedResponse U (translateCoeffField z a) p

theorem HCPolySupport.sigmaCoarse_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : sigmaCoarse (translateSet z U) a = sigmaCoarse U (translateCoeffField z a)

theorem HCPolySupport.bCoarse_translateSet_eq_translateCoeffField {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : bCoarse (sigmaCoarse (translateSet z U) a) (sigmaStarCoarse (translateSet z U) a) (kappaCoarse (translateSet z U) a) = bCoarse (sigmaCoarse U (translateCoeffField z a)) (sigmaStarCoarse U (translateCoeffField z a)) (kappaCoarse U (translateCoeffField z a))

theorem HCPolySupport.isSigmaStarCoarse_translateSet_iff {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (sigmaStar : Mat d) : IsSigmaStarCoarse (translateSet z U) a sigmaStar ↔ IsSigmaStarCoarse U (translateCoeffField z a) sigmaStar

theorem HCPolySupport.isKappaCoarse_translateSet_iff {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (sigmaStar kappa : Mat d) : IsKappaCoarse (translateSet z U) a sigmaStar kappa ↔ IsKappaCoarse U (translateCoeffField z a) sigmaStar kappa

theorem HCPolySupport.isSigmaCoarse_translateSet_iff {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) (sigma sigmaStar kappa : Mat d) : IsSigmaCoarse (translateSet z U) a sigma sigmaStar kappa ↔ IsSigmaCoarse U (translateCoeffField z a) sigma sigmaStar kappa

theorem HCPolySupport.responseJ_blockQuadratic_translateSet_iff {d : ℕ} (z : Vec d) (U : Set (Vec d)) (a : CoeffField d) : (∀ (p q : Vec d), ResponseJ (translateSet z U) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (translateSet z U) a) (-p, q)) - vecDot p q) ↔ ∀ (p q : Vec d), ResponseJ U p q (translateCoeffField z a) = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix U (translateCoeffField z a)) (-p, q)) - vecDot p q