Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.VectorFieldAndApex.BlockFold

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

noncomputable def HCPolySupport.H1Function.cubeFaceReflectionCellFold {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) : H1Function (openCubeSet (cubeFaceReflectionCellCube Q choice))

Precompose an H¹ function on the original cube with one affine reflection-cell fold. On that cell, the weak gradient is the corresponding linear sign fold of the original weak gradient.

Equations

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

@[simp]

theorem HCPolySupport.H1Function.cubeFaceReflectionCellFold_toFun {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) (x : Vec d) : (u.cubeFaceReflectionCellFold choice).toFun x = u.toFun (cubeFaceReflectionCellFoldMap Q choice x)

@[simp]

theorem HCPolySupport.H1Function.cubeFaceReflectionCellFold_grad {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) (x : Vec d) : (u.cubeFaceReflectionCellFold choice).grad x = (cubeFaceReflectionCellFoldLinear choice) (u.grad (cubeFaceReflectionCellFoldMap Q choice x))

theorem HCPolySupport.H1Function.cubeFaceReflectionCellFold_isPotentialOn {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) : IsPotentialOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) fun (x : Vec d) => (cubeFaceReflectionCellFoldLinear choice) (u.grad (cubeFaceReflectionCellFoldMap Q choice x))

theorem HCPolySupport.H1Function.cubeFaceReflectionCellFold_isPotentialOn_reflectedVectorField {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) : IsPotentialOn (openCubeSet (cubeFaceReflectionCellCube Q choice)) (cubeCoordinateFoldReflectedVectorField Q fun (y : Vec d) => u.grad y)

On a reflection cell, the reflected vector field is the weak gradient of the cell-folded potential, using the global reflected-vector representative.

theorem HCPolySupport.H1Function.cubeFaceReflectionCellFold_weakGradient_of_tsupport_subset_block {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ cubeFaceReflectionBlockSet Q) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), cubeCoordinateFoldReflectedScalar Q u.toFun x * euclideanCoordDeriv i φ x = -∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => u.grad y) x i * φ x

Single-cell weak-gradient identity for a test supported in the full reflection block, localized to this cell by zero extension. The statement uses the global reflected scalar/vector representatives, so it can be summed over cells without further representative conversions.

noncomputable def HCPolySupport.H1Function.cubeFaceReflectionBlockFold {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : H1Function (cubeFaceReflectionBlockSet Q)

Fold an H¹ function on the original cube to the whole all-coordinate reflection block. The scalar part is even-reflected by coordinate folding, and the weak gradient is the corresponding reflected vector field.

Equations

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

@[simp]

theorem HCPolySupport.H1Function.cubeFaceReflectionBlockFold_toFun {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (x : Vec d) : u.cubeFaceReflectionBlockFold.toFun x = cubeCoordinateFoldReflectedScalar Q u.toFun x

@[simp]

theorem HCPolySupport.H1Function.cubeFaceReflectionBlockFold_grad {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (x : Vec d) : u.cubeFaceReflectionBlockFold.grad x = cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => u.grad y) x

theorem HCPolySupport.H1Function.cubeFaceReflectionBlockFold_isPotentialOn {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : IsPotentialOn (cubeFaceReflectionBlockSet Q) (cubeCoordinateFoldReflectedVectorField Q fun (y : Vec d) => u.grad y)

The reflected vector field on the whole reflection block is a Sobolev potential, witnessed by the block-folded scalar potential.