KuhnInterpolation

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

The Kuhn-cell affine interpolant

This module provides a proved local carrier-level implementation for ABK26's l.piecewise.affine.approx: the operation "assign a value at each vertex, then extend affinely to the simplex" of the lemma's Step 1, together with the Step-2 gradient computation.

On a Kuhn cell T -- one triadic simplex of e.simplex.def, with the d + 1 vertices V(△) represented by KuhnCell.vertex -- the affine function agreeing with a datum g : Vec d → ℝ at those vertices is unique, and its gradient is the vector of Kuhn-edge difference quotients. This file defines that gradient (kuhnSlope) and that affine function (kuhnInterp) and proves the characterizing A:

• kuhnInterp_vertex -- the interpolant agrees with g at every vertex;
• kuhnInterp_sub / kuhnInterp_apply -- the interpolant is affine on all of Vec d, with constant gradient kuhnSlope T g;
• kuhnInterp_congr -- the interpolant depends on the vertex datum only through its d + 1 vertex values. Together with kuhnInterp_vertex this pins kuhnInterp as the affine extension of vertex data. A uniqueness statement against an arbitrary competitor in the coordinate presentation c + v·x is not among the statements below: the manuscript's "affine on the simplex" reading would additionally need affineSpan ℝ T.vertexSet = ⊤, which the edge chain v_{d-r} - v_{d-r-1} = 3^{scale}·e_{π(r)} supplies but which is not recorded here;
• kuhnSlope_apply / kuhnSlope_order -- the gradient formula in terms of vertex differences, ∂_{π(r)} = (g(v_{d-r}) − g(v_{d-r-1})) / 3^{scale};
• vertex_kuhnEdge_sub_apply -- the Kuhn edge chain: consecutive vertices differ by one cube side in one coordinate direction, the chain running from the lower to the upper corner of the support cube;
• kuhnInterpAffine -- the same function bundled as a Vec d →ᵃ[ℝ] ℝ, whose only purpose is kuhnInterpAffine_eqOn_affineSpan_inter_vertexSet: two cells interpolating one global vertex datum agree on the affine span of the vertices they share. That is the well-definedness instrument for a global interpolant assembled cell by cell, and it assumes no face-to-face property of SW(□_m).

What of the manuscript this file already carries

• e.hat.linear.linearity at the cell level: kuhnSlope_add, kuhnSlope_smul, kuhnInterp_add.
• Clause 1 of e.hat.linear.properties at the cell level: kuhnSlope_eq_zero_of_vertex_const, kuhnSlope_eq_zero_of_eqOn_vertexSet -- a competitor whose vertex values are all equal has vanishing gradient on the cell. This is the manuscript's "inside 𝒞_j, all coarse vertices receive the same value ⨍_{𝒞_j} ℓ_e, so ∇ℓ̂_e = 0 there".
• Clause 3 of e.hat.linear.properties ((clause 3; the cases-end line asserts nothing —, format)) at the cell level: kuhnSlope_linearFn, kuhnInterp_linearFn, kuhnSlope_eq_of_eqOn_vertexSet, kuhnInterp_eq_linearFn_of_eqOn_vertexSet -- if the vertex datum is ℓ_p on V(△) then the interpolant is ℓ_p and its gradient is p.
• Step 2's gradient display: abs_kuhnSlope_sub_le_of_vertex_oscillation, vecNormSq_kuhnSlope_sub_le_of_vertex_oscillation and its pointwise-vertex forms vecNormSq_kuhnSlope_sub_le_of_vertex_bound, vecNormSq_kuhnSlope_sub_le_of_vertexSet_bound are |∇ℓ̂_e − e|_{L^∞(𝔰)} ≤ (C / diam 𝔰) · max_{v,w ∈ V(𝔰)} |(ℓ̂_e − ℓ_e)(v) − (ℓ̂_e − ℓ_e)(w)| with the explicit constants of this implementation: the per-coordinate constant is 1 against the cube side 3^{scale}, and the Euclidean form carries √d.

Scope: what this file does NOT do

This file is the cell-level carrier only. It does not construct the global ℓ̂_p of l.piecewise.affine.approx, does not mention bad cubes, components, neighborhoods, layers, or the collar, and asserts nothing about how cells of different scales meet. In particular:

• (the neighborhood 𝒩(𝒞_j) spans three layers, not two) (neighborhoods of distinct components are not disjoint): no layer window and no disjointness statement occurs here.
• What it provides is the per-cell input to either reading -- the exact gradient of one affine piece in terms of its own vertex data -- so it is neutral with respect to the layer count and the overlap. *: no face-to-face or simplicial-complex property of SW(□_m) is used or asserted. kuhnInterp_eqOn_inter_vertexSet compares two cells only at points that are vertices of both.
• : no slope-square or collar constant enters.
• (ruled): not consumed -- no connectivity or cluster geometry appears.

References

• ABK26, (l.piecewise.affine.approx with e.hat.linear.properties), (its proof, Steps 1 and 2), (e.simplex.def, V(△)), (ℓ_e(x) = e · x), (e.hat.linear.linearity).

The linear function ℓ_p

def Algsuperdiff.Section3.Provider.Affine.linearFn {d : ℕ} (p : HCPolySupport.Vec d) : HCPolySupport.Vec d → ℝ

ABK26 ℓ_p: "we let ℓ_e(x) = e · x denote the linear function with slope e ∈ ℝ^d".

Equations

• Algsuperdiff.Section3.Provider.Affine.linearFn p x = HCPolySupport.vecDot p x

@[simp]

theorem Algsuperdiff.Section3.Provider.Affine.linearFn_apply {d : ℕ} (p x : HCPolySupport.Vec d) : linearFn p x = HCPolySupport.vecDot p x

Elementary vecDot algebra

The Kuhn edge chain

def Algsuperdiff.Section3.Provider.Affine.kuhnEdgeVertex {d : ℕ} (r : Fin d) : Fin (d + 1)

The upper endpoint of the r-th edge of the Kuhn vertex chain of a cell: the vertex v_{d-r} of KuhnCell.vertex.

Equations

• Algsuperdiff.Section3.Provider.Affine.kuhnEdgeVertex r = ⟨d - ↑r, ⋯⟩

def Algsuperdiff.Section3.Provider.Affine.kuhnEdgePrevVertex {d : ℕ} (r : Fin d) : Fin (d + 1)

The lower endpoint of the r-th edge of the Kuhn vertex chain of a cell: the vertex v_{d-r-1} of KuhnCell.vertex.

Equations

• Algsuperdiff.Section3.Provider.Affine.kuhnEdgePrevVertex r = ⟨d - ↑r - 1, ⋯⟩

theorem Algsuperdiff.Section3.Provider.Affine.vertex_kuhnEdge_sub_apply {d : ℕ} (T : Whitney.KuhnCell d) (r j : Fin d) : T.vertex (kuhnEdgeVertex r) j - T.vertex (kuhnEdgePrevVertex r) j = if j = T.order r then HCPolySupport.cubeScaleFactor T.supportCube else 0

The Kuhn edge chain. Consecutive vertices of a Kuhn cell differ in exactly one coordinate, by exactly one cube side: the r-th edge points along the coordinate direction T.order r. This is the geometric fact that makes the vertex list of KuhnCell.vertex a monotone lattice path from the lower to the upper corner of the support cube.

The slope of the interpolant

noncomputable def Algsuperdiff.Section3.Provider.Affine.kuhnSlope {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) : HCPolySupport.Vec d

The gradient of the affine interpolant on a Kuhn cell. Along the coordinate direction T.order r the cell has exactly one edge, from v_{d-r-1} to v_{d-r}, of length 3^{scale}; the gradient coordinate is the corresponding difference quotient. This is the "∇ℓ̂_e is constant on each coarse simplex" made explicit.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_apply {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (i : Fin d) : kuhnSlope T g i = (g (T.vertex (kuhnEdgeVertex ((Equiv.symm T.order) i))) - g (T.vertex (kuhnEdgePrevVertex ((Equiv.symm T.order) i)))) / HCPolySupport.cubeScaleFactor T.supportCube

The gradient formula, indexed in the ambient coordinate order.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_order {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (r : Fin d) : kuhnSlope T g (T.order r) = (g (T.vertex (kuhnEdgeVertex r)) - g (T.vertex (kuhnEdgePrevVertex r))) / HCPolySupport.cubeScaleFactor T.supportCube

The gradient formula, indexed in the cell's own edge order.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_congr {d : ℕ} (T : Whitney.KuhnCell d) {g g' : HCPolySupport.Vec d → ℝ} (hvert : ∀ (k : Fin (d + 1)), g (T.vertex k) = g' (T.vertex k)) : kuhnSlope T g = kuhnSlope T g'

The gradient depends on the vertex datum only through its d + 1 vertex values.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_add {d : ℕ} (T : Whitney.KuhnCell d) (g g' : HCPolySupport.Vec d → ℝ) : (kuhnSlope T fun (x : HCPolySupport.Vec d) => g x + g' x) = kuhnSlope T g + kuhnSlope T g'

e.hat.linear.linearity at the cell level: the interpolant's gradient is additive in the vertex datum.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_sub {d : ℕ} (T : Whitney.KuhnCell d) (g g' : HCPolySupport.Vec d → ℝ) : (kuhnSlope T fun (x : HCPolySupport.Vec d) => g x - g' x) = kuhnSlope T g - kuhnSlope T g'

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_smul {d : ℕ} (T : Whitney.KuhnCell d) (c : ℝ) (g : HCPolySupport.Vec d → ℝ) : (kuhnSlope T fun (x : HCPolySupport.Vec d) => c * g x) = c • kuhnSlope T g

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_eq_zero_of_vertex_const {d : ℕ} (T : Whitney.KuhnCell d) {g : HCPolySupport.Vec d → ℝ} {c : ℝ} (hconst : ∀ (k : Fin (d + 1)), g (T.vertex k) = c) : kuhnSlope T g = 0

Clause 1 of e.hat.linear.properties at the cell level, as the manuscript proves it: if every vertex of the cell receives the same value, the interpolant has vanishing gradient there.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_linearFn {d : ℕ} (T : Whitney.KuhnCell d) (p : HCPolySupport.Vec d) : kuhnSlope T (linearFn p) = p

Clause 3 of e.hat.linear.properties ((clause 3; the cases-end line asserts nothing —, format)) at the cell level, as the manuscript proves it: the vertex datum ℓ_p has interpolant gradient exactly p.

The interpolant

noncomputable def Algsuperdiff.Section3.Provider.Affine.kuhnInterp {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) : HCPolySupport.Vec d → ℝ

The affine interpolant of vertex data on a Kuhn cell, the object of Step 1 of the proof of l.piecewise.affine.approx: the affine function anchored at the cell's lower corner v_0 with gradient kuhnSlope T g. kuhnInterp_vertex shows it agrees with g at all d + 1 vertices, and eq_kuhnInterp_of_vertex_eq shows it is the only affine function that does; so this is the manuscript's "extend affinely" of the vertex datum g. It is defined, and affine, on all of Vec d; the manuscript uses its restriction to the cell.

Equations

• Algsuperdiff.Section3.Provider.Affine.kuhnInterp T g x = g (T.vertex 0) + HCPolySupport.vecDot (Algsuperdiff.Section3.Provider.Affine.kuhnSlope T g) (x - T.vertex 0)

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_apply {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : kuhnInterp T g x = g (T.vertex 0) + HCPolySupport.vecDot (kuhnSlope T g) (x - T.vertex 0)

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_sub {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (x y : HCPolySupport.Vec d) : kuhnInterp T g x - kuhnInterp T g y = HCPolySupport.vecDot (kuhnSlope T g) (x - y)

e.hat.linear.2 at the cell level: kuhnInterp T g is affine, with constant gradient kuhnSlope T g.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_add {d : ℕ} (T : Whitney.KuhnCell d) (g g' : HCPolySupport.Vec d → ℝ) : (kuhnInterp T fun (x : HCPolySupport.Vec d) => g x + g' x) = fun (x : HCPolySupport.Vec d) => kuhnInterp T g x + kuhnInterp T g' x

e.hat.linear.linearity at the cell level.

Agreement at the vertices

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_vertex {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (k : Fin (d + 1)) : kuhnInterp T g (T.vertex k) = g (T.vertex k)

The interpolant agrees with the vertex datum at every vertex. This is the defining property of Step 1's "extend affinely".

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_eqOn_inter_vertexSet {d : ℕ} (T U : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) : Set.EqOn (kuhnInterp T g) (kuhnInterp U g) (T.vertexSet ∩ U.vertexSet)

Two cells interpolating the same global vertex datum agree at every point that is a vertex of both. No face-to-face property of the partition is used or asserted.

The bundled affine map

noncomputable def Algsuperdiff.Section3.Provider.Affine.kuhnInterpAffine {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) : HCPolySupport.Vec d →ᵃ[ℝ] ℝ

kuhnInterp T g bundled as an affine map on Vec d, with linear part v ↦ (∇ℓ̂) · v. The bundling exists for exactly one purpose: it makes kuhnInterpAffine_eqOn_affineSpan_inter_vertexSet available, which is the well-definedness instrument for a global interpolant assembled cell by cell (the manuscript's "since adjacent coarse simplices share complete faces, this extension is well-defined and continuous"; the mesh-interior half ---). No face-to-face property is assumed anywhere: the statement is about the affine span of whatever vertices two cells happen to share.

Equations

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

@[simp]

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterpAffine_linear_apply {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (v : HCPolySupport.Vec d) : (kuhnInterpAffine T g).linear v = HCPolySupport.vecDot (kuhnSlope T g) v

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterpAffine_eqOn_affineSpan_inter_vertexSet {d : ℕ} (T U : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) : Set.EqOn ⇑(kuhnInterpAffine T g) ⇑(kuhnInterpAffine U g) ↑(affineSpan ℝ (T.vertexSet ∩ U.vertexSet))

Two cells interpolating the same global vertex datum agree on the affine span of the vertices they share. Nothing here asserts that any two cells of SW(□_m) do share a face.

Determination by the vertex values

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_linearFn {d : ℕ} (T : Whitney.KuhnCell d) (p : HCPolySupport.Vec d) : kuhnInterp T (linearFn p) = linearFn p

The interpolant of the vertex datum ℓ_p is ℓ_p itself: clause 3 of e.hat.linear.properties ((clause 3; the cases-end line asserts nothing —, format)) at the cell level.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_congr {d : ℕ} (T : Whitney.KuhnCell d) {g g' : HCPolySupport.Vec d → ℝ} (hvert : ∀ (k : Fin (d + 1)), g (T.vertex k) = g' (T.vertex k)) : kuhnInterp T g = kuhnInterp T g'

The interpolant depends on the vertex datum only through its d + 1 vertex values.

The Set.EqOn interface of clauses 1 and 3

These are the shapes that the global competitor of l.piecewise.affine.approx feeds to Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean), whose hbadF/hbadG carry clause 1 and whose hoffF/hoffG carry clause 3 as statements about the per-cell gradient value. Each is the corresponding vertex statement above, restated over V(△).

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_eq_zero_of_eqOn_vertexSet {d : ℕ} (T : Whitney.KuhnCell d) {g : HCPolySupport.Vec d → ℝ} {c : ℝ} (hconst : Set.EqOn g (fun (x : HCPolySupport.Vec d) => c) T.vertexSet) : kuhnSlope T g = 0

Clause 1 of e.hat.linear.properties in the vertex-set form: a competitor whose vertex datum is constant on V(△) has zero gradient on the cell.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnSlope_eq_of_eqOn_vertexSet {d : ℕ} (T : Whitney.KuhnCell d) {g : HCPolySupport.Vec d → ℝ} {p : HCPolySupport.Vec d} (hlin : Set.EqOn g (linearFn p) T.vertexSet) : kuhnSlope T g = p

Clause 3 of e.hat.linear.properties ((clause 3; the cases-end line asserts nothing —, format)) in the vertex-set form: a competitor whose vertex datum agrees with ℓ_p on V(△) has gradient exactly p on the cell.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnInterp_eq_linearFn_of_eqOn_vertexSet {d : ℕ} (T : Whitney.KuhnCell d) {g : HCPolySupport.Vec d → ℝ} {p : HCPolySupport.Vec d} (hlin : Set.EqOn g (linearFn p) T.vertexSet) : kuhnInterp T g = linearFn p

The function form of kuhnSlope_eq_of_eqOn_vertexSet: a competitor whose vertex datum agrees with ℓ_p on V(△) is ℓ_p on the cell.

Step 2: the gradient estimate

theorem Algsuperdiff.Section3.Provider.Affine.abs_kuhnSlope_sub_le_of_vertex_oscillation {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (p : HCPolySupport.Vec d) {B : ℝ} (hB : ∀ (k l : Fin (d + 1)), |g (T.vertex k) - linearFn p (T.vertex k) - (g (T.vertex l) - linearFn p (T.vertex l))| ≤ B) (i : Fin d) : |kuhnSlope T g i - p i| ≤ B / HCPolySupport.cubeScaleFactor T.supportCube

Step 2 of the proof of l.piecewise.affine.approx, in the coordinate form. If the vertex values of ℓ̂ − ℓ_p oscillate by at most B over the vertices of the cell, then each coordinate of ∇ℓ̂ − p is at most B over the cube side 3^{scale}. This is the printed |∇ℓ̂_e − e|_{L^∞(𝔰)} ≤ (C / diam 𝔰) · max_{v,w ∈ V(𝔰)} |(ℓ̂_e − ℓ_e)(v) − (ℓ̂_e − ℓ_e)(w)| with C = 1 against the cube side.

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_kuhnSlope_sub_le_of_vertex_oscillation {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (p : HCPolySupport.Vec d) {B : ℝ} (hB : ∀ (k l : Fin (d + 1)), |g (T.vertex k) - linearFn p (T.vertex k) - (g (T.vertex l) - linearFn p (T.vertex l))| ≤ B) : HCPolySupport.vecNormSq (kuhnSlope T g - p) ≤ ↑d * (B / HCPolySupport.cubeScaleFactor T.supportCube) ^ 2

Step 2 of the proof of l.piecewise.affine.approx, in the Euclidean form used downstream: the squared Euclidean norm of ∇ℓ̂ − p on the cell is at most d · (B / 3^{scale})². Against the cube side 3^{scale} the constant is √d; the printed display normalizes by diam(𝔰) = √d·3^{scale}, so the printed C(d) is d, not √d.

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_kuhnSlope_sub_le_of_vertex_bound {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (p : HCPolySupport.Vec d) {B : ℝ} (hB : ∀ (k : Fin (d + 1)), |g (T.vertex k) - linearFn p (T.vertex k)| ≤ B) : HCPolySupport.vecNormSq (kuhnSlope T g - p) ≤ ↑d * (2 * B / HCPolySupport.cubeScaleFactor T.supportCube) ^ 2

The form of Step 2 that the manuscript actually feeds: a pointwise vertex bound |ℓ̂ − ℓ_p| ≤ B at the vertices of the cell gives the gradient bound with the oscillation replaced by 2B.

theorem Algsuperdiff.Section3.Provider.Affine.vecNormSq_kuhnSlope_sub_le_of_vertexSet_bound {d : ℕ} (T : Whitney.KuhnCell d) (g : HCPolySupport.Vec d → ℝ) (p : HCPolySupport.Vec d) {B : ℝ} (hB : ∀ v ∈ T.vertexSet, |g v - linearFn p v| ≤ B) : HCPolySupport.vecNormSq (kuhnSlope T g - p) ≤ ↑d * (2 * B / HCPolySupport.cubeScaleFactor T.supportCube) ^ 2

Step 2 in the vertex-set form: this is the shape a global competitor feeds, since the manuscript's Step-2 vertex bound |ℓ̂_e(v) − ℓ_e(v)| ≤ |e| diam(𝒞_j) 1_{v ∈ V(𝒞_j)} is a statement about the points of V(△).