Coarse-graining support: Support.HighContrast.Coupled.WeakForm

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

Coupled representation: weak-form definition and algebraic scaffolding

This module holds the G0 weak-form definition together with the pointwise matrix/vector algebra and Sobolev scaffolding consumed by the G1 existence package in Coupled/Representation.lean.

All coefficients act on Vec d = Fin d → ℝ; no EuclideanSpace. The file is deliberately factored into small named lemmas.

G0 — the weak-form predicate

def HCPolySupport.CoupledWeakForm {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) (q : Vec d) (v vstar : H1Function U) : Prop

G0. The variational-identity component of the coupled boundary problem e.coupled.weak, to be paired with its affine trace condition. For flux data q, the identity requires that every test pair (φ, φ*) of H¹(U) functions whose sum lies in H¹₀(U) satisfy ∫_U ∇φ·(a ∇v) + ∫_U ∇φ*·(aᵗ ∇v*) = ∫_U q·∇φ.

Equations

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

Finite-measure instance on the open cube

theorem HCPolySupport.isFiniteMeasure_openCubeSet_originCube {d : ℕ} (m : ℤ) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (openCubeSet (originCube d m)))

The restricted Lebesgue measure on a centered open triadic cube is finite.

Sums of H¹ functions

theorem HCPolySupport.H1Function.sum_grad {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} (s : Finset ι) (f : ι → H1Function U) : (∑ i ∈ s, f i).grad = fun (x : Vec d) => ∑ i ∈ s, (f i).grad x

theorem HCPolySupport.H1Function.sum_toFun {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} (s : Finset ι) (f : ι → H1Function U) : (∑ i ∈ s, f i).toFun = fun (x : Vec d) => ∑ i ∈ s, (f i).toFun x

The affine coordinate H¹ function x ↦ p·x

noncomputable def HCPolySupport.affineH1 {d : ℕ} (m : ℤ) (p : Vec d) : H1Function (openCubeSet (originCube d m))

The affine map x ↦ p·x as an H¹ function on the centered open cube, with constant gradient p. This is the coordinate construction assembled from the library's coordinate projections coordOnOpenCubeSetOriginCube.

Equations

• HCPolySupport.affineH1 m p = ∑ i : Fin d, p i • HCPolySupport.H1Function.coordOnOpenCubeSetOriginCube i

@[simp]

theorem HCPolySupport.affineH1_grad {d : ℕ} (m : ℤ) (p : Vec d) : (affineH1 m p).grad = fun (x : Vec d) => p

@[simp]

theorem HCPolySupport.affineH1_toFun {d : ℕ} (m : ℤ) (p : Vec d) : (affineH1 m p).toFun = fun (x : Vec d) => vecDot p x

Symmetric/skew decomposition of the transpose action

theorem HCPolySupport.matVecMul_matTranspose_eq {d : ℕ} (A : Mat d) (w : Vec d) : matVecMul (matTranspose A) w = matVecMul (symmPart A) w - matVecMul (skewPart A) w

matVecMul Aᵀ w = matVecMul s w − matVecMul k w where s = symmPart A, k = skewPart A.

theorem HCPolySupport.matVecMul_sub_vec {d : ℕ} (A : Mat d) (x y : Vec d) : matVecMul A (x - y) = matVecMul A x - matVecMul A y

Symmetric-part regrouping of a∇v + aᵀ∇v*: A vg + Aᵀ vsg = s (vg + vsg) + k (vg − vsg).

theorem HCPolySupport.matVecMul_add_matTranspose_eq {d : ℕ} (A : Mat d) (vg vsg : Vec d) : matVecMul A vg + matVecMul (matTranspose A) vsg = matVecMul (symmPart A) (vg + vsg) + matVecMul (skewPart A) (vg - vsg)

theorem HCPolySupport.matVecMul_sub_matTranspose_eq {d : ℕ} (A : Mat d) (vg vsg : Vec d) : matVecMul A vg - matVecMul (matTranspose A) vsg = matVecMul (symmPart A) (vg - vsg) + matVecMul (skewPart A) (vg + vsg)

Symmetric-part regrouping of a∇v − aᵀ∇v*: A vg − Aᵀ vsg = s (vg − vsg) + k (vg + vsg).

The α/β bilinear split of the weak-form integrand

theorem HCPolySupport.vecDot_alpha_beta_split {d : ℕ} (Pv Ps X Y : Vec d) : vecDot Pv X + vecDot Ps Y = vecDot ((1 / 2) • (Pv + Ps)) (X + Y) + vecDot ((1 / 2) • (Pv - Ps)) (X - Y)

Bilinear α/β split: Pv·X + Ps·Y = α·(X+Y) + β·(X−Y) where α = ½(Pv+Ps), β = ½(Pv−Ps).

The symmetric parallelogram identity

theorem HCPolySupport.vecDot_half_parallelogram {d : ℕ} (p τ A B : Vec d) : 2 * vecDot ((1 / 2) • (p + τ)) ((1 / 2) • (A + B)) + 2 * vecDot ((1 / 2) • (p - τ)) ((1 / 2) • (A - B)) = vecDot p A + vecDot τ B

Bilinear parallelogram identity: 2 (½(p+τ))·(½(A+B)) + 2 (½(p−τ))·(½(A−B)) = p·A + τ·B.

theorem HCPolySupport.two_vecDot_symmPart_half_add_sub {d : ℕ} (s : Mat d) (p τ : Vec d) : 2 * vecDot ((1 / 2) • (p + τ)) (matVecMul s ((1 / 2) • (p + τ))) + 2 * vecDot ((1 / 2) • (p - τ)) (matVecMul s ((1 / 2) • (p - τ))) = vecDot p (matVecMul s p) + vecDot τ (matVecMul s τ)

Parallelogram identity for the symmetric form s: 2 (½(p+τ))·s(½(p+τ)) + 2 (½(p−τ))·s(½(p−τ)) = p·s p + τ·s τ.

The pointwise energy identity (A7 + Schur inverse)

theorem HCPolySupport.blockEnergy_pointwise_eq {d : ℕ} {A : Mat d} (hdet : IsUnit (Matrix.det (symmPart A))) (p j : Vec d) : blockVecDot (p, j) (blockMatVecMul (blockMatrixOfCoeff A) (p, j)) = vecDot p (matVecMul (symmPart A) p) + vecDot (matVecMul (symmPart A)⁻¹ (j - matVecMul (skewPart A) p)) (matVecMul (symmPart A) (matVecMul (symmPart A)⁻¹ (j - matVecMul (skewPart A) p)))

The doubled quadratic form of bfA equals p·s p + τ·s τ with τ := s⁻¹(j − k p). This is the A7 factorization with the Schur term rewritten through s s⁻¹ = 1.