TestPair

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

Local block energy: the centered potentials and the test pair

The centered potentials u = v − ½p·x − c, u* = v* − ½p·x + c as H¹ functions (with constant gradients V = ∇v − ½p, V* = ∇v* − ½p), and the smooth test pair (η²u, η²u*) built from the library's smooth×H¹ product H1Function.mulContDiffMemLpTop. The admissibility MemH10 (η²u + η²u*) is obtained from η²·(v+v*−p·x) ∈ H¹₀ via H10Function.mulContDiffMemLpTop.

The centered potentials

noncomputable def HCPolySupport.centeredPotential {d : ℕ} (m : ℤ) (v : H1Function (openCubeSet (originCube d m))) (p : Vec d) (c : ℝ) : H1Function (openCubeSet (originCube d m))

u = v − ½ p·x − c as an H¹ function.

Equations

• HCPolySupport.centeredPotential m v p c = v + -(1 / 2) • HCPolySupport.affineH1 m p + HCPolySupport.H1Function.const (-c)

@[simp]

theorem HCPolySupport.centeredPotential_toFun {d : ℕ} {m : ℤ} (v : H1Function (openCubeSet (originCube d m))) (p : Vec d) (c : ℝ) (x : Vec d) : (centeredPotential m v p c).toFun x = v.toFun x - 1 / 2 * vecDot p x - c

Evaluation formula for the centered potential.

@[simp]

theorem HCPolySupport.centeredPotential_grad {d : ℕ} {m : ℤ} (v : H1Function (openCubeSet (originCube d m))) (p : Vec d) (c : ℝ) (x : Vec d) : (centeredPotential m v p c).grad x = v.grad x - (1 / 2) • p

Gradient formula for the centered potential.

theorem HCPolySupport.centeredPotential_add_toFun {d : ℕ} {m : ℤ} (v vstar : H1Function (openCubeSet (originCube d m))) (p : Vec d) (c : ℝ) (x : Vec d) : (centeredPotential m v p c).toFun x + (centeredPotential m vstar p (-c)).toFun x = v.toFun x + vstar.toFun x - vecDot p x

The sum of the two centered potentials is v + v* − p·x.

L^∞ data for η²

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

Packaged L^∞ data for η² on the finite-measure cube.

theorem HCPolySupport.sqCutoff_fderiv_memLpTop {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) {Gη : ℝ} (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)) ⊤ (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))

Packaged L∞ data for a partial derivative of η².

The test function η²·u

noncomputable def HCPolySupport.testFun {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) {Gη : ℝ} (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (u : H1Function (openCubeSet (originCube d m))) : H1Function (openCubeSet (originCube d m))

η² · u as an H¹ function via the library's smooth×H¹ product.

Equations

• HCPolySupport.testFun hη hIcc hGη u = u.mulContDiffMemLpTop ⋯ ⋯ ⋯

@[simp]

theorem HCPolySupport.testFun_toFun {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) {Gη : ℝ} (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (u : H1Function (openCubeSet (originCube d m))) (x : Vec d) : (testFun hη hIcc hGη u).toFun x = sqCutoff η x * u.toFun x

Evaluation formula for the cutoff test function.

@[simp]

theorem HCPolySupport.testFun_grad {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) {Gη : ℝ} (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (u : H1Function (openCubeSet (originCube d m))) (x : Vec d) (i : Fin d) : (testFun hη hIcc hGη u).grad x i = sqCutoff η x * u.grad x i + u.toFun x * (fderiv ℝ (sqCutoff η) x) (basisVec i)

Gradient formula for the cutoff test function.

Admissibility of the test pair

theorem HCPolySupport.memH10_testPair_sum {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) {Gη : ℝ} (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) {v vstar : H1Function (openCubeSet (originCube d m))} {p : Vec d} {c : ℝ} (hTrace : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot p x) : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => (testFun hη hIcc hGη (centeredPotential m v p c)).toFun x + (testFun hη hIcc hGη (centeredPotential m vstar p (-c))).toFun x

MemH10 (η² u + η² u*), from η² · (u + u*) ∈ H¹₀ and the library's H10Function smooth product. The input hTrace is the trace fact v + v* − p·x ∈ H¹₀(U).