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

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

BlockResponse Foundations -- pair and pair-half state witnesses

blockResponsePairState and blockResponsePairHalfState definitions plus their mem_responseSpace / lowerImage_ae_eq / integrability data theorems under IsEllipticFieldOn.

def HCPolySupport.blockResponsePairState {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : BlockState d

The doubled state (∇u + ∇v, a∇u - aᵀ∇v) formed from primal and adjoint harmonic functions.

Equations

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

noncomputable def HCPolySupport.blockResponsePairHalfState {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : BlockState d

Half the doubled state formed from the sum of primal and adjoint gradients and the difference of their fluxes.

Equations

• HCPolySupport.blockResponsePairHalfState a u v = (1 / 2) • HCPolySupport.blockResponsePairState a u v

theorem HCPolySupport.blockResponse_pair_mem_responseSpace_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : BlockResponseSpace a U { potential := fun (x : Vec d) => u.toH1.grad x + v.toH1.grad x, flux := fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul (matTranspose (a x)) (v.toH1.grad x) }

theorem HCPolySupport.blockResponse_pair_half_mem_responseSpace_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : BlockResponseSpace a U ((1 / 2) • { potential := fun (x : Vec d) => u.toH1.grad x + v.toH1.grad x, flux := fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul (matTranspose (a x)) (v.toH1.grad x) })

theorem HCPolySupport.blockResponse_lowerImage_pair_half_ae_eq_gradDiff_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : (fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) ((blockResponsePairHalfState a u v).eval x)).2) =ᵐ[volumeMeasureOn U] fun (x : Vec d) => (1 / 2) • (u.toH1.grad x - v.toH1.grad x)

theorem HCPolySupport.blockResponseIntegrabilityData_pair_half_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : BlockResponseIntegrabilityData U a (blockResponsePairHalfState a u v)