Coarse-graining support: Support.CoarseGraining.BlockResponse.Foundations.BasicIdentities

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

BlockResponse Foundations -- basic deterministic identities

blockResponse_zero membership in responseSpace, isEllipticFieldOn for adjointCoeffField, blockMatVecMul_blockCoeffField_pair identities, symmPart algebra and pointwiseBlockEnergy_pair_eq_symmPart_sum plus the lowerImage / upperImage orthogonality and responseSpace_smul lemmas.

theorem HCPolySupport.blockResponse_zero_mem_responseSpace {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) : BlockResponseSpace a U { potential := 0, flux := 0 }

theorem HCPolySupport.isEllipticFieldOn_adjointCoeffField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : IsEllipticFieldOn lam Lam U (adjointCoeffField a)

theorem HCPolySupport.blockMatVecMul_blockCoeffField_pair_of_isUnit_det_symmPart {d : ℕ} (a : CoeffField d) (x : Vec d) (hdet : IsUnit (Matrix.det (symmPart (a x)))) (ξ η : Vec d) : blockMatVecMul (blockCoeffField a x) (ξ + η, matVecMul (a x) ξ - matVecMul (matTranspose (a x)) η) = (matVecMul (a x) ξ + matVecMul (matTranspose (a x)) η, ξ - η)

theorem HCPolySupport.blockMatVecMul_blockCoeffField_pair_of_isEllipticFieldOn {d : ℕ} (a : CoeffField d) {lam Lam : ℝ} {U : Set (Vec d)} (hEll : IsEllipticFieldOn lam Lam U a) {x : Vec d} (hx : x ∈ U) (ξ η : Vec d) : blockMatVecMul (blockCoeffField a x) (ξ + η, matVecMul (a x) ξ - matVecMul (matTranspose (a x)) η) = (matVecMul (a x) ξ + matVecMul (matTranspose (a x)) η, ξ - η)

noncomputable def HCPolySupport.pointwiseScalarResponseIntegrand {d : ℕ} (A : Mat d) (p q ξ : Vec d) : ℝ

The scalar response density -ξ · symmPart(A) ξ / 2 - p · Aξ + q · ξ.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.vecDot_matVecMul_self_eq_symmPart {d : ℕ} (A : Mat d) (ξ : Vec d) : vecDot ξ (matVecMul A ξ) = vecDot ξ (matVecMul (symmPart A) ξ)

theorem HCPolySupport.pointwiseBlockEnergy_pair_eq_symmPart_sum_of_isUnit_det_symmPart {d : ℕ} (A : Mat d) (hdet : IsUnit (Matrix.det (symmPart A))) (ξ η : Vec d) : 1 / 2 * blockVecDot (ξ + η, matVecMul A ξ - matVecMul (matTranspose A) η) (blockMatVecMul (blockMatrixOfCoeff A) (ξ + η, matVecMul A ξ - matVecMul (matTranspose A) η)) = vecDot ξ (matVecMul (symmPart A) ξ) + vecDot η (matVecMul (symmPart A) η)

theorem HCPolySupport.blockResponse_mem_responseSpace_smul {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} (hX : BlockResponseSpace a U X) (c : ℝ) : BlockResponseSpace a U (c • X)

theorem HCPolySupport.blockResponse_upperImage_orthogonal_of_mem_responseSpace {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} (hX : BlockResponseSpace a U X) {Y : Vec d → Vec d} (hY : IsPotentialZeroTraceOn U Y) : ∫ (x : Vec d) in U, vecDot (Y x) (blockMatVecMul (blockCoeffField a x) (X.eval x)).1 = 0

theorem HCPolySupport.blockResponse_lowerImage_orthogonal_of_mem_responseSpace {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} (hX : BlockResponseSpace a U X) {Y : Vec d → Vec d} (hY : IsSolenoidalZeroNormalTraceOn U Y) : ∫ (x : Vec d) in U, vecDot (Y x) (blockMatVecMul (blockCoeffField a x) (X.eval x)).2 = 0

structure HCPolySupport.BlockJIntegrabilityData {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) (P Q : BlockVec d) : Prop

Integrability on U of the block response integrand for every state in the response space.

• response (X : BlockState d) : BlockResponseSpace a U X → MeasureTheory.IntegrableOn (blockResponseIntegrand a P Q X) U MeasureTheory.volume

structure HCPolySupport.BlockResponseLowerImageMemVectorL2Data {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Prop

L² membership on U of the lower component of the block coefficient image of every response state.

• lowerImage_memVectorL2 (X : BlockState d) : BlockResponseSpace a U X → MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2

theorem HCPolySupport.blockResponse_potential_memL2_of_mem_responseSpace {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} (hX : BlockResponseSpace a U X) : MemVectorL2 U X.potential

theorem HCPolySupport.blockResponse_upperImage_isSolenoidalOn_of_mem_responseSpace {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} (hX : BlockResponseSpace a U X) : IsSolenoidalOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).1

theorem HCPolySupport.blockResponse_lowerImage_potential_of_hodgeConverse {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} (hHodge : HodgeConverseCriterion U) (hX : BlockResponseSpace a U X) (hLowerL2 : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2

theorem HCPolySupport.blockResponse_lowerImage_isPotential_of_mem_responseSpace_of_memVectorL2 {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] [HasHodgeConverse U] (hX : BlockResponseSpace a U X) (hLowerL2 : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2

theorem HCPolySupport.blockResponse_lowerImage_isPotential_of_memVectorL2_of_convexDomain {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hConv : IsOpenBoundedConvexDomain U) (hX : BlockResponseSpace a U X) (hLowerL2 : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2

Preferred convex-domain wrapper for promoting the lower image of a response state to a potential field. This is the Chapter-2-facing surface to use when the domain is a bounded open convex set.

theorem HCPolySupport.blockResponse_memBlockL2_of_mem_responseSpace_of_integrabilityData {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {X : BlockState d} (hX : BlockResponseSpace a U X) (hInt : BlockResponseIntegrabilityData U a X) : MemBlockL2 U X.eval