Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.PartitionGeometry

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

Raw one-sided overlap weights

These are the planned Stage-7 building blocks for the uniform smooth overlap partition. Interior coordinates use a two-sided smooth transition across the outer collar of an overlap cube. If an overlap face coincides with a parent face, the corresponding one-sided transition is suppressed; this keeps the raw weight uniformly positive near ∂Q when we work relative to openCubeSet Q.

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

The lower coordinate endpoint of a triadic cube, used to describe its faces and membership.

Equations

• HCPolySupport.cubeCoordLower Q i = (↑(Q.index i) - 1 / 2) * HCPolySupport.cubeScaleFactor Q

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

The upper coordinate endpoint of a triadic cube, used to describe its faces and membership.

Equations

• HCPolySupport.cubeCoordUpper Q i = (↑(Q.index i) + 1 / 2) * HCPolySupport.cubeScaleFactor Q

noncomputable def HCPolySupport.overlapCoordLower {d : ℕ} (S : TriadicCube d) (i : Fin d) : ℝ

The lower coordinate endpoint of the overlap cube centered at S.

Equations

• HCPolySupport.overlapCoordLower S i = (↑(S.index i) - 3 / 2) * HCPolySupport.cubeScaleFactor S

noncomputable def HCPolySupport.overlapCoordUpper {d : ℕ} (S : TriadicCube d) (i : Fin d) : ℝ

The upper coordinate endpoint of the overlap cube centered at S.

Equations

• HCPolySupport.overlapCoordUpper S i = (↑(S.index i) + 3 / 2) * HCPolySupport.cubeScaleFactor S

theorem HCPolySupport.mem_openCubeSet_iff_coord_bounds {d : ℕ} {Q : TriadicCube d} {x : Vec d} : x ∈ openCubeSet Q ↔ ∀ (i : Fin d), cubeCoordLower Q i < x i ∧ x i < cubeCoordUpper Q i

theorem HCPolySupport.mem_cubeSet_iff_coord_bounds {d : ℕ} {Q : TriadicCube d} {x : Vec d} : x ∈ cubeSet Q ↔ ∀ (i : Fin d), cubeCoordLower Q i ≤ x i ∧ x i < cubeCoordUpper Q i

theorem HCPolySupport.mem_openOverlapCubeSet_iff_coord_bounds {d : ℕ} {S : TriadicCube d} {x : Vec d} : x ∈ openOverlapCubeSet S ↔ ∀ (i : Fin d), overlapCoordLower S i < x i ∧ x i < overlapCoordUpper S i

theorem HCPolySupport.mem_overlapCubeSet_iff_coord_bounds {d : ℕ} {S : TriadicCube d} {x : Vec d} : x ∈ overlapCubeSet S ↔ ∀ (i : Fin d), overlapCoordLower S i ≤ x i ∧ x i < overlapCoordUpper S i

theorem HCPolySupport.cubeScaleFactor_pos' {d : ℕ} (Q : TriadicCube d) : 0 < cubeScaleFactor Q

theorem HCPolySupport.cubeCoordUpper_eq_lower_add_scale {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeCoordUpper Q i = cubeCoordLower Q i + cubeScaleFactor Q

theorem HCPolySupport.cubeCoordLower_child {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) (i : Fin d) : cubeCoordLower { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 } i = cubeCoordLower Q i + ↑↑↑(digits i) * cubeScaleFactor { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 }

theorem HCPolySupport.cubeCoordUpper_child {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) (i : Fin d) : cubeCoordUpper { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 } i = cubeCoordUpper Q i - (↑2 - ↑↑↑(digits i)) * cubeScaleFactor { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 }

theorem HCPolySupport.cubeScaleFactor_child_eq_three_mul {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) : cubeScaleFactor Q = 3 * cubeScaleFactor { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 }

theorem HCPolySupport.overlapCoordLower_child {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) (i : Fin d) : overlapCoordLower { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 } i = cubeCoordLower Q i + (↑↑↑(digits i) - 1) * cubeScaleFactor { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 }

theorem HCPolySupport.overlapCoordUpper_child {d : ℕ} (Q : TriadicCube d) (digits : Fin d → Fin 3) (i : Fin d) : overlapCoordUpper { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 } i = cubeCoordUpper Q i + (↑↑↑(digits i) - 1) * cubeScaleFactor { scale := Q.scale - 1, index := fun (k : Fin d) => 3 * Q.index k + ↑↑(digits k) - 1 }

theorem HCPolySupport.cubeCoordLower_descendant_eq_or_one_scale_le {d n : ℕ} {Q R : TriadicCube d} : R ∈ descendantsAtDepth Q n → ∀ (i : Fin d), cubeCoordLower R i = cubeCoordLower Q i ∨ cubeCoordLower Q i + cubeScaleFactor R ≤ cubeCoordLower R i

theorem HCPolySupport.cubeCoordUpper_descendant_eq_or_one_scale_le {d n : ℕ} {Q R : TriadicCube d} : R ∈ descendantsAtDepth Q n → ∀ (i : Fin d), cubeCoordUpper R i = cubeCoordUpper Q i ∨ cubeCoordUpper R i + cubeScaleFactor R ≤ cubeCoordUpper Q i

theorem HCPolySupport.cubeCoordLower_le_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {n : ℕ} (hR : R ∈ descendantsAtDepth Q n) (i : Fin d) : cubeCoordLower Q i ≤ cubeCoordLower R i

theorem HCPolySupport.cubeCoordUpper_le_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {n : ℕ} (hR : R ∈ descendantsAtDepth Q n) (i : Fin d) : cubeCoordUpper R i ≤ cubeCoordUpper Q i

theorem HCPolySupport.overlapCubeSet_child_subset_cubeSet_of_digit_safe {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (digits : Fin d → Fin 3) (hlo_safe : ∀ (i : Fin d), ↑(digits i) = 0 → cubeCoordLower Q i + cubeScaleFactor R ≤ cubeCoordLower R i) (hhi_safe : ∀ (i : Fin d), ↑(digits i) = 2 → cubeCoordUpper R i + cubeScaleFactor R ≤ cubeCoordUpper Q i) : overlapCubeSet { scale := R.scale - 1, index := fun (k : Fin d) => 3 * R.index k + ↑↑(digits k) - 1 } ⊆ cubeSet Q

noncomputable def HCPolySupport.plateauChildDigit {d : ℕ} (Q R : TriadicCube d) (x : Vec d) (i : Fin d) : Fin 3

The child digit used to obtain an overlap weight equal to one at x, choosing the middle digit near parent faces.

Equations

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

theorem HCPolySupport.plateauChildDigit_zero_safe {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {x : Vec d} {i : Fin d} (hR : R ∈ descendantsAtDepth Q j) (hzero : ↑(plateauChildDigit Q R x i) = 0) : cubeCoordLower Q i + cubeScaleFactor R ≤ cubeCoordLower R i

theorem HCPolySupport.plateauChildDigit_two_safe {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {x : Vec d} {i : Fin d} (hR : R ∈ descendantsAtDepth Q j) (htwo : ↑(plateauChildDigit Q R x i) = 2) : cubeCoordUpper R i + cubeScaleFactor R ≤ cubeCoordUpper Q i

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

The child of R selected by the plateau digits to provide a unit raw overlap weight for points of R.

Equations

• HCPolySupport.plateauChildCube Q R x = { scale := R.scale - 1, index := fun (i : Fin d) => 3 * R.index i + ↑↑(HCPolySupport.plateauChildDigit Q R x i) - 1 }

theorem HCPolySupport.plateauChildCube_mem_childCubes {d : ℕ} (Q R : TriadicCube d) (x : Vec d) : plateauChildCube Q R x ∈ childCubes R

theorem HCPolySupport.plateauChildCube_mem_overlapCentersAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {x : Vec d} (hR : R ∈ descendantsAtDepth Q j) : plateauChildCube Q R x ∈ overlapCentersAtDepth Q j

theorem HCPolySupport.contDiff_lowerOverlapArgument {d : ℕ} (S : TriadicCube d) (i : Fin d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => (x i - overlapCoordLower S i) / cubeScaleFactor S

theorem HCPolySupport.contDiff_upperOverlapArgument {d : ℕ} (S : TriadicCube d) (i : Fin d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => (overlapCoordUpper S i - x i) / cubeScaleFactor S

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

Smooth cutoff from the lower overlap face, set to one when that face reaches or lies beyond the lower parent face.

Equations

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

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

Smooth cutoff from the upper overlap face, set to one when that face reaches or lies beyond the upper parent face.

Equations

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

theorem HCPolySupport.contDiff_lowerOverlapTransition {d : ℕ} (Q S : TriadicCube d) (i : Fin d) : ContDiff ℝ (↑⊤) (lowerOverlapTransition Q S i)

theorem HCPolySupport.contDiff_upperOverlapTransition {d : ℕ} (Q S : TriadicCube d) (i : Fin d) : ContDiff ℝ (↑⊤) (upperOverlapTransition Q S i)

theorem HCPolySupport.lowerOverlapTransition_nonneg {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : 0 ≤ lowerOverlapTransition Q S i x

theorem HCPolySupport.upperOverlapTransition_nonneg {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : 0 ≤ upperOverlapTransition Q S i x

theorem HCPolySupport.lowerOverlapTransition_le_one {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : lowerOverlapTransition Q S i x ≤ 1

theorem HCPolySupport.upperOverlapTransition_le_one {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : upperOverlapTransition Q S i x ≤ 1

theorem HCPolySupport.fderiv_lowerOverlapTransition_eq_zero_of_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hx : x i ≤ overlapCoordLower S i) : fderiv ℝ (lowerOverlapTransition Q S i) x = 0

theorem HCPolySupport.fderiv_upperOverlapTransition_eq_zero_of_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hx : overlapCoordUpper S i ≤ x i) : fderiv ℝ (upperOverlapTransition Q S i) x = 0

theorem HCPolySupport.lowerOverlapTransition_eq_zero_of_mem_openCubeSet_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hx : x i ≤ overlapCoordLower S i) : lowerOverlapTransition Q S i x = 0

theorem HCPolySupport.upperOverlapTransition_eq_zero_of_mem_openCubeSet_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hx : overlapCoordUpper S i ≤ x i) : upperOverlapTransition Q S i x = 0

theorem HCPolySupport.overlapTransitionFactor_eq_zero_of_lower_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hx : x i ≤ overlapCoordLower S i) : lowerOverlapTransition Q S i x * upperOverlapTransition Q S i x = 0

theorem HCPolySupport.overlapTransitionFactor_eq_zero_of_upper_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hx : overlapCoordUpper S i ≤ x i) : lowerOverlapTransition Q S i x * upperOverlapTransition Q S i x = 0

theorem HCPolySupport.overlapTransitionFactor_nonneg {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : 0 ≤ lowerOverlapTransition Q S i x * upperOverlapTransition Q S i x

theorem HCPolySupport.overlapTransitionFactor_le_one {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : lowerOverlapTransition Q S i x * upperOverlapTransition Q S i x ≤ 1

theorem HCPolySupport.fderiv_overlapTransitionFactor_eq_zero_of_lower_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hx : x i ≤ overlapCoordLower S i) : fderiv ℝ (fun (y : Vec d) => lowerOverlapTransition Q S i y * upperOverlapTransition Q S i y) x = 0

theorem HCPolySupport.fderiv_overlapTransitionFactor_eq_zero_of_upper_coord_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hx : overlapCoordUpper S i ≤ x i) : fderiv ℝ (fun (y : Vec d) => lowerOverlapTransition Q S i y * upperOverlapTransition Q S i y) x = 0