Coarse-graining support: Support.Geometry.OriginCubeBoundaryPush

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

theorem HCPolySupport.isOpen_openCubeSet {d : ℕ} (Q : TriadicCube d) : IsOpen (openCubeSet Q)

The open realization of a triadic cube is open in \R^d.

theorem HCPolySupport.IsCompact.exists_pos_forall_uniformTranslate_subset_openCubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} {K : Set (Vec d)} (hK : IsCompact K) (hKsub : K ⊆ cubeSet (originCube d n)) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ {ε : ℝ}, 0 < ε → ε < ε₀ → (fun (x : Vec d) => x + fun (x : Fin d) => ε) '' K ⊆ openCubeSet (originCube d n)

If a compact set K is contained in the half-open centered cube \square_n, then every sufficiently small positive diagonal translation pushes K into the open centered cube.

This is the geometric input behind later boundary-pushing arguments for smooth test functions on cubeSet (originCube d n).

theorem HCPolySupport.IsCompact.exists_pos_uniformTranslate_subset_openCubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} {K : Set (Vec d)} (hK : IsCompact K) (hKsub : K ⊆ cubeSet (originCube d n)) : ∃ (ε : ℝ), 0 < ε ∧ (fun (x : Vec d) => x + fun (x : Fin d) => ε) '' K ⊆ openCubeSet (originCube d n)

If a compact set K is contained in the half-open centered cube \square_n, then some positive diagonal translation pushes K into the open centered cube.

theorem HCPolySupport.HasCompactSupport.exists_pos_forall_precomp_subRight_tsupport_subset_openCubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (hφsub : tsupport φ ⊆ cubeSet (originCube d n)) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ {ε : ℝ}, 0 < ε → ε < ε₀ → (tsupport fun (x : Vec d) => φ (x - fun (x : Fin d) => ε)) ⊆ openCubeSet (originCube d n)

If a smooth test has compact support in the half-open centered cube, then every sufficiently small positive precomposition by a negative diagonal translation pushes its support into the open centered cube.

theorem HCPolySupport.HasCompactSupport.exists_pos_precomp_subRight_tsupport_subset_openCubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} {φ : Vec d → ℝ} (hφ : HasCompactSupport φ) (hφsub : tsupport φ ⊆ cubeSet (originCube d n)) : ∃ (ε : ℝ), 0 < ε ∧ (tsupport fun (x : Vec d) => φ (x - fun (x : Fin d) => ε)) ⊆ openCubeSet (originCube d n)

If a smooth test has compact support in the half-open centered cube, then after precomposing with a small negative diagonal translation, its support lies in the open centered cube.