Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentTestFold

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

Signed folded parent tests

For the parent-cube H¹ gluing step, a parent test is pulled back to the original cube through every reflection cell. In the weak-gradient identity for coordinate i, the cell pullback is weighted by the ith reflection sign. The resulting signed sum is the test whose boundary-face cancellation should feed the face-zero cutoff closure.

def HCPolySupport.cubeFaceReflectionCellFoldSign {d : ℕ} (choice : Fin d → Fin 3) (i : Fin d) : ℝ

The sign contributed by a reflection cell in coordinate i.

Equations

• HCPolySupport.cubeFaceReflectionCellFoldSign choice i = if choice i = 1 then 1 else -1

@[simp]

theorem HCPolySupport.cubeFaceReflectionCellFoldSign_mul_self {d : ℕ} (choice : Fin d → Fin 3) (i : Fin d) : cubeFaceReflectionCellFoldSign choice i * cubeFaceReflectionCellFoldSign choice i = 1

noncomputable def HCPolySupport.cubeFaceReflectionFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) (i : Fin d) (φ : Vec d → ℝ) : Vec d → ℝ

Signed pullback of a parent scalar test to the original cube, for the weak-gradient identity in coordinate i.

Equations

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

def HCPolySupport.cubeFaceReflectionLowerChoiceSwap {d : ℕ} (i : Fin d) (choice : Fin d → Fin 3) : Fin d → Fin 3

Involution on reflection-cell choices pairing the lower neighbor strip with the original strip in coordinate i. The upper strip is fixed.

Equations

• HCPolySupport.cubeFaceReflectionLowerChoiceSwap i choice = Function.update choice i (if choice i = 0 then 1 else if choice i = 1 then 0 else choice i)

def HCPolySupport.cubeFaceReflectionUpperChoiceSwap {d : ℕ} (i : Fin d) (choice : Fin d → Fin 3) : Fin d → Fin 3

Involution on reflection-cell choices pairing the original strip with the upper neighbor strip in coordinate i. The lower strip is fixed.

Equations

• HCPolySupport.cubeFaceReflectionUpperChoiceSwap i choice = Function.update choice i (if choice i = 1 then 2 else if choice i = 2 then 1 else choice i)

@[simp]

theorem HCPolySupport.cubeFaceReflectionLowerChoiceSwap_apply_self {d : ℕ} (i : Fin d) (choice : Fin d → Fin 3) : cubeFaceReflectionLowerChoiceSwap i choice i = if choice i = 0 then 1 else if choice i = 1 then 0 else choice i

@[simp]

theorem HCPolySupport.cubeFaceReflectionUpperChoiceSwap_apply_self {d : ℕ} (i : Fin d) (choice : Fin d → Fin 3) : cubeFaceReflectionUpperChoiceSwap i choice i = if choice i = 1 then 2 else if choice i = 2 then 1 else choice i

@[simp]

theorem HCPolySupport.cubeFaceReflectionLowerChoiceSwap_apply_ne {d : ℕ} {i j : Fin d} (hji : j ≠ i) (choice : Fin d → Fin 3) : cubeFaceReflectionLowerChoiceSwap i choice j = choice j

@[simp]

theorem HCPolySupport.cubeFaceReflectionUpperChoiceSwap_apply_ne {d : ℕ} {i j : Fin d} (hji : j ≠ i) (choice : Fin d → Fin 3) : cubeFaceReflectionUpperChoiceSwap i choice j = choice j

@[simp]

theorem HCPolySupport.cubeFaceReflectionLowerChoiceSwap_involutive {d : ℕ} (i : Fin d) : Function.Involutive (cubeFaceReflectionLowerChoiceSwap i)

@[simp]

theorem HCPolySupport.cubeFaceReflectionUpperChoiceSwap_involutive {d : ℕ} (i : Fin d) : Function.Involutive (cubeFaceReflectionUpperChoiceSwap i)

theorem HCPolySupport.cubeFaceReflectionCellFoldMap_lowerChoiceSwap_lowerFaceProjection {d : ℕ} (Q : TriadicCube d) (i : Fin d) (choice : Fin d → Fin 3) (x : Vec d) : cubeFaceReflectionCellFoldMap Q (cubeFaceReflectionLowerChoiceSwap i choice) (cubeLowerFaceProjection Q i x) = cubeFaceReflectionCellFoldMap Q choice (cubeLowerFaceProjection Q i x)

On the lower i-face, the lower/original paired cell fold maps agree.

theorem HCPolySupport.cubeFaceReflectionCellFoldMap_upperChoiceSwap_upperFaceProjection {d : ℕ} (Q : TriadicCube d) (i : Fin d) (choice : Fin d → Fin 3) (x : Vec d) : cubeFaceReflectionCellFoldMap Q (cubeFaceReflectionUpperChoiceSwap i choice) (cubeUpperFaceProjection Q i x) = cubeFaceReflectionCellFoldMap Q choice (cubeUpperFaceProjection Q i x)

On the upper i-face, the original/upper paired cell fold maps agree.

theorem HCPolySupport.cubeFaceReflectionFoldedParentScalarTest_lowerFaceProjection_eq_zero_of_outer {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (houter : ∀ (choice : Fin d → Fin 3) (x : Vec d), choice i ≠ 0 → choice i ≠ 1 → φ (cubeFaceReflectionCellFoldMap Q choice (cubeLowerFaceProjection Q i x)) = 0) (x : Vec d) : cubeFaceReflectionFoldedParentScalarTest Q i φ (cubeLowerFaceProjection Q i x) = 0

Lower-face cancellation for the signed folded parent test, assuming the unpaired upper-strip outer cell evaluates to zero.

theorem HCPolySupport.cubeFaceReflectionFoldedParentScalarTest_upperFaceProjection_eq_zero_of_outer {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (houter : ∀ (choice : Fin d → Fin 3) (x : Vec d), choice i ≠ 1 → choice i ≠ 2 → φ (cubeFaceReflectionCellFoldMap Q choice (cubeUpperFaceProjection Q i x)) = 0) (x : Vec d) : cubeFaceReflectionFoldedParentScalarTest Q i φ (cubeUpperFaceProjection Q i x) = 0

Upper-face cancellation for the signed folded parent test, assuming the unpaired lower-strip outer cell evaluates to zero.

theorem HCPolySupport.cubeFaceReflectionCellFoldMap_lowerFaceProjection_notMem_openCubeSet_succ_originCube {d : ℕ} (m : ℤ) (i : Fin d) (choice : Fin d → Fin 3) (x : Vec d) (h0 : choice i ≠ 0) (h1 : choice i ≠ 1) : cubeFaceReflectionCellFoldMap (originCube d m) choice (cubeLowerFaceProjection (originCube d m) i x) ∉ openCubeSet (originCube d (m + 1))

On the lower original face, the unpaired upper reflection cell lands on the upper outer face of the parent centered cube.

theorem HCPolySupport.cubeFaceReflectionCellFoldMap_upperFaceProjection_notMem_openCubeSet_succ_originCube {d : ℕ} (m : ℤ) (i : Fin d) (choice : Fin d → Fin 3) (x : Vec d) (h1 : choice i ≠ 1) (h2 : choice i ≠ 2) : cubeFaceReflectionCellFoldMap (originCube d m) choice (cubeUpperFaceProjection (originCube d m) i x) ∉ openCubeSet (originCube d (m + 1))

On the upper original face, the unpaired lower reflection cell lands on the lower outer face of the parent centered cube.

theorem HCPolySupport.cubeFaceReflectionFoldedParentScalarTest_lowerFaceProjection_eq_zero_originCube {d : ℕ} (m : ℤ) (i : Fin d) {φ : Vec d → ℝ} (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) (x : Vec d) : cubeFaceReflectionFoldedParentScalarTest (originCube d m) i φ (cubeLowerFaceProjection (originCube d m) i x) = 0

Origin-cube lower-face cancellation for parent tests supported in the next larger centered cube.

theorem HCPolySupport.cubeFaceReflectionFoldedParentScalarTest_upperFaceProjection_eq_zero_originCube {d : ℕ} (m : ℤ) (i : Fin d) {φ : Vec d → ℝ} (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) (x : Vec d) : cubeFaceReflectionFoldedParentScalarTest (originCube d m) i φ (cubeUpperFaceProjection (originCube d m) i x) = 0

Origin-cube upper-face cancellation for parent tests supported in the next larger centered cube.

theorem HCPolySupport.contDiff_cubeFaceReflectionFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (cubeFaceReflectionFoldedParentScalarTest Q i φ)

The signed folded parent test is smooth when the parent test is smooth.

theorem HCPolySupport.euclideanCoordDeriv_cubeFaceReflectionFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x : Vec d) : euclideanCoordDeriv i (cubeFaceReflectionFoldedParentScalarTest Q i φ) x = ∑ choice : Fin d → Fin 3, euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap Q choice x)

Coordinate derivative of the signed folded parent test. The prefactor sign cancels the chain-rule reflection sign.

theorem HCPolySupport.hasCompactSupport_cubeFaceReflectionFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) : HasCompactSupport (cubeFaceReflectionFoldedParentScalarTest Q i φ)

The signed folded parent test has compact support when the parent test has compact support.