Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.Definitions

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

noncomputable def HCPolySupport.foldedCubeUpperFaceMeanZeroH1Test {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : H1MeanZeroFunction (openCubeSet Q)

The folded upper-face test, normalized to the mean-zero Neumann test space.

The normalization subtracts a constant only, so its weak gradient is still the folded classical gradient.

Equations

• HCPolySupport.foldedCubeUpperFaceMeanZeroH1Test Q i hφ = (HCPolySupport.foldedCubeUpperFaceH1Test Q i hφ).toMeanZero

noncomputable def HCPolySupport.foldedCubeLowerFaceMeanZeroH1Test {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : H1MeanZeroFunction (openCubeSet Q)

The folded lower-face test, normalized to the mean-zero Neumann test space.

The normalization subtracts a constant only, so its weak gradient is still the folded classical gradient.

Equations

• HCPolySupport.foldedCubeLowerFaceMeanZeroH1Test Q i hφ = (HCPolySupport.foldedCubeLowerFaceH1Test Q i hφ).toMeanZero

@[simp]

theorem HCPolySupport.foldedCubeUpperFaceMeanZeroH1Test_grad {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x : Vec d) : (foldedCubeUpperFaceMeanZeroH1Test Q i hφ).toH1Function.grad x = euclideanGradient (foldedCubeUpperFaceTest Q i φ) x

@[simp]

theorem HCPolySupport.foldedCubeLowerFaceMeanZeroH1Test_grad {d : ℕ} (Q : TriadicCube d) (i : Fin d) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x : Vec d) : (foldedCubeLowerFaceMeanZeroH1Test Q i hφ).toH1Function.grad x = euclideanGradient (foldedCubeLowerFaceTest Q i φ) x

theorem HCPolySupport.setIntegral_mul_foldedCubeUpperFaceMeanZeroH1Test_eq_of_cubeAverage_eq_zero {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (i : Fin d) (hφ : ContDiff ℝ (↑⊤) φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q))) (hfold : MeasureTheory.Integrable (fun (x : Vec d) => F x * foldedCubeUpperFaceTest Q i φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in openCubeSet Q, F x * (foldedCubeUpperFaceMeanZeroH1Test Q i hφ).toH1Function.toFun x = ∫ (x : Vec d) in openCubeSet Q, F x * foldedCubeUpperFaceTest Q i φ x

If the forcing has zero cube average, subtracting the average from a folded upper-face test does not change the forcing pairing.

theorem HCPolySupport.setIntegral_mul_foldedCubeLowerFaceMeanZeroH1Test_eq_of_cubeAverage_eq_zero {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (i : Fin d) (hφ : ContDiff ℝ (↑⊤) φ) (hmean : cubeAverage Q F = 0) (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q))) (hfold : MeasureTheory.Integrable (fun (x : Vec d) => F x * foldedCubeLowerFaceTest Q i φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in openCubeSet Q, F x * (foldedCubeLowerFaceMeanZeroH1Test Q i hφ).toH1Function.toFun x = ∫ (x : Vec d) in openCubeSet Q, F x * foldedCubeLowerFaceTest Q i φ x

If the forcing has zero cube average, subtracting the average from a folded lower-face test does not change the forcing pairing.

theorem HCPolySupport.setIntegral_mul_foldedCubeUpperFaceTest_reflection_split {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (i : Fin d) (hmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) (hreflected : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeUpperFaceReflection Q i x)) (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in openCubeSet Q, F x * foldedCubeUpperFaceTest Q i φ x = (∫ (x : Vec d) in openCubeSet Q, F x * φ x) + ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), F (cubeUpperFaceReflection Q i x) * φ x

Split the forcing pairing against a folded upper-face test into the original cube and its reflected upper-face neighbor.

theorem HCPolySupport.setIntegral_mul_foldedCubeLowerFaceTest_reflection_split {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (i : Fin d) (hmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) (hreflected : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeLowerFaceReflection Q i x)) (MeasureTheory.volume.restrict (openCubeSet Q))) : ∫ (x : Vec d) in openCubeSet Q, F x * foldedCubeLowerFaceTest Q i φ x = (∫ (x : Vec d) in openCubeSet Q, F x * φ x) + ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), F (cubeLowerFaceReflection Q i x) * φ x

Split the forcing pairing against a folded lower-face test into the original cube and its reflected lower-face neighbor.

theorem HCPolySupport.integrable_mul_foldedCubeUpperFaceTest_of_integrable_split {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (i : Fin d) (hmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) (hreflected : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeUpperFaceReflection Q i x)) (MeasureTheory.volume.restrict (openCubeSet Q))) : MeasureTheory.Integrable (fun (x : Vec d) => F x * foldedCubeUpperFaceTest Q i φ x) (MeasureTheory.volume.restrict (openCubeSet Q))

Integrability of the upper-face folded forcing pairing follows from integrability of the original and reflected pieces.

theorem HCPolySupport.integrable_mul_foldedCubeLowerFaceTest_of_integrable_split {d : ℕ} {Q : TriadicCube d} {F φ : Vec d → ℝ} (i : Fin d) (hmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q))) (hreflected : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeLowerFaceReflection Q i x)) (MeasureTheory.volume.restrict (openCubeSet Q))) : MeasureTheory.Integrable (fun (x : Vec d) => F x * foldedCubeLowerFaceTest Q i φ x) (MeasureTheory.volume.restrict (openCubeSet Q))

Integrability of the lower-face folded forcing pairing follows from integrability of the original and reflected pieces.

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

Piecewise gradient-pairing integrand for the upper-face doubled domain: the original field on Q, and the reflected field on the upper neighbor.

Equations

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

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

Piecewise gradient-pairing integrand for the lower-face doubled domain: the original field on Q, and the reflected field on the lower neighbor.

Equations

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

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

Piecewise forcing integrand for the upper-face doubled domain: the original forcing on Q, and the reflected forcing on the upper neighbor.

Equations

• HCPolySupport.upperFaceReflectedForcingIntegrand Q i F φ x = if x ∈ HCPolySupport.openCubeSet Q then F x * φ x else F (HCPolySupport.cubeUpperFaceReflection Q i x) * φ x

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

Piecewise forcing integrand for the lower-face doubled domain: the original forcing on Q, and the reflected forcing on the lower neighbor.

Equations

• HCPolySupport.lowerFaceReflectedForcingIntegrand Q i F φ x = if x ∈ HCPolySupport.openCubeSet Q then F x * φ x else F (HCPolySupport.cubeLowerFaceReflection Q i x) * φ x

noncomputable def HCPolySupport.upperFaceReflectedVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) : Vec d → Vec d

Even-reflected vector field across the upper face of Q, written on the doubled domain by using the original field on Q and the reflected field on the neighboring cube.

Equations

• HCPolySupport.upperFaceReflectedVectorField Q i G x = if x ∈ HCPolySupport.openCubeSet Q then G x else (HCPolySupport.coordReflectionLinear i) (G (HCPolySupport.cubeUpperFaceReflection Q i x))

noncomputable def HCPolySupport.lowerFaceReflectedVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) : Vec d → Vec d

Even-reflected vector field across the lower face of Q.

Equations

• HCPolySupport.lowerFaceReflectedVectorField Q i G x = if x ∈ HCPolySupport.openCubeSet Q then G x else (HCPolySupport.coordReflectionLinear i) (G (HCPolySupport.cubeLowerFaceReflection Q i x))

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

Even-reflected scalar forcing across the upper face of Q.

Equations

• HCPolySupport.upperFaceReflectedScalar Q i F x = if x ∈ HCPolySupport.openCubeSet Q then F x else F (HCPolySupport.cubeUpperFaceReflection Q i x)

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

Even-reflected scalar forcing across the lower face of Q.

Equations

• HCPolySupport.lowerFaceReflectedScalar Q i F x = if x ∈ HCPolySupport.openCubeSet Q then F x else F (HCPolySupport.cubeLowerFaceReflection Q i x)

noncomputable def HCPolySupport.faceNeighborSlabReflectedVectorField {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) : Vec d → Vec d

Even-reflected vector field on the one-coordinate lower/original/upper face-neighbor slab.

Equations

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

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

Even-reflected scalar forcing on the one-coordinate lower/original/upper face-neighbor slab.

Equations

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

@[simp]

theorem HCPolySupport.faceNeighborSlabReflectedVectorField_of_mem_lower {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)) : faceNeighborSlabReflectedVectorField Q i G x = (coordReflectionLinear i) (G (cubeLowerFaceReflection Q i x))

@[simp]

theorem HCPolySupport.faceNeighborSlabReflectedScalar_of_mem_lower {d : ℕ} (Q : TriadicCube d) (i : Fin d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)) : faceNeighborSlabReflectedScalar Q i F x = F (cubeLowerFaceReflection Q i x)

@[simp]

theorem HCPolySupport.faceNeighborSlabReflectedVectorField_of_mem_cube {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) : faceNeighborSlabReflectedVectorField Q i G x = G x

@[simp]

theorem HCPolySupport.faceNeighborSlabReflectedScalar_of_mem_cube {d : ℕ} (Q : TriadicCube d) (i : Fin d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet Q) : faceNeighborSlabReflectedScalar Q i F x = F x

@[simp]

theorem HCPolySupport.faceNeighborSlabReflectedVectorField_of_mem_upper {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)) : faceNeighborSlabReflectedVectorField Q i G x = (coordReflectionLinear i) (G (cubeUpperFaceReflection Q i x))

@[simp]

theorem HCPolySupport.faceNeighborSlabReflectedScalar_of_mem_upper {d : ℕ} (Q : TriadicCube d) (i : Fin d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)) : faceNeighborSlabReflectedScalar Q i F x = F (cubeUpperFaceReflection Q i x)

theorem HCPolySupport.cubeCoordinateFoldReflectedScalar_eq_faceNeighborSlabReflectedScalar_of_mem_lower {d : ℕ} (Q : TriadicCube d) (i : Fin d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)) : cubeCoordinateFoldReflectedScalar Q F x = faceNeighborSlabReflectedScalar Q i F x

On the lower slab cube, the all-coordinate reflected scalar agrees with the one-coordinate slab reflected scalar.

theorem HCPolySupport.cubeCoordinateFoldReflectedScalar_eq_faceNeighborSlabReflectedScalar_of_mem_cube {d : ℕ} (Q : TriadicCube d) (i : Fin d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet Q) : cubeCoordinateFoldReflectedScalar Q F x = faceNeighborSlabReflectedScalar Q i F x

On the original cube, the all-coordinate reflected scalar agrees with the one-coordinate slab reflected scalar.

theorem HCPolySupport.cubeCoordinateFoldReflectedScalar_eq_faceNeighborSlabReflectedScalar_of_mem_upper {d : ℕ} (Q : TriadicCube d) (i : Fin d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)) : cubeCoordinateFoldReflectedScalar Q F x = faceNeighborSlabReflectedScalar Q i F x

On the upper slab cube, the all-coordinate reflected scalar agrees with the one-coordinate slab reflected scalar.

theorem HCPolySupport.cubeCoordinateFoldReflectedVectorField_eq_faceNeighborSlabReflectedVectorField_of_mem_lower {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)) : cubeCoordinateFoldReflectedVectorField Q G x = faceNeighborSlabReflectedVectorField Q i G x

On the lower slab cube, the all-coordinate reflected vector field agrees with the one-coordinate slab reflected vector field.

theorem HCPolySupport.cubeCoordinateFoldReflectedVectorField_eq_faceNeighborSlabReflectedVectorField_of_mem_cube {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) : cubeCoordinateFoldReflectedVectorField Q G x = faceNeighborSlabReflectedVectorField Q i G x

On the original cube, the all-coordinate reflected vector field agrees with the one-coordinate slab reflected vector field.

theorem HCPolySupport.cubeCoordinateFoldReflectedVectorField_eq_faceNeighborSlabReflectedVectorField_of_mem_upper {d : ℕ} (Q : TriadicCube d) (i : Fin d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)) : cubeCoordinateFoldReflectedVectorField Q G x = faceNeighborSlabReflectedVectorField Q i G x

On the upper slab cube, the all-coordinate reflected vector field agrees with the one-coordinate slab reflected vector field.

theorem HCPolySupport.memScalarL2_openCubeSet_union_upperFaceReflectedScalar {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : MemScalarL2 (openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i)) (upperFaceReflectedScalar Q i F)

The upper-face reflected scalar forcing is L² on the doubled cube-neighbor domain whenever the original forcing is L² on Q.

theorem HCPolySupport.memScalarL2_openCubeSet_union_lowerFaceReflectedScalar {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : MemScalarL2 (openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i)) (lowerFaceReflectedScalar Q i F)

The lower-face reflected scalar forcing is L² on the doubled cube-neighbor domain whenever the original forcing is L² on Q.

theorem HCPolySupport.memVectorL2_openCubeSet_union_upperFaceReflectedVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : MemVectorL2 (openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i)) (upperFaceReflectedVectorField Q i G)

The upper-face reflected vector field is L² on the doubled cube-neighbor domain whenever the original vector field is L² on Q.

theorem HCPolySupport.memVectorL2_openCubeSet_union_lowerFaceReflectedVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : MemVectorL2 (openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i)) (lowerFaceReflectedVectorField Q i G)

The lower-face reflected vector field is L² on the doubled cube-neighbor domain whenever the original vector field is L² on Q.

theorem HCPolySupport.memScalarL2_cubeFaceNeighborSlabSet_faceNeighborSlabReflectedScalar {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : MemScalarL2 (cubeFaceNeighborSlabSet Q i) (faceNeighborSlabReflectedScalar Q i F)

The one-coordinate slab-reflected scalar forcing is L² on the lower/original/upper face-neighbor slab whenever the original forcing is L² on Q.

theorem HCPolySupport.memVectorL2_cubeFaceNeighborSlabSet_faceNeighborSlabReflectedVectorField {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : MemVectorL2 (cubeFaceNeighborSlabSet Q i) (faceNeighborSlabReflectedVectorField Q i G)

The one-coordinate slab-reflected vector field is L² on the lower/original/upper face-neighbor slab whenever the original vector field is L² on Q.