KuhnFaceAlignment

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Equal-scale face alignment for Kuhn cells

"A face-alignment lemma for equal-scale adjacent cubes, together with the nested-refinement lemma, supplies the complete-face compatibility actually used."

and the gluing step it exists for.

What is proved

• closedCarrier_eq_convexHull_vertexSet -- a closed Kuhn cell is the convex hull of its d + 1 labelled corners. This resolves the second of the two identities queued as a disclosure by KuhnCell.vertex (Whitney/KuhnCells.lean). Still open, and still used nowhere: the first queued identity vertexSet = extremePoints ℝ closedCarrier, and the separate item affineSpan ℝ vertexSet = ⊤ queued by the uniqueness scope note of KuhnInterpolation.lean.
• closedCarrier_inter_subset_commonClosedFace -- the face-alignment lemma. Two Kuhn cells of the same scale on the globally aligned triadic grid meet only inside the convex hull of the vertices they share. No adjacency, face-compatibility or simplicial-complex hypothesis is assumed: the conclusion is proved for an arbitrary pair of equal-scale cells, whether they sit on the same support cube, on neighbouring cubes, or on cubes that do not meet at all.
• kuhnInterp_eqOn_closedCarrier_inter and kuhnInterpAffine_eqOn_closedCarrier_inter -- the gluing step. Two equal-scale cells interpolating one global vertex datum agree at every point of the intersection of their closed carriers. Combined with the proved refinement statements this is the well-definedness input for the global piecewise-affine ℓ̂_p of l.piecewise.affine.approx.
• isClosed_closedCarrier -- a by-product of the convex-hull description, recorded because the gluing consumer needs it to patch continuity.

Scope: exactly what is and is not claimed

The cross-scale direction is deliberately not stated in face form: the only cross-scale facts are the proved containments (a fine cell lies inside a coarse cell), which is all needs and all that is true.

The equal-scale hypothesis is not cosmetic. It is what makes the two support cubes members of one aligned grid, so that at any common point their indices differ by at most one in each coordinate; the proof of closedCarrier_inter_subset_commonClosedFace runs on exactly that trichotomy.

Method

For x in the closed cell T the ordered normalized coordinates 0 = y₀ ≤ y₁ ≤ ⋯ ≤ y_d ≤ y_{d+1} = 1 (kuhnLevel) give the barycentric weights kuhnWeight T x k = y_{d+1-k} − y_{d-k} of the d + 1 corners; these are nonnegative, sum to 1, and reproduce x. That is closedCarrier_eq_convexHull_vertexSet. If a weight is strictly positive then, in the second cell, every coordinate of the corresponding corner is forced to the lower or the upper face of the second support cube; so the corner is a corner of the second cell too. Averaging the positive-weight corners then places x in the convex hull of the common corners.

References

• ABK26, (e.simplex.def, V(△)), (e.SW.def), (Step 1 of l.piecewise.affine.approx, the "adjacent coarse simplices share complete faces" sentence).

Normalized cube coordinates

noncomputable def Algsuperdiff.Section3.Provider.Affine.normCoord {d : ℕ} (Q : HCPolySupport.TriadicCube d) (i : Fin d) (x : HCPolySupport.Vec d) : ℝ

The coordinate of x in direction i normalized by the cube Q: it is 0 on the lower face of Q and 1 on the upper face.

Equations

• Algsuperdiff.Section3.Provider.Affine.normCoord Q i x = (HCPolySupport.cubeScaleFactor Q)⁻¹ * (x i - ↑(Q.index i) * HCPolySupport.cubeScaleFactor Q) + 1 / 2

The barycentric coordinates of a closed Kuhn cell

noncomputable def Algsuperdiff.Section3.Provider.Affine.kuhnLevel {d : ℕ} (T : Whitney.KuhnCell d) (x : HCPolySupport.Vec d) (j : ℕ) : ℝ

The ordered normalized coordinates of x in the cell T, with the endpoint conventions y₀ = 0 and y_{d+1} = 1.

Equations

• Algsuperdiff.Section3.Provider.Affine.kuhnLevel T x j = if hj0 : j = 0 then 0 else if hj : j ≤ d then Algsuperdiff.Section3.Provider.Affine.normCoord T.supportCube (T.order ⟨j - 1, ⋯⟩) x else 1

noncomputable def Algsuperdiff.Section3.Provider.Affine.kuhnWeight {d : ℕ} (T : Whitney.KuhnCell d) (x : HCPolySupport.Vec d) (k : Fin (d + 1)) : ℝ

The barycentric weight of the k-th corner of the Kuhn chain.

Equations

• Algsuperdiff.Section3.Provider.Affine.kuhnWeight T x k = Algsuperdiff.Section3.Provider.Affine.kuhnLevel T x (d + 1 - ↑k) - Algsuperdiff.Section3.Provider.Affine.kuhnLevel T x (d - ↑k)

theorem Algsuperdiff.Section3.Provider.Affine.closedCarrier_eq_convexHull_vertexSet {d : ℕ} (T : Whitney.KuhnCell d) : T.closedCarrier = (convexHull ℝ) T.vertexSet

A closed Kuhn cell is the convex hull of its d + 1 corners. This is one of the two identities queued as a disclosure by KuhnCell.vertex (Whitney/KuhnCells.lean); it is what makes the labelled corner list of KuhnCell.vertex an honest stand-in for the printed "extreme points" definition on the closed simplex.

theorem Algsuperdiff.Section3.Provider.Affine.isClosed_closedCarrier {d : ℕ} (T : Whitney.KuhnCell d) : IsClosed T.closedCarrier

Closed Kuhn cells are closed sets.

Strictness at a positive-weight corner

Equal-scale grid geometry

A positive-weight corner of the first cell is a corner of the second

The face-alignment lemma and the gluing step

def Algsuperdiff.Section3.Provider.Affine.commonClosedFace {d : ℕ} (T U : Whitney.KuhnCell d) : Set (HCPolySupport.Vec d)

The closed geometric face shared by two Kuhn cells: the convex hull of exactly their common corners. It is empty when they share no corner.

Equations

• Algsuperdiff.Section3.Provider.Affine.commonClosedFace T U = (convexHull ℝ) (T.vertexSet ∩ U.vertexSet)

theorem Algsuperdiff.Section3.Provider.Affine.commonClosedFace_subset_affineSpan {d : ℕ} (T U : Whitney.KuhnCell d) : commonClosedFace T U ⊆ ↑(affineSpan ℝ (T.vertexSet ∩ U.vertexSet))

theorem Algsuperdiff.Section3.Provider.Affine.closedCarrier_inter_subset_commonClosedFace {d : ℕ} (T U : Whitney.KuhnCell d) (hscale : T.supportCube.scale = U.supportCube.scale) : T.closedCarrier ∩ U.closedCarrier ⊆ commonClosedFace T U

The equal-scale face-alignment lemma of the Correction paragraph (used; pin corrected). Two Kuhn cells of the same scale on the globally aligned triadic grid meet only inside the convex hull of the corners they share: their closed carriers overlap in a common face.

The hypothesis is only that the two support cubes have the same scale, i.e. belong to one aligned grid.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterpAffine_eqOn_closedCarrier_inter {d : ℕ} (T U : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (hscale : T.supportCube.scale = U.supportCube.scale) : Set.EqOn (⇑(kuhnInterpAffine T g)) (⇑(kuhnInterpAffine U g)) (T.closedCarrier ∩ U.closedCarrier)

The gluing step, in bundled form: two equal-scale Kuhn cells interpolating one global vertex datum define the same affine value at every point of the intersection of their closed carriers. This is the manuscript's "since adjacent coarse simplices share complete faces, this extension is well-defined and continuous" (; mesh-interior half —), with the face-sharing supplied by closedCarrier_inter_subset_commonClosedFace rather than assumed.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_eqOn_closedCarrier_inter {d : ℕ} (T U : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (hscale : T.supportCube.scale = U.supportCube.scale) : Set.EqOn (kuhnInterp T g) (kuhnInterp U g) (T.closedCarrier ∩ U.closedCarrier)

The gluing step, in the unbundled form the piecewise-affine competitor uses: the two cell interpolants of one global vertex datum agree on the overlap of their closed carriers.