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

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

@[simp]

theorem HCPolySupport.cubeCoordinateFoldSign_mul_self {d : ℕ} (Q : TriadicCube d) (x : Vec d) (i : Fin d) : cubeCoordinateFoldSign Q x i * cubeCoordinateFoldSign Q x i = 1

theorem HCPolySupport.vecDot_cubeCoordinateFoldReflectedVectorField_self {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (x : Vec d) : vecDot (cubeCoordinateFoldReflectedVectorField Q G x) (cubeCoordinateFoldReflectedVectorField Q G x) = vecDot (G (cubeCoordinateFold Q x)) (G (cubeCoordinateFold Q x))

The all-coordinate reflected vector field preserves pointwise Euclidean self-pairing after folding.

theorem HCPolySupport.measurableSet_cubeFaceNeighborSlabSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) : MeasurableSet (cubeFaceNeighborSlabSet Q i)

The one-coordinate face-neighbor slab is measurable.

theorem HCPolySupport.measurableSet_cubeFaceReflectionCellCoordSet {d : ℕ} (Q : TriadicCube d) (choice : Fin 3) (i : Fin d) : MeasurableSet (cubeFaceReflectionCellCoordSet Q choice i)

A one-coordinate reflection-cell strip is measurable.

theorem HCPolySupport.measurableSet_cubeFaceReflectionCellSet {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : MeasurableSet (cubeFaceReflectionCellSet Q choice)

A 3^d reflection-block cell is measurable.

theorem HCPolySupport.measurableSet_cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) : MeasurableSet (cubeFaceReflectionBlockSet Q)

The all-coordinate reflection block is measurable.

theorem HCPolySupport.cubeFaceReflectionCellSet_subset_cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : cubeFaceReflectionCellSet Q choice ⊆ cubeFaceReflectionBlockSet Q

Every reflection-block cell is contained in the full all-coordinate reflection block.

theorem HCPolySupport.cubeFaceReflectionBlockSet_eq_iUnion_cellSet {d : ℕ} (Q : TriadicCube d) : cubeFaceReflectionBlockSet Q = ⋃ (choice : Fin d → Fin 3), cubeFaceReflectionCellSet Q choice

The all-coordinate reflection block is the union of its 3^d lower/original/upper cells.

theorem HCPolySupport.cubeFaceReflectionBlockSet_eq_iUnion_cellCube {d : ℕ} (Q : TriadicCube d) : cubeFaceReflectionBlockSet Q = ⋃ (choice : Fin d → Fin 3), openCubeSet (cubeFaceReflectionCellCube Q choice)

The all-coordinate reflection block is the union of the translated open triadic cubes represented by its cells.

theorem HCPolySupport.isOpen_cubeFaceReflectionCellSet {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) : IsOpen (cubeFaceReflectionCellSet Q choice)

Every reflection-block cell is open.

theorem HCPolySupport.isOpen_cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) : IsOpen (cubeFaceReflectionBlockSet Q)

The all-coordinate reflection block is open.

theorem HCPolySupport.disjoint_cubeFaceReflectionCellCoordSet_of_ne {d : ℕ} (Q : TriadicCube d) (i : Fin d) {a b : Fin 3} (hab : a ≠ b) : Disjoint (cubeFaceReflectionCellCoordSet Q a i) (cubeFaceReflectionCellCoordSet Q b i)

Distinct one-coordinate lower/original/upper strips are disjoint.

theorem HCPolySupport.disjoint_cubeFaceReflectionCellSet_of_ne {d : ℕ} (Q : TriadicCube d) {choice₁ choice₂ : Fin d → Fin 3} (hchoice : choice₁ ≠ choice₂) : Disjoint (cubeFaceReflectionCellSet Q choice₁) (cubeFaceReflectionCellSet Q choice₂)

Different reflection-block cells are disjoint.

theorem HCPolySupport.disjoint_openCubeSet_cubeFaceReflectionCellCube_of_ne {d : ℕ} (Q : TriadicCube d) {choice₁ choice₂ : Fin d → Fin 3} (hchoice : choice₁ ≠ choice₂) : Disjoint (openCubeSet (cubeFaceReflectionCellCube Q choice₁)) (openCubeSet (cubeFaceReflectionCellCube Q choice₂))

The translated open cubes associated to different reflection cells are disjoint.

theorem HCPolySupport.setIntegral_cubeFaceReflectionBlockSet_cellCube {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Q : TriadicCube d) (f : Vec d → E) (hf : ∀ (choice : Fin d → Fin 3), MeasureTheory.Integrable f (MeasureTheory.volume.restrict (openCubeSet (cubeFaceReflectionCellCube Q choice)))) : ∫ (x : Vec d) in cubeFaceReflectionBlockSet Q, f x = ∑ choice : Fin d → Fin 3, ∫ (x : Vec d) in openCubeSet (cubeFaceReflectionCellCube Q choice), f x

Set-integral split over the all-coordinate reflection block, written as a finite sum over its translated open triadic-cube cells.

theorem HCPolySupport.card_cubeFaceReflectionChoices (d : ℕ) : Fintype.card (Fin d → Fin 3) = 3 ^ d

The reflection block has one lower/original/upper choice in each coordinate, hence 3^d cells.

theorem HCPolySupport.real_card_cubeFaceReflectionChoices (d : ℕ) : ↑(Fintype.card (Fin d → Fin 3)) = 3 ^ d

Real-valued form of card_cubeFaceReflectionChoices, for constants in energy estimates.

theorem HCPolySupport.openCubeSet_subset_cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) : openCubeSet Q ⊆ cubeFaceReflectionBlockSet Q

The original open cube is contained in the all-coordinate reflection block.

theorem HCPolySupport.openCubeSet_cubeLowerFaceNeighbor_subset_cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) : openCubeSet (cubeLowerFaceNeighbor Q i) ⊆ cubeFaceReflectionBlockSet Q

A lower same-scale face neighbor is contained in the all-coordinate reflection block.

theorem HCPolySupport.openCubeSet_cubeUpperFaceNeighbor_subset_cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) : openCubeSet (cubeUpperFaceNeighbor Q i) ⊆ cubeFaceReflectionBlockSet Q

An upper same-scale face neighbor is contained in the all-coordinate reflection block.

theorem HCPolySupport.cubeFaceNeighborSlabSet_subset_cubeFaceReflectionBlockSet {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeFaceNeighborSlabSet Q i ⊆ cubeFaceReflectionBlockSet Q

Every one-coordinate lower/original/upper slab is contained in the all-coordinate reflection block.

theorem HCPolySupport.cubeCoordinateFold_eq_self_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) {x : Vec d} (hx : x ∈ openCubeSet Q) : cubeCoordinateFold Q x = x

On the original open cube, the coordinatewise fold is the identity.

theorem HCPolySupport.cubeCoordinateFoldReflectedScalar_eq_self_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet Q) : cubeCoordinateFoldReflectedScalar Q F x = F x

theorem HCPolySupport.cubeCoordinateFoldReflectedVectorField_eq_self_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) : cubeCoordinateFoldReflectedVectorField Q G x = G x

theorem HCPolySupport.cubeCoordinateFold_eq_cubeLowerFaceReflection_of_mem_neighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)) : cubeCoordinateFold Q x = cubeLowerFaceReflection Q i x

On the lower same-scale face neighbor, the all-coordinate fold is the one-coordinate lower-face reflection.

theorem HCPolySupport.cubeCoordinateFold_eq_cubeUpperFaceReflection_of_mem_neighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)) : cubeCoordinateFold Q x = cubeUpperFaceReflection Q i x

On the upper same-scale face neighbor, the all-coordinate fold is the one-coordinate upper-face reflection.

theorem HCPolySupport.cubeCoordinateFoldSign_eq_one_of_mem_openCubeSet {d : ℕ} (Q : TriadicCube d) {x : Vec d} (hx : x ∈ openCubeSet Q) (i : Fin d) : cubeCoordinateFoldSign Q x i = 1

The all-coordinate fold sign is 1 on the original open cube.

theorem HCPolySupport.cubeCoordinateFoldSign_of_mem_cubeLowerFaceNeighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeLowerFaceNeighbor Q i)) (j : Fin d) : cubeCoordinateFoldSign Q x j = if j = i then -1 else 1

On the lower same-scale face neighbor, the all-coordinate fold sign is the one-coordinate reflection sign.

theorem HCPolySupport.cubeCoordinateFoldSign_of_mem_cubeUpperFaceNeighbor {d : ℕ} (Q : TriadicCube d) (i : Fin d) {x : Vec d} (hx : x ∈ openCubeSet (cubeUpperFaceNeighbor Q i)) (j : Fin d) : cubeCoordinateFoldSign Q x j = if j = i then -1 else 1

On the upper same-scale face neighbor, the all-coordinate fold sign is the one-coordinate reflection sign.

theorem HCPolySupport.cubeCoordinateFold_mem_openCubeSet_of_mem_block {d : ℕ} (Q : TriadicCube d) {x : Vec d} (hx : x ∈ cubeFaceReflectionBlockSet Q) : cubeCoordinateFold Q x ∈ openCubeSet Q

The coordinatewise fold maps the open all-coordinate reflection block into the original open cube.

theorem HCPolySupport.cubeCoordinateFold_eq_cubeFaceReflectionCellFoldMap_of_mem_cellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) : cubeCoordinateFold Q x = cubeFaceReflectionCellFoldMap Q choice x

On each reflection-block cell, the x-dependent coordinate fold agrees with the affine fold map attached to that cell.

theorem HCPolySupport.cubeCoordinateFoldSign_eq_cellFoldLinear_sign_of_mem_cellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) (i : Fin d) : cubeCoordinateFoldSign Q x i = if choice i = 1 then 1 else -1

On each reflection-block cell, the x-dependent fold sign is the constant sign of the affine cell fold.

theorem HCPolySupport.cubeCoordinateFoldReflectedScalar_eq_cellFoldMap_of_mem_cellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (F : Vec d → ℝ) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) : cubeCoordinateFoldReflectedScalar Q F x = F (cubeFaceReflectionCellFoldMap Q choice x)

On each reflection-block cell, scalar pullback by the x-dependent fold agrees with scalar pullback by the affine cell fold.

theorem HCPolySupport.cubeCoordinateFoldReflectedVectorField_eq_cellFoldLinear_of_mem_cellCube {d : ℕ} (Q : TriadicCube d) (choice : Fin d → Fin 3) (G : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet (cubeFaceReflectionCellCube Q choice)) : cubeCoordinateFoldReflectedVectorField Q G x = (cubeFaceReflectionCellFoldLinear choice) (G (cubeFaceReflectionCellFoldMap Q choice x))

On each reflection-block cell, the reflected vector field agrees with the affine cell-fold linear sign applied to the pulled-back vector field.