Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.ReflectionWeakEquation

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

Folded tests for the Dirichlet odd-reflection weak equation

The full reflected weak equation is reduced to the original Dirichlet weak problem by folding a parent test back to the original cube with the product odd-reflection sign. This file packages the folded test as an H¹₀ test on origin cubes.

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

Fold a parent scalar test back to the original cube using the product Dirichlet odd-reflection sign.

Equations

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

theorem HCPolySupport.cubeDirichletOddReflectionFoldedParentScalarTest_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) : cubeDirichletOddReflectionFoldedParentScalarTest Q φ (cubeLowerFaceProjection Q i x) = 0

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

theorem HCPolySupport.cubeDirichletOddReflectionFoldedParentScalarTest_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) : cubeDirichletOddReflectionFoldedParentScalarTest Q φ (cubeUpperFaceProjection Q i x) = 0

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

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

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

theorem HCPolySupport.cubeDirichletOddReflectionFoldedParentScalarTest_upperFaceProjection_eq_zero_originCube {d : ℕ} (m : ℤ) (i : Fin d) {φ : Vec d → ℝ} (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) (x : Vec d) : cubeDirichletOddReflectionFoldedParentScalarTest (originCube d m) φ (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_cubeDirichletOddReflectionFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (cubeDirichletOddReflectionFoldedParentScalarTest Q φ)

The product-sign folded parent test is smooth when the parent test is smooth.

theorem HCPolySupport.hasCompactSupport_cubeDirichletOddReflectionFoldedParentScalarTest {d : ℕ} (Q : TriadicCube d) {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) : HasCompactSupport (cubeDirichletOddReflectionFoldedParentScalarTest Q φ)

The product-sign folded parent test has compact support when the parent test has compact support.

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

Coordinate derivative of the product-sign folded parent test.

noncomputable def HCPolySupport.H10Function.cubeDirichletOddReflectionFoldedParentScalarTestToH10 {d : ℕ} (m : ℤ) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : H10Function (openCubeSet (originCube d m))

The folded parent test, packaged as an H¹₀ function on an origin cube.

Equations

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

theorem HCPolySupport.setIntegral_cubeFaceReflectionCellCube_vecDot_cubeDirichletOddReflectionVectorField_eq {d : ℕ} {Q : TriadicCube d} {G : Vec d → Vec d} (choice : Fin d → Fin 3) {φ : Vec d → ℝ} : ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), vecDot (cubeDirichletOddReflectionVectorField Q G x) (euclideanGradient φ x) = ∫ (y : Vec d) in openCubeSet Q, cubeDirichletOddReflectionCellSign choice * vecDot (G y) ((cubeFaceReflectionCellFoldLinear choice) (euclideanGradient φ (cubeFaceReflectionCellFoldMap Q choice y)))

Change variables on one reflection cell in the odd-reflected gradient pairing.

theorem HCPolySupport.setIntegral_cubeFaceReflectionCellCube_cubeDirichletOddReflectionScalar_mul_eq {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (choice : Fin d → Fin 3) {φ : Vec d → ℝ} : ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), cubeDirichletOddReflectionScalar Q F x * φ x = ∫ (y : Vec d) in openCubeSet Q, F y * (cubeDirichletOddReflectionCellSign choice * φ (cubeFaceReflectionCellFoldMap Q choice y))

Change variables on one reflection cell in the odd-reflected scalar pairing.

theorem HCPolySupport.setIntegral_cubeReflection_vectorDot_oddReflectedField_eq_foldedDerivativeSum {d : ℕ} {Q : TriadicCube d} {G : Vec d → Vec d} (hG : MemVectorL2 (openCubeSet Q) G) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, vecDot (cubeDirichletOddReflectionVectorField Q G x) (euclideanGradient φ x) = ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) fun (i : Fin d) => ∑ choice : Fin d → Fin 3, cubeDirichletOddReflectionCellSign choice * cubeFaceReflectionCellFoldSign choice i * euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap Q choice y)

The block pairing with the odd-reflected vector field is the original-cube pairing against the folded derivative sum.

theorem HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionScalar_mul_eq_folded {d : ℕ} {Q : TriadicCube d} {F : Vec d → ℝ} (hF : MemScalarL2 (openCubeSet Q) F) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeDirichletOddReflectionScalar Q F x * φ x = ∫ (y : Vec d) in openCubeSet Q, F y * ∑ choice : Fin d → Fin 3, cubeDirichletOddReflectionCellSign choice * φ (cubeFaceReflectionCellFoldMap Q choice y)

The block pairing with the odd-reflected scalar forcing is the original-cube folded scalar pairing.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.test_cubeDirichletOddReflectionFoldedParentScalarTest_originCube {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F φ : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : ∫ (y : Vec d) in openCubeSet (originCube d m), vecDot (u.grad y) (euclideanGradient (cubeDirichletOddReflectionFoldedParentScalarTest (originCube d m) φ) y) = ∫ (y : Vec d) in openCubeSet (originCube d m), F y * cubeDirichletOddReflectionFoldedParentScalarTest (originCube d m) φ y

The original Dirichlet weak equation may be tested against the folded parent test produced by odd reflection.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.test_cubeDirichletOddReflectionFoldedParentScalarTest_derivSum_originCube {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F φ : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : (∫ (y : Vec d) in openCubeSet (originCube d m), vecDot (u.grad y) fun (i : Fin d) => ∑ choice : Fin d → Fin 3, cubeDirichletOddReflectionCellSign choice * cubeFaceReflectionCellFoldSign choice i * euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap (originCube d m) choice y)) = ∫ (y : Vec d) in openCubeSet (originCube d m), F y * ∑ choice : Fin d → Fin 3, cubeDirichletOddReflectionCellSign choice * φ (cubeFaceReflectionCellFoldMap (originCube d m) choice y)

Expanded cell-sum form of the folded-test weak identity. This is the algebraic shape needed for the subsequent reflected-block change-of-variables step.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeFaceReflectionBlock_oddWeakEquationOnBlock_originCube {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F φ : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MemScalarL2 (openCubeSet (originCube d m)) F) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet (originCube d m), vecDot (cubeDirichletOddReflectionVectorField (originCube d m) (fun (y : Vec d) => u.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in cubeFaceReflectionBlockSet (originCube d m), cubeDirichletOddReflectionScalar (originCube d m) F x * φ x

Compact-test weak equation for the odd-reflected Dirichlet solution on the full all-coordinate reflection block of an origin cube.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletOddReflectionParent_weakEquationOnParent_originCube {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F φ : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MemScalarL2 (openCubeSet (originCube d m)) F) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (cubeDirichletOddReflectionVectorField (originCube d m) (fun (y : Vec d) => u.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeDirichletOddReflectionScalar (originCube d m) F x * φ x

Centered parent-cube compact-test weak equation for the odd-reflected Dirichlet solution.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.oddReflectedParent_satisfies_weakEquation {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F φ : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet (originCube d (m + 1))) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (cubeDirichletOddReflectionVectorField (originCube d m) (fun (y : Vec d) => u.grad y) x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeDirichletOddReflectionScalar (originCube d m) F x * φ x

Centered parent-cube weak equation, with the forcing hypothesis in the normalized cube measure used by the public regularity contract.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletOddReflectionParent_weakPoissonEquationOn_originCube_of_grad_eq {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (uP : H1Function (openCubeSet (originCube d (m + 1)))) (huP_grad : uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) : WeakPoissonEquationOn (openCubeSet (originCube d (m + 1))) uP (cubeDirichletOddReflectionScalar (originCube d m) F)

If the odd-reflected vector field has already been realized as the weak gradient of an H¹ function on the centered parent cube, the parent integral identity becomes the standard WeakPoissonEquationOn interface.