Documentation

LeanPool.HighContrastHomogenization.Support.Geometry.BoundaryLayer

Coarse-graining support: Support.Geometry.BoundaryLayer #

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

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

The geometric boundary of a half-open cube, encoded as the difference between the half-open realization and its open core.

Equations
Instances For
    source
    def HCPolySupport.cubeShrunkSet {d : ℕ} (Q : TriadicCube d) (t : ℝ) :
    Set (Vec d)

    The cube obtained by shrinking each face inward by the normalized amount t. For t = 0 this recovers the original half-open cube.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def HCPolySupport.cubeBoundaryLayer {d : ℕ} (Q : TriadicCube d) (t : ℝ) :
      Set (Vec d)

      The boundary layer of thickness t, defined as the part of the cube left after removing the shrunk core.

      Equations
      Instances For
        source
        @[simp]
        theorem HCPolySupport.mem_cubeBoundary_iff {d : ℕ} {Q : TriadicCube d} {x : Vec d} :
        x ∈ cubeBoundary Q ↔ x ∈ cubeSet Q ∧ x ∉ openCubeSet Q
        source
        @[simp]
        theorem HCPolySupport.mem_cubeShrunkSet_iff {d : ℕ} {Q : TriadicCube d} {t : ℝ} {x : Vec d} :
        x ∈ cubeShrunkSet Q t ↔ ∀ (i : Fin d), (↑(Q.index i) - 1 / 2 + t) * cubeScaleFactor Q ≤ x i ∧ x i < (↑(Q.index i) + 1 / 2 - t) * cubeScaleFactor Q
        source
        @[simp]
        theorem HCPolySupport.mem_cubeBoundaryLayer_iff {d : ℕ} {Q : TriadicCube d} {t : ℝ} {x : Vec d} :
        x ∈ cubeBoundaryLayer Q t ↔ x ∈ cubeSet Q ∧ x ∉ cubeShrunkSet Q t
        source
        @[simp]
        theorem HCPolySupport.cubeShrunkSet_zero {d : ℕ} (Q : TriadicCube d) :
        cubeShrunkSet Q 0 = cubeSet Q
        source
        @[simp]
        theorem HCPolySupport.cubeBoundaryLayer_zero {d : ℕ} (Q : TriadicCube d) :
        cubeBoundaryLayer Q 0 = ∅
        source
        theorem HCPolySupport.cubeBoundary_subset_cubeSet {d : ℕ} (Q : TriadicCube d) :
        cubeBoundary Q ⊆ cubeSet Q
        source
        theorem HCPolySupport.cubeBoundaryLayer_subset_cubeSet {d : ℕ} (Q : TriadicCube d) (t : ℝ) :
        cubeBoundaryLayer Q t ⊆ cubeSet Q
        source
        theorem HCPolySupport.cubeShrunkSet_anti {d : ℕ} (Q : TriadicCube d) :
        Antitone (cubeShrunkSet Q)
        source
        theorem HCPolySupport.cubeShrunkSet_subset_cubeSet {d : ℕ} (Q : TriadicCube d) {t : ℝ} (ht : 0 ≤ t) :
        cubeShrunkSet Q t ⊆ cubeSet Q
        source
        theorem HCPolySupport.cubeBoundaryLayer_mono {d : ℕ} (Q : TriadicCube d) :
        Monotone (cubeBoundaryLayer Q)
        source
        theorem HCPolySupport.openCubeSet_subset_cubeSet {d : ℕ} (Q : TriadicCube d) :
        openCubeSet Q ⊆ cubeSet Q
        source
        theorem HCPolySupport.pairwiseDisjoint_openCubeSet_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) (n : ℕ) :
        (↑(descendantsAtDepth Q n)).PairwiseDisjoint openCubeSet
        source
        theorem HCPolySupport.openCubeSet_union_cubeBoundary_eq_cubeSet {d : ℕ} (Q : TriadicCube d) :
        openCubeSet Q ∪ cubeBoundary Q = cubeSet Q
        source
        theorem HCPolySupport.cubeShrunkSet_eq_empty_of_half_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {t : ℝ} (ht : 1 / 2 ≤ t) :
        cubeShrunkSet Q t = ∅
        source
        theorem HCPolySupport.cubeBoundaryLayer_eq_cubeSet_of_half_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {t : ℝ} (ht : 1 / 2 ≤ t) :
        cubeBoundaryLayer Q t = cubeSet Q
        source
        theorem HCPolySupport.center_mem_cubeShrunkSet_of_lt_half {d : ℕ} (Q : TriadicCube d) {t : ℝ} (ht : t < 1 / 2) :
        (fun (i : Fin d) => ↑(Q.index i) * cubeScaleFactor Q) ∈ cubeShrunkSet Q t
        source
        theorem HCPolySupport.cubeShrunkSet_nonempty_of_lt_half {d : ℕ} (Q : TriadicCube d) {t : ℝ} (ht : t < 1 / 2) :
        (cubeShrunkSet Q t).Nonempty
        source
        theorem HCPolySupport.cubeShrunkSet_nonempty_iff {d : ℕ} [NeZero d] {Q : TriadicCube d} {t : ℝ} :
        (cubeShrunkSet Q t).Nonempty ↔ t < 1 / 2
        source
        theorem HCPolySupport.cubeShrunkSet_eq_empty_iff {d : ℕ} [NeZero d] {Q : TriadicCube d} {t : ℝ} :
        cubeShrunkSet Q t = ∅ ↔ 1 / 2 ≤ t
        source
        theorem HCPolySupport.cubeSet_middleChild_subset_cubeShrunkSet {d : ℕ} (Q : TriadicCube d) {t : ℝ} (ht : t ≤ 1 / 3) :
        cubeSet { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i } ⊆ cubeShrunkSet Q t
        source
        theorem HCPolySupport.cubeSet_childCube_subset_cubeShrunkSet_of_digits_eq_one {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) (hdigits : ∀ (i : Fin d), digits i = 1) {t : ℝ} (ht : t ≤ 1 / 3) :
        cubeSet { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i + ↑↑(digits i) - 1 } ⊆ cubeShrunkSet Q t
        source
        @[simp]
        theorem HCPolySupport.descendantsAtScale_pred {d : ℕ} (Q : TriadicCube d) :
        descendantsAtScale Q (Q.scale - 1) = childCubes Q
        source
        theorem HCPolySupport.middleChild_mem_childCubes {d : ℕ} (Q : TriadicCube d) :
        { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i } ∈ childCubes Q
        source
        theorem HCPolySupport.middleChild_mem_descendantsAtScale_pred {d : ℕ} (Q : TriadicCube d) :
        { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i } ∈ descendantsAtScale Q (Q.scale - 1)
        source
        theorem HCPolySupport.descendantsAtScale_pred_card {d : ℕ} (Q : TriadicCube d) :
        (descendantsAtScale Q (Q.scale - 1)).card = 3 ^ d
        source
        theorem HCPolySupport.cubeBoundaryLayer_subset_iUnion_childCubes_except_middle {d : ℕ} (Q : TriadicCube d) {t : ℝ} (ht : t ≤ 1 / 3) :
        cubeBoundaryLayer Q t ⊆ ⋃ R ∈ {S : TriadicCube d | S ∈ childCubes Q ∧ S ≠ { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i }}, cubeSet R