Coarse-graining support: Support.Sobolev.Foundations.CubeReflection.Homeomorphism

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

theorem HCPolySupport.injective_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) : Function.Injective (coordFaceReflection a i)

def HCPolySupport.coordFaceReflectionHomeomorph {d : ℕ} (a : ℝ) (i : Fin d) : Vec d ≃ₜ Vec d

Reflection through the coordinate hyperplane x i = a, packaged as an involutive homeomorphism.

Equations

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

noncomputable def HCPolySupport.cubeUpperFaceReflectionHomeomorph {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Vec d ≃ₜ Vec d

Reflection through the upper ith cube face, packaged as an involutive homeomorphism.

Equations

• HCPolySupport.cubeUpperFaceReflectionHomeomorph Q i = HCPolySupport.coordFaceReflectionHomeomorph (HCPolySupport.cubeUpperFaceCoord Q i) i

noncomputable def HCPolySupport.cubeLowerFaceReflectionHomeomorph {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Vec d ≃ₜ Vec d

Reflection through the lower ith cube face, packaged as an involutive homeomorphism.

Equations

• HCPolySupport.cubeLowerFaceReflectionHomeomorph Q i = HCPolySupport.coordFaceReflectionHomeomorph (HCPolySupport.cubeLowerFaceCoord Q i) i

theorem HCPolySupport.measurableEmbedding_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) : MeasurableEmbedding (coordFaceReflection a i)

theorem HCPolySupport.measurableEmbedding_cubeUpperFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : MeasurableEmbedding (cubeUpperFaceReflection Q i)

theorem HCPolySupport.measurableEmbedding_cubeLowerFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : MeasurableEmbedding (cubeLowerFaceReflection Q i)

theorem HCPolySupport.preimage_cubeUpperFaceReflection_openCubeSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeUpperFaceReflection Q i ⁻¹' openCubeSet Q = openCubeSet (cubeUpperFaceNeighbor Q i)

theorem HCPolySupport.preimage_cubeUpperFaceReflection_neighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeUpperFaceReflection Q i ⁻¹' openCubeSet (cubeUpperFaceNeighbor Q i) = openCubeSet Q

theorem HCPolySupport.preimage_cubeLowerFaceReflection_openCubeSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeLowerFaceReflection Q i ⁻¹' openCubeSet Q = openCubeSet (cubeLowerFaceNeighbor Q i)

theorem HCPolySupport.preimage_cubeLowerFaceReflection_neighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeLowerFaceReflection Q i ⁻¹' openCubeSet (cubeLowerFaceNeighbor Q i) = openCubeSet Q

theorem HCPolySupport.setIntegral_cubeUpperFaceNeighbor_comp_reflection {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (i : Fin d) (g : Vec d → E) : ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), g (cubeUpperFaceReflection Q i x) = ∫ (y : Vec d) in openCubeSet Q, g y

theorem HCPolySupport.setIntegral_openCubeSet_comp_cubeUpperFaceReflection {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (i : Fin d) (g : Vec d → E) : ∫ (x : Vec d) in openCubeSet Q, g (cubeUpperFaceReflection Q i x) = ∫ (y : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), g y

theorem HCPolySupport.setIntegral_cubeLowerFaceNeighbor_comp_reflection {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (i : Fin d) (g : Vec d → E) : ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), g (cubeLowerFaceReflection Q i x) = ∫ (y : Vec d) in openCubeSet Q, g y

theorem HCPolySupport.setIntegral_openCubeSet_comp_cubeLowerFaceReflection {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (i : Fin d) (g : Vec d → E) : ∫ (x : Vec d) in openCubeSet Q, g (cubeLowerFaceReflection Q i x) = ∫ (y : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), g y

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

Integrability of a reflected scalar forcing/test product transports from Q to the upper face neighbor.

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

Integrability of a reflected scalar forcing/test product transports from Q to the lower face neighbor.

theorem HCPolySupport.memScalarL2_cubeUpperFaceNeighbor_comp_reflection {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : MemScalarL2 (openCubeSet (cubeUpperFaceNeighbor Q i)) fun (x : Vec d) => F (cubeUpperFaceReflection Q i x)

Scalar L² membership transports from Q to the upper face neighbor by precomposition with the upper face reflection.

theorem HCPolySupport.memScalarL2_cubeLowerFaceNeighbor_comp_reflection {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) (hF : MemScalarL2 (openCubeSet Q) F) : MemScalarL2 (openCubeSet (cubeLowerFaceNeighbor Q i)) fun (x : Vec d) => F (cubeLowerFaceReflection Q i x)

Scalar L² membership transports from Q to the lower face neighbor by precomposition with the lower face reflection.

theorem HCPolySupport.memVectorL2_cubeUpperFaceNeighbor_reflected {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : MemVectorL2 (openCubeSet (cubeUpperFaceNeighbor Q i)) fun (x : Vec d) => (coordReflectionLinear i) (G (cubeUpperFaceReflection Q i x))

Vector L² membership transports from Q to the upper face neighbor under the reflected vector-field rule.

theorem HCPolySupport.memVectorL2_cubeLowerFaceNeighbor_reflected {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) (hG : MemVectorL2 (openCubeSet Q) G) : MemVectorL2 (openCubeSet (cubeLowerFaceNeighbor Q i)) fun (x : Vec d) => (coordReflectionLinear i) (G (cubeLowerFaceReflection Q i x))

Vector L² membership transports from Q to the lower face neighbor under the reflected vector-field rule.

theorem HCPolySupport.setIntegral_cubeUpperFaceNeighbor_reflectedScalar_sq {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), F (cubeUpperFaceReflection Q i x) * F (cubeUpperFaceReflection Q i x) = ∫ (y : Vec d) in openCubeSet Q, F y * F y

The scalar square integral is preserved when transported to the upper face neighbor by reflection.

theorem HCPolySupport.setIntegral_cubeLowerFaceNeighbor_reflectedScalar_sq {d : ℕ} {F : Vec d → ℝ} (Q : TriadicCube d) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), F (cubeLowerFaceReflection Q i x) * F (cubeLowerFaceReflection Q i x) = ∫ (y : Vec d) in openCubeSet Q, F y * F y

The scalar square integral is preserved when transported to the lower face neighbor by reflection.

theorem HCPolySupport.setIntegral_cubeUpperFaceNeighbor_reflectedField_self_pairing {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (G (cubeUpperFaceReflection Q i x))) ((coordReflectionLinear i) (G (cubeUpperFaceReflection Q i x))) = ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)

The vector self-pairing integral is preserved when the vector field is reflected to the upper face neighbor.

theorem HCPolySupport.setIntegral_cubeLowerFaceNeighbor_reflectedField_self_pairing {d : ℕ} {G : Vec d → Vec d} (Q : TriadicCube d) (i : Fin d) : ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (G (cubeLowerFaceReflection Q i x))) ((coordReflectionLinear i) (G (cubeLowerFaceReflection Q i x))) = ∫ (y : Vec d) in openCubeSet Q, vecDot (G y) (G y)

The vector self-pairing integral is preserved when the vector field is reflected to the lower face neighbor.