Identity

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Local block energy: the test identity

Testing the coupled weak form CoupledWeakForm at the smooth pair (η²u, η²u*) and expanding both sides gives the paper's e.local.block.test.identity:

𝓔 := ∫_U η²(V·sV + V*·sV*) = ∫_U η²(q − ½ap)·V − ½∫_U η²(aᵀp)·V* + ∫_U u(q − a∇v)·∇(η²) − ∫_U u*(aᵀ∇v*)·∇(η²),

where V = ∇v − ½p, V* = ∇v* − ½p, u = v − ½p·x − c, u* = v* − ½p·x + c.

The engine is a single pointwise algebraic identity (pointwise_energy_test_identity) that rewrites the energy density as the sum of the bulk density, the cutoff density and the weak-form defect (a∇v·∇φ + aᵀ∇v*·∇φ*) − q·∇φ; integrating and cancelling the defect via the weak form yields the identity. No EuclideanSpace.

The pointwise test-identity density

theorem HCPolySupport.pointwise_energy_test_identity {d : ℕ} (A : Mat d) (gv gvs p q gS : Vec d) (η2 uu uus : ℝ) : η2 * (vecDot (gv - (1 / 2) • p) (matVecMul (symmPart A) (gv - (1 / 2) • p)) + vecDot (gvs - (1 / 2) • p) (matVecMul (symmPart A) (gvs - (1 / 2) • p))) = η2 * (vecDot (q - (1 / 2) • matVecMul A p) (gv - (1 / 2) • p) - 1 / 2 * vecDot (matVecMul (matTranspose A) p) (gvs - (1 / 2) • p)) + (uu * vecDot (q - matVecMul A gv) gS - uus * vecDot (matVecMul (matTranspose A) gvs) gS) + (vecDot (η2 • (gv - (1 / 2) • p) + uu • gS) (matVecMul A gv) + vecDot (η2 • (gvs - (1 / 2) • p) + uus • gS) (matVecMul (matTranspose A) gvs) - vecDot q (η2 • (gv - (1 / 2) • p) + uu • gS))

Pointwise algebraic identity underlying e.local.block.test.identity. With V = gv − ½p, V* = gvs − ½p the energy density equals the bulk density plus the cutoff density plus the weak-form defect.

noncomputable def HCPolySupport.energyIntegrand {d : ℕ} {m : ℤ} (a : CoeffField d) (v vstar : H1Function (openCubeSet (originCube d m))) (P : BlockVec d) (η : Vec d → ℝ) : Vec d → ℝ

The energy density η²(V·sV + V*·sV*) with V = ∇v − ½p, s = symmPart a.

Equations

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

noncomputable def HCPolySupport.bulkIntegrand {d : ℕ} {m : ℤ} (a : CoeffField d) (v vstar : H1Function (openCubeSet (originCube d m))) (P : BlockVec d) (η : Vec d → ℝ) : Vec d → ℝ

The bulk density η²((q − ½ap)·V − ½(aᵀp)·V*).

Equations

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

noncomputable def HCPolySupport.cutoffIntegrand {d : ℕ} {m : ℤ} (a : CoeffField d) (v vstar : H1Function (openCubeSet (originCube d m))) (P : BlockVec d) (c : ℝ) (η : Vec d → ℝ) : Vec d → ℝ

The cutoff density u(q − a∇v)·∇(η²) − u*(aᵀ∇v*)·∇(η²).

Equations

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

Integrability of the four densities

theorem HCPolySupport.memLpTop_sqCutoff_cube {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) : MeasureTheory.MemLp (sqCutoff η) ⊤ (volumeMeasureOn (openCubeSet (originCube d m)))

L∞ control of η².

theorem HCPolySupport.memLpTop_fderiv_sqCutoff_cube {d : ℕ} {m : ℤ} {η : Vec d → ℝ} {Gη : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ (sqCutoff η) x) (basisVec i)) ⊤ (volumeMeasureOn (openCubeSet (originCube d m)))

L∞ control of ∂ᵢ(η²).

theorem HCPolySupport.memVectorL2_centeredGrad {d : ℕ} {m : ℤ} (v : H1Function (openCubeSet (originCube d m))) (P : BlockVec d) : MemVectorL2 (openCubeSet (originCube d m)) fun (x : Vec d) => v.grad x - (1 / 2) • P.1

V = ∇v − ½p ∈ L².

theorem HCPolySupport.integrableOn_energyIntegrand {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) : MeasureTheory.IntegrableOn (energyIntegrand a v vstar P η) (openCubeSet (originCube d m)) MeasureTheory.volume

theorem HCPolySupport.integrableOn_bulkIntegrand {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) : MeasureTheory.IntegrableOn (bulkIntegrand a v vstar P η) (openCubeSet (originCube d m)) MeasureTheory.volume

theorem HCPolySupport.integrableOn_cutoffIntegrand {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {Gη : ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (c : ℝ) : MeasureTheory.IntegrableOn (cutoffIntegrand a v vstar P c η) (openCubeSet (originCube d m)) MeasureTheory.volume

The integral test identity

theorem HCPolySupport.energyIntegral_eq_bulk_add_cutoff {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {Gη c : ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (hWeak : CoupledWeakForm a (openCubeSet (originCube d m)) P.2 v vstar) (hTrace : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot P.1 x) : ∫ (x : Vec d) in openCubeSet (originCube d m), energyIntegrand a v vstar P η x = (∫ (x : Vec d) in openCubeSet (originCube d m), bulkIntegrand a v vstar P η x) + ∫ (x : Vec d) in openCubeSet (originCube d m), cutoffIntegrand a v vstar P c η x

The test identity. With the weak form and the η²·u test pair, the energy integral equals the bulk integral plus the cutoff integral.