Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

First-order differentiability almost everywhere on source cubes

This file supplies the first-differentiability-a.e. input used by the source upper-contact estimate. The proof is the standard route: convexity on the open cube gives local Lipschitz regularity; compactness of the closed unit cube upgrades this to a global Lipschitz bound on a compact neighborhood of Q_1; Rademacher then gives differentiability almost everywhere on Q_1.

theorem AleksandrovDifferentiability.ConvexOn.sourceOpenCube_locallyLipschitzOn {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : LocallyLipschitzOn (sourceOpenCube n 3) u

A convex function on the source cube is locally Lipschitz on Q_3.

theorem AleksandrovDifferentiability.ConvexOn.exists_lipschitzOnWith_sourceClosedCube_one {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : ∃ (K : NNReal), LipschitzOnWith K u (sourceClosedCube n 1)

Convexity on Q_3 gives a global Lipschitz bound on the closed unit cube.

theorem AleksandrovDifferentiability.ConvexOn.exists_lipschitzOnWith_sourceOpenCube_one {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : ∃ (K : NNReal), LipschitzOnWith K u (sourceOpenCube n 1)

Convexity on Q_3 gives a global Lipschitz bound on Q_1.

theorem AleksandrovDifferentiability.ConvexOn.ae_differentiableAt_sourceOpenCube_one {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : ∀ᵐ (x : SourceCubeSpace n) ∂MeasureTheory.volume.restrict (sourceOpenCube n 1), DifferentiableAt ℝ u x

Convex functions on the source cube are differentiable almost everywhere on Q_1.

theorem AleksandrovDifferentiability.ConvexOn.volume_sourceOpenCube_diff_firstOrderDifferentiabilitySet_eq_zero {n : ℕ} {u : SourceCubeSpace n → ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0

The non-first-differentiability set in Q_1 is null for convex functions on Q_3.