Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.VectorFieldAndApex.WeakEquationHelpers

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

theorem HCPolySupport.h10WeakEquationOn_of_contDiff_tests {d : ℕ} {U : Set (Vec d)} {G : Vec d → Vec d} {f : Vec d → ℝ} (hU : IsOpen U) (hG : MemVectorL2 U G) (hf : MemScalarL2 U f) (htest : ∀ (ψ : Vec d → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ U → ∫ (x : Vec d) in U, vecDot (G x) (euclideanGradient ψ x) = ∫ (x : Vec d) in U, f x * ψ x) (φ : H10Function U) : ∫ (x : Vec d) in U, vecDot (G x) (φ.grad x) = ∫ (x : Vec d) in U, f x * φ.toFun x

Extend an inhomogeneous weak equation from smooth compactly supported tests to arbitrary H¹₀ tests on an open domain. The proof uses exactly the approximation data bundled in H10Function: the gradient side is continuous by L² × L² → L¹, and the forcing side is the same scalar argument.

theorem HCPolySupport.IsPotentialOn.congr_ae {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfg : f =ᵐ[MeasureTheory.volume.restrict U] g) (hf : IsPotentialOn U f) : IsPotentialOn U g

The H¹-potential predicate is insensitive to changing the vector-field representative a.e. on the domain.

theorem HCPolySupport.eventuallyEq_indicator_cubeFaceReflectionCell_of_mem {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (φ : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) : (openCubeSet (cubeFaceReflectionCellCube Q choice)).indicator φ =ᶠ[nhds x] φ

On a reflection cell, the cell indicator of a function is locally the function itself.

theorem HCPolySupport.eventuallyEq_indicator_cubeFaceReflectionCell_of_notMem {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφ_sub : tsupport φ ⊆ cubeFaceReflectionBlockSet Q) {x : Vec d} (hx : x ∉ openCubeSet (cubeFaceReflectionCellCube Q choice)) : (openCubeSet (cubeFaceReflectionCellCube Q choice)).indicator φ =ᶠ[nhds x] 0

Away from a reflection cell, the cell indicator of a test supported in the reflection block is locally zero. If the base point lies in another cell, this is disjointness of the open cells; if it lies outside the block, it is the support hypothesis.

theorem HCPolySupport.contDiff_indicator_cubeFaceReflectionCell_of_tsupport_subset_block {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_sub : tsupport φ ⊆ cubeFaceReflectionBlockSet Q) : ContDiff ℝ (↑⊤) ((openCubeSet (cubeFaceReflectionCellCube Q choice)).indicator φ)

The zero extension of a smooth compactly supported reflection-block test to one reflection cell remains smooth.

theorem HCPolySupport.hasCompactSupport_indicator_cubeFaceReflectionCell {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφs : HasCompactSupport φ) : HasCompactSupport ((openCubeSet (cubeFaceReflectionCellCube Q choice)).indicator φ)

The cell indicator of a compactly supported test is compactly supported.

theorem HCPolySupport.tsupport_indicator_cubeFaceReflectionCell_subset {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφ_sub : tsupport φ ⊆ cubeFaceReflectionBlockSet Q) : tsupport ((openCubeSet (cubeFaceReflectionCellCube Q choice)).indicator φ) ⊆ openCubeSet (cubeFaceReflectionCellCube Q choice)

If a smooth test is supported in the reflection block, then its cell indicator has topological support inside that cell.