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

Final convex Aleksandrov theorem

This module provides the public theorem endpoint for the convex Aleksandrov second-order differentiability theorem in finite-dimensional real inner product spaces.

theorem AleksandrovDifferentiability.convexAleksandrovAEStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : ConvexAleksandrovAEStatement E Ω u

Convex Aleksandrov second-order differentiability theorem, statement-predicate form.

theorem AleksandrovDifferentiability.convexAleksandrovAE (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (hΩ : IsOpen Ω) (hu : ConvexOn ℝ Ω u) : ∀ᵐ (x : E) ∂MeasureTheory.volume.restrict Ω, SecondOrderDifferentiableAt u x

Convex Aleksandrov second-order differentiability theorem.

If u is convex on an open subset Ω of a finite-dimensional real inner product space, then u is second-order differentiable at Lebesgue-a.e. point of Ω.