Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.PartitionDerivatives

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

theorem HCPolySupport.norm_fderiv_lowerOverlapArgument_le {d : ℕ} (S : TriadicCube d) (i : Fin d) (x : Vec d) : ‖fderiv ℝ (fun (y : Vec d) => (y i - overlapCoordLower S i) / cubeScaleFactor S) x‖ ≤ (cubeScaleFactor S)⁻¹

theorem HCPolySupport.norm_fderiv_upperOverlapArgument_le {d : ℕ} (S : TriadicCube d) (i : Fin d) (x : Vec d) : ‖fderiv ℝ (fun (y : Vec d) => (overlapCoordUpper S i - y i) / cubeScaleFactor S) x‖ ≤ (cubeScaleFactor S)⁻¹

theorem HCPolySupport.norm_fderiv_lowerOverlapTransition_le {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : ‖fderiv ℝ (lowerOverlapTransition Q S i) x‖ ≤ smoothTransitionProfile.derivBound * (cubeScaleFactor S)⁻¹

theorem HCPolySupport.norm_fderiv_upperOverlapTransition_le {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : ‖fderiv ℝ (upperOverlapTransition Q S i) x‖ ≤ smoothTransitionProfile.derivBound * (cubeScaleFactor S)⁻¹

theorem HCPolySupport.norm_fderiv_overlapTransitionFactor_le {d : ℕ} (Q S : TriadicCube d) (i : Fin d) (x : Vec d) : ‖fderiv ℝ (fun (y : Vec d) => lowerOverlapTransition Q S i y * upperOverlapTransition Q S i y) x‖ ≤ 2 * smoothTransitionProfile.derivBound * (cubeScaleFactor S)⁻¹

theorem HCPolySupport.norm_basisVec {d : ℕ} (i : Fin d) : ‖basisVec i‖ = 1

theorem HCPolySupport.lowerOverlapTransition_eq_one_of_add_scale_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hle : overlapCoordLower S i + cubeScaleFactor S ≤ x i) : lowerOverlapTransition Q S i x = 1

theorem HCPolySupport.upperOverlapTransition_eq_one_of_add_scale_le {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hle : x i + cubeScaleFactor S ≤ overlapCoordUpper S i) : upperOverlapTransition Q S i x = 1

theorem HCPolySupport.lowerOverlapTransition_plateauChildCube_eq_one {d : ℕ} {Q R : TriadicCube d} {x : Vec d} (hxR : x ∈ cubeSet R) (i : Fin d) : lowerOverlapTransition Q (plateauChildCube Q R x) i x = 1

theorem HCPolySupport.upperOverlapTransition_plateauChildCube_eq_one {d : ℕ} {Q R : TriadicCube d} {x : Vec d} (hxR : x ∈ cubeSet R) (i : Fin d) : upperOverlapTransition Q (plateauChildCube Q R x) i x = 1

theorem HCPolySupport.lowerOverlapTransition_ne_zero_coord_lt {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hne : lowerOverlapTransition Q S i x ≠ 0) : overlapCoordLower S i < x i

theorem HCPolySupport.upperOverlapTransition_ne_zero_coord_lt {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (hne : upperOverlapTransition Q S i x ≠ 0) : x i < overlapCoordUpper S i