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

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

noncomputable def HCPolySupport.rawOverlapWeight {d : ℕ} (Q : TriadicCube d) (j : ℕ) (S : TriadicCube d) (x : Vec d) : ℝ

Raw relative overlap weight before normalization. It is only meant to be used for retained centers; off the retained set it is exactly zero so that later finite sums can range over all cubes without changing values.

Equations

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

theorem HCPolySupport.rawOverlapWeight_zero_of_not_mem {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∉ overlapCentersAtDepth Q j) (x : Vec d) : rawOverlapWeight Q j S x = 0

theorem HCPolySupport.contDiff_rawOverlapWeight {d : ℕ} (Q : TriadicCube d) (j : ℕ) (S : TriadicCube d) : ContDiff ℝ (↑⊤) (rawOverlapWeight Q j S)

theorem HCPolySupport.rawOverlapWeight_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (S : TriadicCube d) (x : Vec d) : 0 ≤ rawOverlapWeight Q j S x

theorem HCPolySupport.rawOverlapWeight_le_one {d : ℕ} (Q : TriadicCube d) (j : ℕ) (S : TriadicCube d) (x : Vec d) : rawOverlapWeight Q j S x ≤ 1

theorem HCPolySupport.rawOverlapWeight_support_subset {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hne : rawOverlapWeight Q j S x ≠ 0) : x ∈ openOverlapCubeSet S

theorem HCPolySupport.rawOverlapWeight_support_subset_overlapCubeSet {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hne : rawOverlapWeight Q j S x ≠ 0) : x ∈ overlapCubeSet S

theorem HCPolySupport.rawOverlapWeight_eq_zero_of_not_mem_overlapCubeSet {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hxS : x ∉ overlapCubeSet S) : rawOverlapWeight Q j S x = 0

theorem HCPolySupport.exists_coord_le_or_upper_le_of_not_mem_overlapCubeSet {d : ℕ} {S : TriadicCube d} {x : Vec d} (hxS : x ∉ overlapCubeSet S) : ∃ (i : Fin d), x i ≤ overlapCoordLower S i ∨ overlapCoordUpper S i ≤ x i

theorem HCPolySupport.rawOverlapWeight_fderiv_eq_zero_of_not_mem_overlapCubeSet {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hxS : x ∉ overlapCubeSet S) : fderiv ℝ (rawOverlapWeight Q j S) x = 0

theorem HCPolySupport.norm_fderiv_rawOverlapWeight_le {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) : ‖fderiv ℝ (rawOverlapWeight Q j S) x‖ ≤ ↑(Fintype.card (Fin d)) * (2 * smoothTransitionProfile.derivBound * (cubeScaleFactor S)⁻¹)

theorem HCPolySupport.abs_rawOverlapWeight_coordDeriv_le {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (i : Fin d) (hS : S ∈ overlapCentersAtDepth Q j) : |euclideanCoordDeriv i (rawOverlapWeight Q j S) x| ≤ ↑(Fintype.card (Fin d)) * (2 * smoothTransitionProfile.derivBound * (cubeScaleFactor S)⁻¹)

theorem HCPolySupport.abs_rawOverlapWeight_coordDeriv_le_depthScale {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (i : Fin d) (hS : S ∈ overlapCentersAtDepth Q j) : |euclideanCoordDeriv i (rawOverlapWeight Q j S) x| ≤ ↑(Fintype.card (Fin d)) * (2 * smoothTransitionProfile.derivBound * (3 * (cubeScaleFactor Q / 3 ^ j)⁻¹))

theorem HCPolySupport.rawOverlapWeight_coordDeriv_eq_zero_of_not_mem_overlapCubeSet {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (i : Fin d) (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hxS : x ∉ overlapCubeSet S) : euclideanCoordDeriv i (rawOverlapWeight Q j S) x = 0

theorem HCPolySupport.lowerOverlapTransition_pos_of_mem_openOverlap {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxS : x ∈ openOverlapCubeSet S) : 0 < lowerOverlapTransition Q S i x

theorem HCPolySupport.upperOverlapTransition_pos_of_mem_openOverlap {d : ℕ} {Q S : TriadicCube d} {i : Fin d} {x : Vec d} (hxS : x ∈ openOverlapCubeSet S) : 0 < upperOverlapTransition Q S i x

theorem HCPolySupport.rawOverlapWeight_pos_of_mem_openOverlap {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hxS : x ∈ openOverlapCubeSet S) : 0 < rawOverlapWeight Q j S x

theorem HCPolySupport.rawOverlapWeight_plateauChildCube_eq_one {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {x : Vec d} (hR : R ∈ descendantsAtDepth Q j) (hxR : x ∈ cubeSet R) : rawOverlapWeight Q j (plateauChildCube Q R x) x = 1

noncomputable def HCPolySupport.rawOverlapWeightDenom {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) : ℝ

Denominator of the normalized overlap partition planned for Stage 7.

Equations

• HCPolySupport.rawOverlapWeightDenom Q j x = ∑ S ∈ HCPolySupport.overlapCentersAtDepth Q j, HCPolySupport.rawOverlapWeight Q j S x

theorem HCPolySupport.rawOverlapWeightDenom_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) : 0 ≤ rawOverlapWeightDenom Q j x

theorem HCPolySupport.contDiff_rawOverlapWeightDenom {d : ℕ} (Q : TriadicCube d) (j : ℕ) : ContDiff ℝ (↑⊤) (rawOverlapWeightDenom Q j)

theorem HCPolySupport.rawOverlapWeightDenom_coordDeriv_eq_sum {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) (i : Fin d) : euclideanCoordDeriv i (rawOverlapWeightDenom Q j) x = ∑ S ∈ overlapCentersAtDepth Q j, euclideanCoordDeriv i (rawOverlapWeight Q j S) x

theorem HCPolySupport.abs_rawOverlapWeightDenom_coordDeriv_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (i : Fin d) : |euclideanCoordDeriv i (rawOverlapWeightDenom Q j) x| ≤ 3 ^ d * (↑(Fintype.card (Fin d)) * (2 * smoothTransitionProfile.derivBound * (3 * (cubeScaleFactor Q / 3 ^ j)⁻¹)))

theorem HCPolySupport.rawOverlapWeightDenom_pos_of_exists_openOverlap {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hcover : ∃ S ∈ overlapCentersAtDepth Q j, x ∈ openOverlapCubeSet S) : 0 < rawOverlapWeightDenom Q j x

theorem HCPolySupport.one_le_rawOverlapWeightDenom_of_mem_openCubeSet {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) : 1 ≤ rawOverlapWeightDenom Q j x

theorem HCPolySupport.rawOverlapWeightDenom_pos_of_mem_openCubeSet {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) : 0 < rawOverlapWeightDenom Q j x

noncomputable def HCPolySupport.overlapWeightDenomSafe {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) : ℝ

A globally positive smooth normalization denominator agreeing with the raw weight sum on the open parent cube.

Equations

• HCPolySupport.overlapWeightDenomSafe Q j x = HCPolySupport.rawOverlapWeightDenom Q j x + HCPolySupport.smoothTransitionProfile (1 - HCPolySupport.rawOverlapWeightDenom Q j x)

theorem HCPolySupport.overlapWeightDenomSafe_eq_raw_of_mem_openCubeSet {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) : overlapWeightDenomSafe Q j x = rawOverlapWeightDenom Q j x

theorem HCPolySupport.overlapWeightDenomSafe_pos {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) : 0 < overlapWeightDenomSafe Q j x

theorem HCPolySupport.contDiff_overlapWeightDenomSafe {d : ℕ} (Q : TriadicCube d) (j : ℕ) : ContDiff ℝ (↑⊤) (overlapWeightDenomSafe Q j)

theorem HCPolySupport.overlapWeightDenomSafe_coordDeriv_eq_raw_of_mem_openCubeSet {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (i : Fin d) : euclideanCoordDeriv i (overlapWeightDenomSafe Q j) x = euclideanCoordDeriv i (rawOverlapWeightDenom Q j) x

theorem HCPolySupport.abs_inv_overlapWeightDenomSafe_coordDeriv_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (i : Fin d) : |euclideanCoordDeriv i (fun (y : Vec d) => (overlapWeightDenomSafe Q j y)⁻¹) x| ≤ |euclideanCoordDeriv i (rawOverlapWeightDenom Q j) x|

noncomputable def HCPolySupport.overlapPartitionWeight {d : ℕ} (Q : TriadicCube d) (j : ℕ) (S : TriadicCube d) (x : Vec d) : ℝ

The raw overlap cutoff divided by the safe denominator to form a smooth relative partition weight.

Equations

• HCPolySupport.overlapPartitionWeight Q j S x = HCPolySupport.rawOverlapWeight Q j S x / HCPolySupport.overlapWeightDenomSafe Q j x

theorem HCPolySupport.contDiff_overlapPartitionWeight {d : ℕ} (Q S : TriadicCube d) (j : ℕ) : ContDiff ℝ (↑⊤) (overlapPartitionWeight Q j S)

theorem HCPolySupport.contDiffOn_overlapPartitionWeight_openCubeSet {d : ℕ} (Q S : TriadicCube d) (j : ℕ) : ContDiffOn ℝ 1 (overlapPartitionWeight Q j S) (openCubeSet Q)

theorem HCPolySupport.overlapPartitionWeight_coordDeriv_eq {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (i : Fin d) : euclideanCoordDeriv i (overlapPartitionWeight Q j S) x = rawOverlapWeight Q j S x * euclideanCoordDeriv i (fun (y : Vec d) => (overlapWeightDenomSafe Q j y)⁻¹) x + (overlapWeightDenomSafe Q j x)⁻¹ * euclideanCoordDeriv i (rawOverlapWeight Q j S) x

theorem HCPolySupport.abs_overlapPartitionWeight_coordDeriv_le {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (i : Fin d) (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) : |euclideanCoordDeriv i (overlapPartitionWeight Q j S) x| ≤ ↑(Fintype.card (Fin d)) * (2 * smoothTransitionProfile.derivBound * (3 * (cubeScaleFactor Q / 3 ^ j)⁻¹)) + 3 ^ d * (↑(Fintype.card (Fin d)) * (2 * smoothTransitionProfile.derivBound * (3 * (cubeScaleFactor Q / 3 ^ j)⁻¹)))

noncomputable def HCPolySupport.smoothOverlapPartitionDerivativeConstant (d : ℕ) : ℝ

The dimension-dependent derivative factor for overlap partition weights after division by the depth scale.

Equations

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

theorem HCPolySupport.smoothOverlapPartitionDerivativeConstant_nonneg (d : ℕ) : 0 ≤ smoothOverlapPartitionDerivativeConstant d

theorem HCPolySupport.abs_overlapPartitionWeight_coordDeriv_le_depthScale {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (i : Fin d) (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) : |euclideanCoordDeriv i (overlapPartitionWeight Q j S) x| ≤ smoothOverlapPartitionDerivativeConstant d / (cubeScaleFactor Q / 3 ^ j)

theorem HCPolySupport.overlapPartitionWeight_nonneg_of_mem_openCubeSet {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (_hxQ : x ∈ openCubeSet Q) : 0 ≤ overlapPartitionWeight Q j S x

theorem HCPolySupport.overlapPartitionWeight_zero_of_not_mem {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∉ overlapCentersAtDepth Q j) (x : Vec d) : overlapPartitionWeight Q j S x = 0

theorem HCPolySupport.overlapPartitionWeight_support_subset {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hne : overlapPartitionWeight Q j S x ≠ 0) : x ∈ openOverlapCubeSet S

theorem HCPolySupport.overlapPartitionWeight_fderiv_eq_zero_of_not_mem_overlapCubeSet {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hxS : x ∉ overlapCubeSet S) : fderiv ℝ (overlapPartitionWeight Q j S) x = 0

theorem HCPolySupport.overlapPartitionWeight_coordDeriv_zero_of_not_mem_overlap {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} (i : Fin d) (hS : S ∈ overlapCentersAtDepth Q j) (hxQ : x ∈ openCubeSet Q) (hxS : x ∉ overlapCubeSet S) : euclideanCoordDeriv i (overlapPartitionWeight Q j S) x = 0

theorem HCPolySupport.overlapPartitionWeight_sum_eq_one {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) : ∑ S ∈ overlapCentersAtDepth Q j, overlapPartitionWeight Q j S x = 1

theorem HCPolySupport.overlapPartitionWeight_coordDeriv_sum_eq_zero {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) (i : Fin d) : ∑ S ∈ overlapCentersAtDepth Q j, euclideanCoordDeriv i (overlapPartitionWeight Q j S) x = 0

theorem HCPolySupport.rawOverlapWeight_active_card_bound {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) : {S ∈ overlapCentersAtDepth Q j | rawOverlapWeight Q j S x ≠ 0}.card ≤ 3 ^ d

theorem HCPolySupport.overlapPartitionWeight_active_card_bound {d : ℕ} {Q : TriadicCube d} {j : ℕ} {x : Vec d} (hxQ : x ∈ openCubeSet Q) : {S ∈ overlapCentersAtDepth Q j | overlapPartitionWeight Q j S x ≠ 0}.card ≤ 3 ^ d