Homeomorphism

Support for the Armstrong–Vicol anomalous-diffusion formalization.

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

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

Homeomorphism reflecting one coordinate across the plane with specified coordinate value.

Equations

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

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

Homeomorphism reflecting a vector across the upper face of a triadic cube.

Equations

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

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

Homeomorphism reflecting a vector across the lower face of a triadic cube.

Equations

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

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

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

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

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

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

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

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

theorem Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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.