Coarse-graining support: Support.Sobolev.Foundations.CubeReflection.Folding.Geometry

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

def HCPolySupport.cubeFaceNeighborSlabSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Set (Vec d)

The three-cube slab obtained by adjoining both same-coordinate face neighbors to Q.

Equations

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

def HCPolySupport.cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) : Set (Vec d)

The open block obtained by allowing each coordinate to lie in the lower neighbor strip, the original cube strip, or the upper neighbor strip.

This is the all-coordinate target for iterating the one-coordinate reflection argument. It excludes the internal reflecting faces, which are null sets for the later weak-form argument.

Equations

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

def HCPolySupport.cubeFaceReflectionCellCoordSet {d : ℕ} (Q : TriadicCube d) (choice : Fin 3) (i : Fin d) : Set (Vec d)

One coordinate strip of the all-coordinate reflection block. The choice 0 is the lower neighbor strip, 1 is the original cube strip, and 2 is the upper neighbor strip.

Equations

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

def HCPolySupport.cubeFaceReflectionCellSet {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : Set (Vec d)

A 3^d cell of the all-coordinate reflection block, with an independent lower/original/upper strip choice in every coordinate.

Equations

• HCPolySupport.cubeFaceReflectionCellSet Q choice = {x : HCPolySupport.Vec d | ∀ (i : Fin d), x ∈ HCPolySupport.cubeFaceReflectionCellCoordSet Q (choice i) i}

def HCPolySupport.cubeFaceReflectionCellShift (choice : Fin 3) : ℤ

Integer shift associated to a reflection cell coordinate choice: lower/original/upper corresponds to -1/0/1.

Equations

• HCPolySupport.cubeFaceReflectionCellShift choice = if choice = 0 then -1 else if choice = 1 then 0 else 1

def HCPolySupport.cubeFaceReflectionCellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : TriadicCube d

The translated cube represented by a 3^d reflection-block cell.

Equations

• HCPolySupport.cubeFaceReflectionCellCube Q choice = HCPolySupport.translateCube (fun (i : Fin d) => HCPolySupport.cubeFaceReflectionCellShift (choice i)) Q

theorem HCPolySupport.cubeLowerFaceCoord_cubeFaceReflectionCellCube_of_choice_eq_zero {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {i : Fin d} (h0 : choice i = 0) : cubeLowerFaceCoord (cubeFaceReflectionCellCube Q choice) i = cubeLowerFaceCoord Q i - cubeScaleFactor Q

theorem HCPolySupport.cubeUpperFaceCoord_cubeFaceReflectionCellCube_of_choice_eq_zero {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {i : Fin d} (h0 : choice i = 0) : cubeUpperFaceCoord (cubeFaceReflectionCellCube Q choice) i = cubeLowerFaceCoord Q i

theorem HCPolySupport.cubeLowerFaceCoord_cubeFaceReflectionCellCube_of_choice_eq_one {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {i : Fin d} (h1 : choice i = 1) : cubeLowerFaceCoord (cubeFaceReflectionCellCube Q choice) i = cubeLowerFaceCoord Q i

theorem HCPolySupport.cubeUpperFaceCoord_cubeFaceReflectionCellCube_of_choice_eq_one {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {i : Fin d} (h1 : choice i = 1) : cubeUpperFaceCoord (cubeFaceReflectionCellCube Q choice) i = cubeUpperFaceCoord Q i

theorem HCPolySupport.cubeLowerFaceCoord_cubeFaceReflectionCellCube_of_choice_upper {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {i : Fin d} (h0 : choice i ≠ 0) (h1 : choice i ≠ 1) : cubeLowerFaceCoord (cubeFaceReflectionCellCube Q choice) i = cubeUpperFaceCoord Q i

theorem HCPolySupport.cubeUpperFaceCoord_cubeFaceReflectionCellCube_of_choice_upper {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {i : Fin d} (h0 : choice i ≠ 0) (h1 : choice i ≠ 1) : cubeUpperFaceCoord (cubeFaceReflectionCellCube Q choice) i = cubeUpperFaceCoord Q i + cubeScaleFactor Q

theorem HCPolySupport.openCubeSet_cubeFaceReflectionCellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : openCubeSet (cubeFaceReflectionCellCube Q choice) = cubeFaceReflectionCellSet Q choice

A reflection-block cell is exactly the open translated triadic cube with coordinate shifts -1/0/1 prescribed by its choices.

noncomputable def HCPolySupport.cubeCoordinateFold {d : ℕ} (Q : TriadicCube d) (x : Vec d) : Vec d

Coordinatewise fold from the all-coordinate reflection block back toward the original cube. Below the lower face it reflects through the lower face, inside the cube it is the identity, and above the upper face it reflects through the upper face.

Equations

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

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

Sign contributed to a vector component by the coordinatewise fold. The component changes sign exactly when that coordinate was reflected through one of the two faces.

Equations

• HCPolySupport.cubeCoordinateFoldSign Q x i = if x i < HCPolySupport.cubeLowerFaceCoord Q i then -1 else if x i < HCPolySupport.cubeUpperFaceCoord Q i then 1 else -1

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

Scalar field pulled back by the all-coordinate fold.

Equations

• HCPolySupport.cubeCoordinateFoldReflectedScalar Q F x = F (HCPolySupport.cubeCoordinateFold Q x)

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

Vector field pulled back by the all-coordinate fold with the reflection sign in each component.

Equations

• HCPolySupport.cubeCoordinateFoldReflectedVectorField Q G x i = HCPolySupport.cubeCoordinateFoldSign Q x i * G (HCPolySupport.cubeCoordinateFold Q x) i

noncomputable def HCPolySupport.cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : Vec d → Vec d

The affine fold map associated to one reflection-block cell. It is the same as cubeCoordinateFold on that cell, but has no x-dependent branching.

Equations

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

def HCPolySupport.cubeFaceReflectionCellFoldLinear {d : ℕ} (choice : Fin d → Fin 3) : Vec d →L[ℝ] Vec d

Linear part of the affine fold map associated to a reflection-block cell: original-coordinate choices have sign +1, reflected choices have sign -1.

Equations

• HCPolySupport.cubeFaceReflectionCellFoldLinear choice = ContinuousLinearMap.pi fun (i : Fin d) => if choice i = 1 then ContinuousLinearMap.proj i else -ContinuousLinearMap.proj i

@[simp]

theorem HCPolySupport.cubeFaceReflectionCellFoldLinear_apply {d : ℕ} (choice : Fin d → Fin 3) (v : Vec d) (i : Fin d) : (cubeFaceReflectionCellFoldLinear choice) v i = if choice i = 1 then v i else -v i

theorem HCPolySupport.cubeFaceReflectionCellFoldLinear_basisVec {d : ℕ} (choice : Fin d → Fin 3) (k : Fin d) : (cubeFaceReflectionCellFoldLinear choice) (basisVec k) = (if choice k = 1 then 1 else -1) • basisVec k

theorem HCPolySupport.cubeFaceReflectionCellFoldLinear_involutive {d : ℕ} (choice : Fin d → Fin 3) : Function.Involutive ⇑(cubeFaceReflectionCellFoldLinear choice)

theorem HCPolySupport.vecDot_cubeFaceReflectionCellFoldLinear_left {d : ℕ} (choice : Fin d → Fin 3) (v w : Vec d) : vecDot ((cubeFaceReflectionCellFoldLinear choice) v) w = vecDot v ((cubeFaceReflectionCellFoldLinear choice) w)

theorem HCPolySupport.cubeFaceReflectionCellFoldMap_involutive {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : Function.Involutive (cubeFaceReflectionCellFoldMap Q choice)

theorem HCPolySupport.injective_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : Function.Injective (cubeFaceReflectionCellFoldMap Q choice)

theorem HCPolySupport.continuous_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : Continuous (cubeFaceReflectionCellFoldMap Q choice)

noncomputable def HCPolySupport.cubeFaceReflectionCellFoldHomeomorph {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : Vec d ≃ₜ Vec d

The affine fold map associated to a reflection cell, as a homeomorphism. Its inverse is itself.

Equations

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

theorem HCPolySupport.contDiff_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : ContDiff ℝ (↑⊤) (cubeFaceReflectionCellFoldMap Q choice)

The affine fold map associated to a reflection cell is smooth.

theorem HCPolySupport.contDiff_comp_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ ↑⊤ fun (x : Vec d) => φ (cubeFaceReflectionCellFoldMap Q choice x)

Smoothness of a compact-test function is preserved by precomposition with the affine fold map of a reflection cell.

theorem HCPolySupport.fderiv_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (x : Vec d) : fderiv ℝ (cubeFaceReflectionCellFoldMap Q choice) x = cubeFaceReflectionCellFoldLinear choice

The Fréchet derivative of a reflection-cell fold map is its diagonal linear reflection part.

theorem HCPolySupport.euclideanGradient_comp_cubeFaceReflectionCellFoldMap {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (Q : TriadicCube d) (choice : Fin d → Fin 3) (x : Vec d) : euclideanGradient (fun (y : Vec d) => φ (cubeFaceReflectionCellFoldMap Q choice y)) x = (cubeFaceReflectionCellFoldLinear choice) (euclideanGradient φ (cubeFaceReflectionCellFoldMap Q choice x))

Chain rule for gradients after precomposing a smooth test with a reflection-cell fold map.

theorem HCPolySupport.euclideanCoordDeriv_comp_cubeFaceReflectionCellFoldMap {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (choice : Fin d → Fin 3) (k : Fin d) (x : Vec d) : euclideanCoordDeriv k (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x = (if choice k = 1 then 1 else -1) * euclideanCoordDeriv k u (cubeFaceReflectionCellFoldMap Q choice x)

Coordinate derivative chain rule for precomposition with a reflection-cell fold map.

theorem HCPolySupport.euclideanCoordSecondDeriv_comp_cubeFaceReflectionCellFoldMap {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (choice : Fin d → Fin 3) (k l : Fin d) (x : Vec d) : euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x = ((if choice k = 1 then 1 else -1) * if choice l = 1 then 1 else -1) * euclideanCoordSecondDeriv k l u (cubeFaceReflectionCellFoldMap Q choice x)

Second coordinate-derivative chain rule for precomposition with a reflection-cell fold map. Each reflected coordinate contributes one sign.

theorem HCPolySupport.euclideanCoordSecondDeriv_diag_comp_cubeFaceReflectionCellFoldMap {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (choice : Fin d → Fin 3) (k : Fin d) (x : Vec d) : euclideanCoordSecondDeriv k k (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x = euclideanCoordSecondDeriv k k u (cubeFaceReflectionCellFoldMap Q choice x)

Diagonal second derivatives are invariant under a reflection-cell fold.

theorem HCPolySupport.euclideanCoordLaplacian_comp_cubeFaceReflectionCellFoldMap {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (choice : Fin d → Fin 3) (x : Vec d) : euclideanCoordLaplacian (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x = euclideanCoordLaplacian u (cubeFaceReflectionCellFoldMap Q choice x)

The coordinate Laplacian is invariant under a reflection-cell fold.

theorem HCPolySupport.sum_sq_euclideanCoordSecondDeriv_comp_cubeFaceReflectionCellFoldMap {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (Q : TriadicCube d) (choice : Fin d → Fin 3) (x : Vec d) : ∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l (fun (y : Vec d) => u (cubeFaceReflectionCellFoldMap Q choice y)) x ^ 2 = ∑ k : Fin d, ∑ l : Fin d, euclideanCoordSecondDeriv k l u (cubeFaceReflectionCellFoldMap Q choice x) ^ 2

The pointwise squared Hessian sum is invariant under a reflection-cell fold.

theorem HCPolySupport.hasCompactSupport_comp_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) : HasCompactSupport fun (x : Vec d) => φ (cubeFaceReflectionCellFoldMap Q choice x)

Compact support of a test function is preserved by precomposition with the affine fold map of a reflection cell.

theorem HCPolySupport.measurableEmbedding_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : MeasurableEmbedding (cubeFaceReflectionCellFoldMap Q choice)

theorem HCPolySupport.measurePreserving_cubeFaceReflectionCellFoldMap {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : MeasureTheory.MeasurePreserving (cubeFaceReflectionCellFoldMap Q choice) MeasureTheory.volume MeasureTheory.volume

theorem HCPolySupport.preimage_cubeFaceReflectionCellFoldMap_openCubeSet {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : cubeFaceReflectionCellFoldMap Q choice ⁻¹' openCubeSet Q = openCubeSet (cubeFaceReflectionCellCube Q choice)

The cell fold map carries exactly its associated reflection-block cell onto the original open cube.

theorem HCPolySupport.setIntegral_cubeFaceReflectionCellCube_comp_cellFoldMap {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (choice : Fin d → Fin 3) (g : Vec d → E) : ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), g (cubeFaceReflectionCellFoldMap Q choice x) = ∫ (y : Vec d) in openCubeSet Q, g y

Change variables from a reflection-block cell to the original open cube using the cell fold map.

theorem HCPolySupport.integrable_cubeFaceReflectionCellCube_comp_cellFoldMap {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {Q : TriadicCube d} {choice : Fin d → Fin 3} {g : Vec d → E} (hg : MeasureTheory.Integrable g (MeasureTheory.volume.restrict (openCubeSet Q))) : MeasureTheory.Integrable (fun (x : Vec d) => g (cubeFaceReflectionCellFoldMap Q choice x)) (MeasureTheory.volume.restrict (openCubeSet (cubeFaceReflectionCellCube Q choice)))

Integrability transports from the original open cube to a reflection-block cell by precomposition with the cell fold map.