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

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

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 HCPolySupport.realFaceReflection (a : ℝ) : ℝ → ℝ

One-dimensional reflection through the point a.

Equations

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

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

Lower coordinate face of a triadic cube.

Equations

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

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

Upper coordinate face of a triadic cube.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Reflection through the coordinate hyperplane {x_i = a}.

Equations

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

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

Reflection through the upper i-face of Q.

Equations

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

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

Reflection through the lower i-face of Q.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem HCPolySupport.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 HCPolySupport.vecDot_coordReflectionLinear_left {d : ℕ} (i : Fin d) (v w : Vec d) : vecDot ((coordReflectionLinear i) v) w = vecDot v ((coordReflectionLinear i) w)

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

@[simp]

theorem HCPolySupport.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 HCPolySupport.coordFaceReflection_apply_self {d : ℕ} (a : ℝ) (i : Fin d) (x : Vec d) : coordFaceReflection a i x i = 2 * a - x i

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

theorem HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.coordFaceReflection_involutive {d : ℕ} (a : ℝ) (i : Fin d) (x : Vec d) : coordFaceReflection a i (coordFaceReflection a i x) = x

@[simp]

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

@[simp]

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