Carrier coordinates for affine barycentric subdivision

The coordinates of one barycentric-subdivision simplex are monotone in the ordering permutation. More precisely, if z = affineSubdivMap n pi x, then

z (pi r) = sum_{k >= r} x k / (k+1).

Consequently every source coefficient is recovered from a consecutive coordinate drop. A positive source coefficient gives a strict cut in the ordered coordinates, so the corresponding prefix face is determined by the image point itself. These are the algebraic carrier facts used to prove that piecewise-affine interpolation agrees on overlapping barycentric-subdivision simplices.

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_apply_perm (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (k r : Fin (n + 1)) : (prefixBarycenter n pi k) (pi r) = if ↑r ≤ ↑k then (↑↑k + 1)⁻¹ else 0

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_apply_perm (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r : Fin (n + 1)) : (affineSubdivMap n pi x) (pi r) = ∑ k : Fin (n + 1), if ↑r ≤ ↑k then x k * (↑↑k + 1)⁻¹ else 0

Ordered-coordinate formula for one affine barycentric-subdivision chart.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_perm_antitone (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) {r s : Fin (n + 1)} (hrs : r ≤ s) : (affineSubdivMap n pi x) (pi s) ≤ (affineSubdivMap n pi x) (pi r)

Coordinates of a barycentric-subdivision image are nonincreasing in the permutation order.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_perm_drop (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r : Fin n) : (affineSubdivMap n pi x) (pi r.castSucc) - (affineSubdivMap n pi x) (pi r.succ) = x r.castSucc * (↑↑r + 1)⁻¹

A consecutive ordered-coordinate drop recovers the corresponding source coefficient.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_perm_last (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) : (affineSubdivMap n pi x) (pi (Fin.last n)) = x (Fin.last n) * (↑n + 1)⁻¹

The final ordered coordinate recovers the final source coefficient.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_perm_strict_drop (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r : Fin n) (hr : 0 < x r.castSucc) : (affineSubdivMap n pi x) (pi r.succ) < (affineSubdivMap n pi x) (pi r.castSucc)

A positive nonfinal source coefficient produces a strict coordinate cut.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_perm_last_pos (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (hr : 0 < x (Fin.last n)) : 0 < (affineSubdivMap n pi x) (pi (Fin.last n))

A positive final source coefficient makes the final ordered coordinate positive.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_perm_lt_of_cut (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r : Fin n) (hr : 0 < x r.castSucc) (s : Fin (n + 1)) (hrs : r.castSucc < s) : (affineSubdivMap n pi x) (pi s) < (affineSubdivMap n pi x) (pi r.castSucc)

Every coordinate strictly after a positive cut is below the coordinate at that cut.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_perm_ge_of_le (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r s : Fin (n + 1)) (hsr : s ≤ r) : (affineSubdivMap n pi x) (pi r) ≤ (affineSubdivMap n pi x) (pi s)

Every coordinate weakly before a cut is at least the coordinate at that cut.

def SphereOddDegree.AffineBarycentricSubdivision.prefixSet (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (r : Fin (n + 1)) : Finset (Fin (n + 1))

The underlying vertex set of the r-th prefix face.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.prefixSet n pi r = Finset.image (⇑pi) (Finset.Iic r)

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.mem_prefixSet (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (r j : Fin (n + 1)) : j ∈ prefixSet n pi r ↔ (Equiv.symm pi) j ≤ r

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.card_prefixSet (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (r : Fin (n + 1)) : (prefixSet n pi r).card = ↑r + 1

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_apply (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (r j : Fin (n + 1)) : (prefixBarycenter n pi r) j = if j ∈ prefixSet n pi r then (↑↑r + 1)⁻¹ else 0

Coordinate formula for a prefix barycenter at an arbitrary ambient vertex.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_ge_cut_of_mem_prefix (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r j : Fin (n + 1)) (hj : j ∈ prefixSet n pi r) : (affineSubdivMap n pi x) (pi r) ≤ (affineSubdivMap n pi x) j

At a positive cut, every vertex in the prefix has coordinate at least the cut coordinate.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_lt_cut_of_not_mem_prefix (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r j : Fin (n + 1)) (hr : 0 < x r) (hj : j ∉ prefixSet n pi r) : (affineSubdivMap n pi x) j < (affineSubdivMap n pi x) (pi r)

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixSet_eq_of_affineSubdivMap_eq_of_pos (n : ℕ) (pi sigma : Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : affineSubdivMap n pi x = affineSubdivMap n sigma y) (r : Fin (n + 1)) (hr : 0 < x r) : prefixSet n pi r = prefixSet n sigma r

A positive coefficient determines its prefix face from the image point. Hence two barycentric-subdivision charts representing the same point have the same active prefix.

theorem SphereOddDegree.AffineBarycentricSubdivision.prefixBarycenter_eq_of_affineSubdivMap_eq_of_pos (n : ℕ) (pi sigma : Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : affineSubdivMap n pi x = affineSubdivMap n sigma y) (r : Fin (n + 1)) (hr : 0 < x r) : prefixBarycenter n pi r = prefixBarycenter n sigma r

Equality of image points identifies every active barycentric-subdivision vertex.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_cut_coordinate_eq_of_pos (n : ℕ) (pi sigma : Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : affineSubdivMap n pi x = affineSubdivMap n sigma y) (r : Fin (n + 1)) (hr : 0 < x r) : (affineSubdivMap n pi x) (pi r) = (affineSubdivMap n sigma y) (sigma r)

The ordered coordinate at an active cut is independent of the sorting permutation.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_next_coordinate_eq_of_pos (n : ℕ) (pi sigma : Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : affineSubdivMap n pi x = affineSubdivMap n sigma y) (r : Fin n) (hr : 0 < x r.castSucc) : (affineSubdivMap n pi x) (pi r.succ) = (affineSubdivMap n sigma y) (sigma r.succ)

The first coordinate after an active nonfinal cut is also permutation-independent.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_active_coefficient_eq (n : ℕ) (pi sigma : Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : affineSubdivMap n pi x = affineSubdivMap n sigma y) (r : Fin (n + 1)) (hr : 0 < x r) : y r = x r

Every active source coefficient is independent of the chart representing the image point.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdiv_vertexInterpolation_eq_of_map_eq {E : Type u_1} [AddCommMonoid E] [Module ℝ E] (n : ℕ) (pi sigma : Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : affineSubdivMap n pi x = affineSubdivMap n sigma y) (V : ↑(Delta n) → E) : ∑ r : Fin (n + 1), x r • V (prefixBarycenter n pi r) = ∑ r : Fin (n + 1), y r • V (prefixBarycenter n sigma r)

One-step affine interpolation of arbitrary globally assigned vertex values agrees on overlap.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_cut_pos (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r : Fin (n + 1)) (hr : 0 < x r) : 0 < (affineSubdivMap n pi x) (pi r)

A positive source coefficient makes the image coordinate at its cut positive.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap_pos_of_mem_prefix (n : ℕ) (pi : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r j : Fin (n + 1)) (hr : 0 < x r) (hj : j ∈ prefixSet n pi r) : 0 < (affineSubdivMap n pi x) j

Every vertex in the prefix of a positive cut has positive image coordinate.

theorem SphereOddDegree.AffineBarycentricSubdivision.delta_val_eq_sum_smul_stdVerts (n : ℕ) (z : ↑(Delta n)) : ↑z = ∑ i : Fin (n + 1), z i • BarycentricSubdivisionDiameter.stdVerts n i

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_eq_of_vertex_eq_on_support (n N : ℕ) (rho sigma : Fin N → Equiv.Perm (Fin (n + 1))) (z : ↑(Delta n)) (hvertex : ∀ (i : Fin (n + 1)), z i ≠ 0 → (affineCompMap n N rho) (FiniteSimplex.vertex i) = (affineCompMap n N sigma) (FiniteSimplex.vertex i)) : (affineCompMap n N rho) z = (affineCompMap n N sigma) z

Two iterated affine charts agree at a point if they agree at every active standard vertex.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_active_vertex_and_coefficient_eq (n N : ℕ) (rho sigma : Fin N → Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : (affineCompMap n N rho) x = (affineCompMap n N sigma) y) (r : Fin (n + 1)) (hr : 0 < x r) : (affineCompMap n N rho) (FiniteSimplex.vertex r) = (affineCompMap n N sigma) (FiniteSimplex.vertex r) ∧ y r = x r

Carrier theorem for iterated barycentric subdivision of one standard simplex.

If two iterated top-simplex charts represent the same point, every active source coefficient is identical and the corresponding represented subdivision vertex is the same geometric point.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineComp_vertexInterpolation_eq_of_map_eq {E : Type u_1} [AddCommMonoid E] [Module ℝ E] (n N : ℕ) (rho sigma : Fin N → Equiv.Perm (Fin (n + 1))) (x y : ↑(Delta n)) (hxy : (affineCompMap n N rho) x = (affineCompMap n N sigma) y) (V : ↑(Delta n) → E) : ∑ r : Fin (n + 1), x r • V ((affineCompMap n N rho) (FiniteSimplex.vertex r)) = ∑ r : Fin (n + 1), y r • V ((affineCompMap n N sigma) (FiniteSimplex.vertex r))

Iterated affine interpolation of arbitrary globally assigned subdivision-vertex values agrees on every overlap of iterated barycentric-subdivision top simplices.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_coordinate_eq_sum_vertices (n N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (j : Fin (n + 1)) : ((affineCompMap n N rho) x) j = ∑ r : Fin (n + 1), x r * ((affineCompMap n N rho) (FiniteSimplex.vertex r)) j

Coordinatewise barycentric formula for an iterated affine chart.

theorem SphereOddDegree.AffineBarycentricSubdivision.affineCompMap_vertex_support_subset (n N : ℕ) (rho : Fin N → Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) (r j : Fin (n + 1)) (hr : 0 < x r) (hj : 0 < ((affineCompMap n N rho) (FiniteSimplex.vertex r)) j) : 0 < ((affineCompMap n N rho) x) j

The support of an active represented subdivision vertex is contained in the support of the represented point.