Cube face reflections

This file begins the C.2 reflection infrastructure for the cube Neumann W^{2,2} discharge. The key analytic reflection step will be proved in weak form; the lemmas here supply the affine one-coordinate face reflections and their first coordinate-derivative chain rule.

def Homogenization.realFaceReflection (a : ℝ) : ℝ → ℝ

One-dimensional reflection through the point a.

Equations

• Homogenization.realFaceReflection a t = 2 * a - t

noncomputable def Homogenization.cubeLowerFaceCoord {d : ℕ} (Q : TriadicCube d) (i : Fin d) : ℝ

Lower coordinate face of a triadic cube.

Equations

• Homogenization.cubeLowerFaceCoord Q i = (↑(Q.index i) - 1 / 2) * Homogenization.cubeScaleFactor Q

noncomputable def Homogenization.cubeUpperFaceCoord {d : ℕ} (Q : TriadicCube d) (i : Fin d) : ℝ

Upper coordinate face of a triadic cube.

Equations

• Homogenization.cubeUpperFaceCoord Q i = (↑(Q.index i) + 1 / 2) * Homogenization.cubeScaleFactor Q

def Homogenization.coordReflectionLinear {d : ℕ} (i : Fin d) : Vec d →L[ℝ] Vec d

Linear part of reflection in the coordinate hyperplane normal to basisVec i.

Equations

• Homogenization.coordReflectionLinear i = ContinuousLinearMap.pi fun (j : Fin d) => if j = i then -ContinuousLinearMap.proj j else ContinuousLinearMap.proj j

def Homogenization.coordFaceReflectionOffset {d : ℕ} (a : ℝ) (i : Fin d) : Vec d

Translation offset for the affine reflection through the face coordinate a.

Equations

• Homogenization.coordFaceReflectionOffset a i j = if j = i then 2 * a else 0

def Homogenization.coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) : Vec d → Vec d

Reflection through the coordinate hyperplane {x_i = a}.

Equations

• Homogenization.coordFaceReflection a i x = (Homogenization.coordReflectionLinear i) x + Homogenization.coordFaceReflectionOffset a i

noncomputable def Homogenization.cubeUpperFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Vec d → Vec d

Reflection through the upper i-face of Q.

Equations

• Homogenization.cubeUpperFaceReflection Q i = Homogenization.coordFaceReflection (Homogenization.cubeUpperFaceCoord Q i) i

noncomputable def Homogenization.cubeLowerFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Vec d → Vec d

Reflection through the lower i-face of Q.

Equations

• Homogenization.cubeLowerFaceReflection Q i = Homogenization.coordFaceReflection (Homogenization.cubeLowerFaceCoord Q i) i

def Homogenization.coordIndexShift {d : ℕ} (i : Fin d) (n : ℤ) : Fin d → ℤ

Integer coordinate shift by n in one coordinate and zero tangentially.

Equations

• Homogenization.coordIndexShift i n j = if j = i then n else 0

def Homogenization.cubeUpperFaceNeighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) : TriadicCube d

Same-scale cube adjacent to Q across its upper i-face.

Equations

• Homogenization.cubeUpperFaceNeighbor Q i = Homogenization.translateCube (Homogenization.coordIndexShift i 1) Q

def Homogenization.cubeLowerFaceNeighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) : TriadicCube d

Same-scale cube adjacent to Q across its lower i-face.

Equations

• Homogenization.cubeLowerFaceNeighbor Q i = Homogenization.translateCube (Homogenization.coordIndexShift i (-1)) Q

@[simp]

theorem Homogenization.cubeLowerFaceCoord_cubeLowerFaceNeighbor_self {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeLowerFaceCoord (cubeLowerFaceNeighbor Q i) i = cubeLowerFaceCoord Q i - cubeScaleFactor Q

@[simp]

theorem Homogenization.cubeUpperFaceCoord_cubeLowerFaceNeighbor_self {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeUpperFaceCoord (cubeLowerFaceNeighbor Q i) i = cubeLowerFaceCoord Q i

@[simp]

theorem Homogenization.cubeLowerFaceCoord_cubeUpperFaceNeighbor_self {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeLowerFaceCoord (cubeUpperFaceNeighbor Q i) i = cubeUpperFaceCoord Q i

@[simp]

theorem Homogenization.cubeUpperFaceCoord_cubeUpperFaceNeighbor_self {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeUpperFaceCoord (cubeUpperFaceNeighbor Q i) i = cubeUpperFaceCoord Q i + cubeScaleFactor Q

@[simp]

theorem Homogenization.cubeLowerFaceCoord_cubeLowerFaceNeighbor_ne {d : ℕ} (Q : TriadicCube d) {i j : Fin d} (hji : j ≠ i) : cubeLowerFaceCoord (cubeLowerFaceNeighbor Q i) j = cubeLowerFaceCoord Q j

@[simp]

theorem Homogenization.cubeUpperFaceCoord_cubeLowerFaceNeighbor_ne {d : ℕ} (Q : TriadicCube d) {i j : Fin d} (hji : j ≠ i) : cubeUpperFaceCoord (cubeLowerFaceNeighbor Q i) j = cubeUpperFaceCoord Q j

@[simp]

theorem Homogenization.cubeLowerFaceCoord_cubeUpperFaceNeighbor_ne {d : ℕ} (Q : TriadicCube d) {i j : Fin d} (hji : j ≠ i) : cubeLowerFaceCoord (cubeUpperFaceNeighbor Q i) j = cubeLowerFaceCoord Q j

@[simp]

theorem Homogenization.cubeUpperFaceCoord_cubeUpperFaceNeighbor_ne {d : ℕ} (Q : TriadicCube d) {i j : Fin d} (hji : j ≠ i) : cubeUpperFaceCoord (cubeUpperFaceNeighbor Q i) j = cubeUpperFaceCoord Q j

@[simp]

theorem Homogenization.coordReflectionLinear_apply {d : ℕ} (i : Fin d) (x : Vec d) (j : Fin d) : (coordReflectionLinear i) x j = if j = i then -x j else x j

theorem Homogenization.vecDot_coordReflectionLinear_left {d : ℕ} (i : Fin d) (v w : Vec d) : vecDot ((coordReflectionLinear i) v) w = vecDot v ((coordReflectionLinear i) w)

theorem Homogenization.vecDot_coordReflectionLinear_coordReflectionLinear {d : ℕ} (i : Fin d) (v w : Vec d) : vecDot ((coordReflectionLinear i) v) ((coordReflectionLinear i) w) = vecDot v w

@[simp]

theorem Homogenization.coordFaceReflection_apply {d : ℕ} (a : ℝ) (i : Fin d) (x : Vec d) (j : Fin d) : coordFaceReflection a i x j = if j = i then 2 * a - x j else x j

theorem Homogenization.coordFaceReflection_apply_self {d : ℕ} (a : ℝ) (i : Fin d) (x : Vec d) : coordFaceReflection a i x i = 2 * a - x i

theorem Homogenization.coordFaceReflection_apply_ne {d : ℕ} (a : ℝ) (i j : Fin d) (x : Vec d) (hji : j ≠ i) : coordFaceReflection a i x j = x j

@[simp]

theorem Homogenization.realFaceReflection_apply (a t : ℝ) : realFaceReflection a t = 2 * a - t

theorem Homogenization.continuous_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) : Continuous (coordFaceReflection a i)

theorem Homogenization.continuous_cubeUpperFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Continuous (cubeUpperFaceReflection Q i)

theorem Homogenization.continuous_cubeLowerFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Continuous (cubeLowerFaceReflection Q i)

theorem Homogenization.contDiff_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) : ContDiff ℝ (↑⊤) (coordFaceReflection a i)

theorem Homogenization.contDiff_cubeUpperFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : ContDiff ℝ (↑⊤) (cubeUpperFaceReflection Q i)

theorem Homogenization.contDiff_cubeLowerFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : ContDiff ℝ (↑⊤) (cubeLowerFaceReflection Q i)

theorem Homogenization.measurePreserving_realFaceReflection (a : ℝ) : MeasureTheory.MeasurePreserving (realFaceReflection a) MeasureTheory.volume MeasureTheory.volume

theorem Homogenization.measurePreserving_coordFaceReflection {d : ℕ} (a : ℝ) (i : Fin d) : MeasureTheory.MeasurePreserving (coordFaceReflection a i) MeasureTheory.volume MeasureTheory.volume

theorem Homogenization.measurePreserving_cubeUpperFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : MeasureTheory.MeasurePreserving (cubeUpperFaceReflection Q i) MeasureTheory.volume MeasureTheory.volume

theorem Homogenization.measurePreserving_cubeLowerFaceReflection {d : ℕ} (Q : TriadicCube d) (i : Fin d) : MeasureTheory.MeasurePreserving (cubeLowerFaceReflection Q i) MeasureTheory.volume MeasureTheory.volume

theorem Homogenization.cubeUpperFaceReflection_mem_openCubeSet_of_mem_neighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)) : cubeUpperFaceReflection Q i x ∈ openCubeSet Q

theorem Homogenization.cubeUpperFaceReflection_mem_neighbor_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet Q) : cubeUpperFaceReflection Q i x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)

theorem Homogenization.cubeLowerFaceReflection_mem_openCubeSet_of_mem_neighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)) : cubeLowerFaceReflection Q i x ∈ openCubeSet Q

theorem Homogenization.cubeLowerFaceReflection_mem_neighbor_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet Q) : cubeLowerFaceReflection Q i x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)

theorem Homogenization.disjoint_openCubeSet_cubeUpperFaceNeighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Disjoint (openCubeSet Q) (openCubeSet (cubeUpperFaceNeighbor Q i))

The open cube is disjoint from its same-scale upper face neighbor.

theorem Homogenization.disjoint_openCubeSet_cubeLowerFaceNeighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Disjoint (openCubeSet Q) (openCubeSet (cubeLowerFaceNeighbor Q i))

The open cube is disjoint from its same-scale lower face neighbor.

theorem Homogenization.disjoint_cubeLowerFaceNeighbor_cubeUpperFaceNeighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Disjoint (openCubeSet (cubeLowerFaceNeighbor Q i)) (openCubeSet (cubeUpperFaceNeighbor Q i))

The lower and upper same-scale face neighbors of a cube are disjoint.

@[simp]

theorem Homogenization.coordFaceReflection_involutive {d : ℕ} (a : ℝ) (i : Fin d) (x : Vec d) : coordFaceReflection a i (coordFaceReflection a i x) = x

@[simp]

theorem Homogenization.cubeUpperFaceReflection_involutive {d : ℕ} (Q : TriadicCube d) (i : Fin d) (x : Vec d) : cubeUpperFaceReflection Q i (cubeUpperFaceReflection Q i x) = x

@[simp]

theorem Homogenization.cubeLowerFaceReflection_involutive {d : ℕ} (Q : TriadicCube d) (i : Fin d) (x : Vec d) : cubeLowerFaceReflection Q i (cubeLowerFaceReflection Q i x) = x