KuhnWeakGradient

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

Weak gradients of finite Kuhn-affine zero extensions

This file proves the finite-mesh analytic bridge needed for one component of the Section 3 piecewise-affine competitor. zeroExtendedKuhnAffine agrees with the proved Kuhn interpolant on a finite equal-scale mesh and is literally zero off the closed-cell union. Coordinate slicing gives a bounded classical line derivative away from finitely many endpoints; one-dimensional integration by parts and Fubini then identify an ambient weak derivative.

Everything here is restated and reproved at this repository's KuhnCell, kuhnInterp, and gluedKuhnAffine carriers.

def Algsuperdiff.Section3.Provider.Affine.kuhnCellCoordSlice {n : ℕ} (T : Whitney.KuhnCell (n + 1)) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : Set ℝ

Parameters at which a coordinate line meets one closed Kuhn cell.

Equations

• Algsuperdiff.Section3.Provider.Affine.kuhnCellCoordSlice T i z = {t : ℝ | i.insertNth t z ∈ T.closedCarrier}

theorem Algsuperdiff.Section3.Provider.Affine.isCompact_kuhnCell_closedCarrier {n : ℕ} (T : Whitney.KuhnCell (n + 1)) : IsCompact T.closedCarrier

A closed Kuhn cell is compact.

theorem Algsuperdiff.Section3.Provider.Affine.isometry_finInsertNth_line {n : ℕ} (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : Isometry fun (t : ℝ) => i.insertNth t z

Inserting the varying coordinate into a fixed coordinate line is an isometry.

theorem Algsuperdiff.Section3.Provider.Affine.isCompact_kuhnCellCoordSlice {n : ℕ} (T : Whitney.KuhnCell (n + 1)) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : IsCompact (kuhnCellCoordSlice T i z)

A coordinate slice of a closed Kuhn cell is compact.

theorem Algsuperdiff.Section3.Provider.Affine.convex_kuhnCellCoordSlice {n : ℕ} (T : Whitney.KuhnCell (n + 1)) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : Convex ℝ (kuhnCellCoordSlice T i z)

A coordinate slice of a closed Kuhn cell is convex.

theorem Algsuperdiff.Section3.Provider.Affine.kuhnCellCoordSlice_eq_Icc {n : ℕ} (T : Whitney.KuhnCell (n + 1)) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) (hne : (kuhnCellCoordSlice T i z).Nonempty) : kuhnCellCoordSlice T i z = Set.Icc (sInf (kuhnCellCoordSlice T i z)) (sSup (kuhnCellCoordSlice T i z))

A nonempty coordinate slice is the interval between its extrema.

noncomputable def Algsuperdiff.Section3.Provider.Affine.kuhnCellCoordSliceEndpoints {n : ℕ} (T : Whitney.KuhnCell (n + 1)) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : Finset ℝ

The at-most-two endpoints of one coordinate slice.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.eventually_mem_kuhnCellCoordSlice_iff {n : ℕ} (T : Whitney.KuhnCell (n + 1)) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) {t : ℝ} (ht : t ∉ kuhnCellCoordSliceEndpoints T i z) : ∀ᶠ (s : ℝ) in nhds t, s ∈ kuhnCellCoordSlice T i z ↔ t ∈ kuhnCellCoordSlice T i z

Away from the endpoints, slice membership is locally constant.

noncomputable def Algsuperdiff.Section3.Provider.Affine.kuhnCellSliceEndpoints {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : Finset ℝ

The finite endpoint set contributed by every cell in a finite mesh.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.eventually_forall_mem_coordSlice_iff {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) {t : ℝ} (ht : t ∉ kuhnCellSliceEndpoints cells i z) : ∀ᶠ (s : ℝ) in nhds t, ∀ T ∈ cells, s ∈ kuhnCellCoordSlice T i z ↔ t ∈ kuhnCellCoordSlice T i z

Off the endpoint set, membership in every mesh cell is locally constant.

The zero-off-mesh representative and its line derivatives

noncomputable def Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffine {d : ℕ} (cells : Finset (Whitney.KuhnCell d)) (g : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : ℝ

The zero extension of a finite Kuhn gluing. Unlike gluedKuhnAffine, which returns its datum off the mesh, this is the representative needed for a compactly supported component correction.

Equations

• Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffine cells g x = if ∃ T ∈ cells, x ∈ T.closedCarrier then Algsuperdiff.Section3.Provider.Affine.gluedKuhnAffine cells g x else 0

theorem Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffine_of_mem_closedCarrier {d : ℕ} {cells : Finset (Whitney.KuhnCell d)} {scale : ℤ} (hscale : ∀ T ∈ cells, T.supportCube.scale = scale) (g : HCPolySupport.Vec d → ℝ) {T : Whitney.KuhnCell d} (hT : T ∈ cells) {x : HCPolySupport.Vec d} (hx : x ∈ T.closedCarrier) : zeroExtendedKuhnAffine cells g x = kuhnInterp T g x

On a selected closed cell, the zero extension is that cell's interpolant.

theorem Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffine_of_forall_notMem {d : ℕ} (cells : Finset (Whitney.KuhnCell d)) (g : HCPolySupport.Vec d → ℝ) {x : HCPolySupport.Vec d} (hx : ∀ T ∈ cells, x ∉ T.closedCarrier) : zeroExtendedKuhnAffine cells g x = 0

Off every selected closed cell, the zero extension is zero.

noncomputable def Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffineLineSlope {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) (t : ℝ) : ℝ

The selected coordinate slope along a line, with value zero off the mesh.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffineCoordBound {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) (i : Fin (n + 1)) : ℝ

A uniform bound for all selected slopes in one coordinate.

Equations

• Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffineCoordBound cells g i = ∑ T ∈ cells, ‖Algsuperdiff.Section3.Provider.Affine.kuhnSlope T g i‖

theorem Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffineCoordBound_nonneg {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) (i : Fin (n + 1)) : 0 ≤ zeroExtendedKuhnAffineCoordBound cells g i

The coordinate-slope bound is nonnegative.

theorem Algsuperdiff.Section3.Provider.Affine.hasDerivAt_zeroExtendedKuhnAffine_insertNth_of_not_mem_endpoints {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) {scale : ℤ} (hscale : ∀ T ∈ cells, T.supportCube.scale = scale) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) {t : ℝ} (ht : t ∉ kuhnCellSliceEndpoints cells i z) : HasDerivAt (fun (s : ℝ) => zeroExtendedKuhnAffine cells g (i.insertNth s z)) (zeroExtendedKuhnAffineLineSlope cells g i z t) t

Away from slice endpoints, the coordinate-line derivative is the selected slope.

theorem Algsuperdiff.Section3.Provider.Affine.norm_zeroExtendedKuhnAffineLineSlope_le {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) (t : ℝ) : ‖zeroExtendedKuhnAffineLineSlope cells g i z t‖ ≤ zeroExtendedKuhnAffineCoordBound cells g i

Every selected line slope is bounded by the finite coordinate sum.

theorem Algsuperdiff.Section3.Provider.Affine.lipschitzWith_zeroExtendedKuhnAffine_insertNth {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) {scale : ℤ} (hscale : ∀ T ∈ cells, T.supportCube.scale = scale) (hcontinuous : Continuous (zeroExtendedKuhnAffine cells g)) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : LipschitzWith ⟨zeroExtendedKuhnAffineCoordBound cells g i, ⋯⟩ fun (t : ℝ) => zeroExtendedKuhnAffine cells g (i.insertNth t z)

A continuous finite equal-scale zero extension is Lipschitz on every coordinate line.

noncomputable def Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffineCoordDeriv {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) (i : Fin (n + 1)) (x : HCPolySupport.Vec (n + 1)) : ℝ

The ambient representative of the coordinate-line derivative.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.measurable_zeroExtendedKuhnAffineCoordDeriv {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) (hcontinuous : Continuous (zeroExtendedKuhnAffine cells g)) (i : Fin (n + 1)) : Measurable (zeroExtendedKuhnAffineCoordDeriv cells g i)

The coordinate-line derivative representative is measurable.

theorem Algsuperdiff.Section3.Provider.Affine.norm_zeroExtendedKuhnAffineCoordDeriv_le {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) {scale : ℤ} (hscale : ∀ T ∈ cells, T.supportCube.scale = scale) (hcontinuous : Continuous (zeroExtendedKuhnAffine cells g)) (i : Fin (n + 1)) (x : HCPolySupport.Vec (n + 1)) : ‖zeroExtendedKuhnAffineCoordDeriv cells g i x‖ ≤ zeroExtendedKuhnAffineCoordBound cells g i

The ambient derivative representative obeys the finite coordinate bound.

One-dimensional integration by parts

theorem Algsuperdiff.Section3.Provider.Affine.integral_zeroExtendedKuhnAffine_mul_testCoordDeriv_eq_neg {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) {scale : ℤ} (hscale : ∀ T ∈ cells, T.supportCube.scale = scale) (hcontinuous : Continuous (zeroExtendedKuhnAffine cells g)) {φ : HCPolySupport.Vec (n + 1) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (i : Fin (n + 1)) (z : HCPolySupport.Vec n) : ∫ (t : ℝ), zeroExtendedKuhnAffine cells g (i.insertNth t z) * (fderiv ℝ φ (i.insertNth t z)) (HCPolySupport.basisVec i) = -∫ (t : ℝ), deriv (fun (s : ℝ) => zeroExtendedKuhnAffine cells g (i.insertNth s z)) t * φ (i.insertNth t z)

Coordinate-line integration by parts for the zero-extended gluing.

Ambient weak derivatives

theorem Algsuperdiff.Section3.Provider.Affine.hasWeakPartialDerivOn_univ_zeroExtendedKuhnAffine {n : ℕ} (cells : Finset (Whitney.KuhnCell (n + 1))) (g : HCPolySupport.Vec (n + 1) → ℝ) {scale : ℤ} (hscale : ∀ T ∈ cells, T.supportCube.scale = scale) (hcontinuous : Continuous (zeroExtendedKuhnAffine cells g)) (i : Fin (n + 1)) : HCPolySupport.HasWeakPartialDerivOn Set.univ i (zeroExtendedKuhnAffine cells g) (zeroExtendedKuhnAffineCoordDeriv cells g i)

The coordinate-line representative is a weak partial derivative on ambient space.

theorem Algsuperdiff.Section3.Provider.Affine.zeroExtendedKuhnAffineCoordDeriv_eq_of_mem_openCarrier {n : ℕ} {cells : Finset (Whitney.KuhnCell (n + 1))} {g : HCPolySupport.Vec (n + 1) → ℝ} {scale : ℤ} (hscale : ∀ T ∈ cells, T.supportCube.scale = scale) {T : Whitney.KuhnCell (n + 1)} (hT : T ∈ cells) {x : HCPolySupport.Vec (n + 1)} (hx : x ∈ T.openCarrier) (i : Fin (n + 1)) : zeroExtendedKuhnAffineCoordDeriv cells g i x = kuhnSlope T g i

On the interior of a mesh cell, the line-derivative representative is the literal Kuhn slope coordinate.