Coarse-graining support: Support.Probability.OriginCubeSymmetry

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

theorem HCPolySupport.matVecMul_signFlipMatrix_apply {d : ℕ} (i j : Fin d) (x : Vec d) : matVecMul (signFlipMatrix i) x j = (if j = i then -1 else 1) * x j

Coordinate formula for the action of a sign-flip matrix on a vector.

theorem HCPolySupport.matVecMul_swap_eq_comp {d : ℕ} (i j : Fin d) (x : Vec d) : matVecMul (Matrix.swap ℝ i j) x = x ∘ ⇑(Equiv.swap i j)

Coordinate formula for the action of a swap matrix on a vector.

theorem HCPolySupport.mem_openCubeSet_originCube_signFlipMatrix_iff {d : ℕ} {m : ℤ} {x : Vec d} (i : Fin d) : matVecMul (signFlipMatrix i) x ∈ openCubeSet (originCube d m) ↔ x ∈ openCubeSet (originCube d m)

The centered open cube (-3^m/2, 3^m/2)^d is invariant under coordinate sign flips.

We record this for openCubeSet; the half-open cubeSet realization is not literally sign-flip invariant on boundary points.

theorem HCPolySupport.mem_openCubeSet_originCube_swap_iff {d : ℕ} {m : ℤ} {x : Vec d} (i j : Fin d) : matVecMul (Matrix.swap ℝ i j) x ∈ openCubeSet (originCube d m) ↔ x ∈ openCubeSet (originCube d m)

The centered open cube (-3^m/2, 3^m/2)^d is invariant under coordinate swaps.