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

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

Parent H¹ realization for the Dirichlet odd reflection

This file turns the pointwise odd reflection on the centered parent cube into an honest H1Function. The proof uses the closed H¹ graph: after folding parent tests back to the original cube, the zero-trace approximation package of H10Function supplies the needed integration-by-parts identity.

theorem HCPolySupport.H10Function.integral_mul_deriv_eq_neg_integral_mul_of_contDiff_hasCompactSupport {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (i : Fin d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) : ∫ (x : Vec d) in U, u.toFun x * euclideanCoordDeriv i ψ x = -∫ (x : Vec d) in U, u.grad x i * ψ x

A zero-trace H¹ function may be integrated by parts against any smooth compactly supported ambient test, without requiring the test support to lie inside the domain.

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

Fold a parent scalar test back to the original cube with the sign needed for the ith weak-gradient graph constraint of the Dirichlet odd reflection.

The coefficient is the product of the odd-reflection cell sign and the coordinate fold sign.

Equations

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

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

The signed coordinate-folded graph test is smooth when the parent test is smooth.

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

The signed coordinate-folded graph test has compact support when the parent test has compact support.

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

Coordinate derivative of the signed coordinate-folded graph test. The coordinate fold sign squares away, leaving only the odd-reflection cell sign.

theorem HCPolySupport.H10Function.foldedParentTest_integral_by_parts {d : ℕ} {m : ℤ} (u : H10Function (openCubeSet (originCube d m))) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : ∫ (y : Vec d) in openCubeSet (originCube d m), u.toFun y * ∑ choice : Fin d → Fin 3, cubeDirichletOddReflectionCellSign choice * euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap (originCube d m) choice y) = -∫ (y : Vec d) in openCubeSet (originCube d m), u.grad y i * cubeDirichletOddReflectionFoldedParentCoordTest (originCube d m) i φ y

The zero-trace weak-gradient identity tested against the signed coordinate-folded graph test, with the derivative expanded cellwise.

theorem HCPolySupport.setIntegral_openCubeSet_succ_originCube_cubeDirichletOddReflectionScalar_mul_deriv_eq_folded {d : ℕ} {m : ℤ} {F φ : Vec d → ℝ} (hF : MemScalarL2 (openCubeSet (originCube d m)) F) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeDirichletOddReflectionScalar (originCube d m) F x * euclideanCoordDeriv i φ x = ∫ (y : Vec d) in openCubeSet (originCube d m), F y * ∑ choice : Fin d → Fin 3, cubeDirichletOddReflectionCellSign choice * euclideanCoordDeriv i φ (cubeFaceReflectionCellFoldMap (originCube d m) choice y)

Centered parent-cube form of the odd reflected scalar derivative pairing.

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

Change variables on one reflection cell in one coordinate of the odd-reflected vector-field pairing.

theorem HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_cubeDirichletOddReflectionVectorField_coord_mul_eq_folded {d : ℕ} {Q : TriadicCube d} {G : Vec d → Vec d} {φ : Vec d → ℝ} (hG : MemVectorL2 (openCubeSet Q) G) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (i : Fin d) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, cubeDirichletOddReflectionVectorField Q G x i * φ x = ∫ (y : Vec d) in openCubeSet Q, G y i * cubeDirichletOddReflectionFoldedParentCoordTest Q i φ y

The block pairing with one coordinate of the odd-reflected vector field is the original-cube pairing against the signed coordinate-folded graph test.

theorem HCPolySupport.successorReflectedVector_component_integral_eq_folded {d : ℕ} {m : ℤ} {G : Vec d → Vec d} {φ : Vec d → ℝ} (hG : MemVectorL2 (openCubeSet (originCube d m)) G) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), cubeDirichletOddReflectionVectorField (originCube d m) G x i * φ x = ∫ (y : Vec d) in openCubeSet (originCube d m), G y i * cubeDirichletOddReflectionFoldedParentCoordTest (originCube d m) i φ y

Centered parent-cube form of the reflected vector coordinate pairing.

theorem HCPolySupport.mem_h1GraphClosedSubmodule_cubeDirichletOddReflection_originCube {d : ℕ} {m : ℤ} (u : H10Function (openCubeSet (originCube d m))) (hscalar : MemScalarL2 (openCubeSet (originCube d (m + 1))) (cubeDirichletOddReflectionScalar (originCube d m) u.toFun)) (hvector : MemVectorL2 (openCubeSet (originCube d (m + 1))) (cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y)) : (toScalarL2 hscalar, toHilbertVectorL2OfVecField hvector) ∈ h1GraphClosedSubmodule

The all-face odd reflection of an origin-cube zero-trace H¹ function defines a point of the closed parent-cube weak-gradient graph.

theorem HCPolySupport.exists_h1Function_cubeDirichletOddReflectionParent_originCube {d : ℕ} {m : ℤ} (u : H10Function (openCubeSet (originCube d m))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeDirichletOddReflectionScalar (originCube d m) u.toFun ∧ uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y

Choose the parent H¹ function whose exact representatives are the all-face Dirichlet odd reflection and its reflected gradient.

theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_cubeDirichletOddReflectionParent_weakPoissonEquationOn_originCube {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))) : ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeDirichletOddReflectionScalar (originCube d m) u.toFun ∧ (uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) ∧ WeakPoissonEquationOn (openCubeSet (originCube d (m + 1))) uP (cubeDirichletOddReflectionScalar (originCube d m) F)

The odd-reflected parent weak equation with the parent H¹ realization chosen by the closed graph construction.