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

Statement of the convex Aleksandrov theorem

This file freezes the target theorem surface without asserting the theorem as an axiom.

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

The target Aleksandrov second order differentiability statement for convex functions.

The statement is intentionally formulated over a finite-dimensional real inner product space, rather than a matrix space. The almost-everywhere assertion is taken with respect to Lebesgue measure restricted to the open convex domain.

Equations

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

def AleksandrovDifferentiability.ConvexAleksandrovNullBadSetStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Equivalent null-exceptional-set formulation of ConvexAleksandrovAEStatement.

Equations

• AleksandrovDifferentiability.ConvexAleksandrovNullBadSetStatement E Ω u = (IsOpen Ω → ConvexOn ℝ Ω u → (MeasureTheory.volume.restrict Ω) (AleksandrovDifferentiability.secondOrderBadSet u) = 0)

def AleksandrovDifferentiability.ConvexAleksandrovNullBadSetOnStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Null-exceptional-set formulation using the exceptional set already intersected with the domain.

Equations

• AleksandrovDifferentiability.ConvexAleksandrovNullBadSetOnStatement E Ω u = (IsOpen Ω → ConvexOn ℝ Ω u → MeasureTheory.volume (AleksandrovDifferentiability.secondOrderBadSetOn Ω u) = 0)

def AleksandrovDifferentiability.DirectionalLineScalarEstimateFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Fubini/slicing target for the finite-dimensional proof: for every fixed direction, the set of base points whose affine-line restriction has scalar quadratic estimate data at the base parameter has full measure in the domain.

Equations

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

def AleksandrovDifferentiability.DirectionalLineScalarQuotientFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Punctured normalized quotient version of DirectionalLineScalarEstimateFubiniStatement.

Equations

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

def AleksandrovDifferentiability.DirectionalLineScalarUnitFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Unit-direction version of DirectionalLineScalarEstimateFubiniStatement. Scalar-rescaling invariance and the zero-direction lemma turn this into the all-directions statement.

Equations

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

def AleksandrovDifferentiability.DirectionalLineScalarQuotientUnitFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Punctured normalized quotient version of DirectionalLineScalarUnitFubiniStatement.

Equations

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

theorem AleksandrovDifferentiability.DirectionalLineScalarEstimateFubiniStatement.quotient (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarEstimateFubiniStatement E Ω u) : DirectionalLineScalarQuotientFubiniStatement E Ω u

The stronger local scalar directional-line Fubini target implies its punctured normalized quotient version.

theorem AleksandrovDifferentiability.DirectionalLineScalarUnitFubiniStatement.fubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarUnitFubiniStatement E Ω u) : DirectionalLineScalarEstimateFubiniStatement E Ω u

Unit-direction scalar Fubini implies the all-directions scalar Fubini target.

theorem AleksandrovDifferentiability.DirectionalLineScalarQuotientUnitFubiniStatement.fubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientUnitFubiniStatement E Ω u) : DirectionalLineScalarQuotientFubiniStatement E Ω u

Unit-direction quotient Fubini implies the all-directions quotient Fubini target.

theorem AleksandrovDifferentiability.DirectionalLineScalarUnitFubiniStatement.quotient (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarUnitFubiniStatement E Ω u) : DirectionalLineScalarQuotientUnitFubiniStatement E Ω u

The stronger local scalar unit-direction Fubini target implies its punctured normalized quotient version.

def AleksandrovDifferentiability.DirectionalLineScalarEstimateSlicewiseStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Slicewise version of DirectionalLineScalarEstimateFubiniStatement: for every affine line parallel to a fixed direction, almost every line parameter gives an ambient base point carrying scalar estimate data in that same direction. This is the one-dimensional input that a future finite-dimensional Fubini/disintegration argument should integrate over transverse parameters.

Equations

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

def AleksandrovDifferentiability.DirectionalLineScalarQuotientSlicewiseStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Punctured normalized quotient version of DirectionalLineScalarEstimateSlicewiseStatement.

Equations

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

theorem AleksandrovDifferentiability.DirectionalLineScalarEstimateSlicewiseStatement.quotient (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarEstimateSlicewiseStatement E Ω u) : DirectionalLineScalarQuotientSlicewiseStatement E Ω u

The stronger local scalar slicewise target implies its punctured normalized quotient version.

def AleksandrovDifferentiability.DirectionalLineScalarSlicewiseToFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

The remaining finite-dimensional measure-theoretic transfer for the directional-line scalar estimate target: slicewise almost-everywhere goodness along every affine line parallel to ξ implies ambient full measure of the fixed-direction good set.

Equations

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

def AleksandrovDifferentiability.DirectionalLineScalarQuotientSlicewiseToFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Punctured normalized quotient version of DirectionalLineScalarSlicewiseToFubiniStatement.

Equations

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

def AleksandrovDifferentiability.DirectionalLineScalarUnitSlicewiseToFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Unit-direction version of DirectionalLineScalarSlicewiseToFubiniStatement. Since scalar directional-line good sets are invariant under nonzero rescaling and the zero direction is automatic, this is enough for the all-directions transfer.

Equations

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

def AleksandrovDifferentiability.DirectionalLineScalarQuotientUnitSlicewiseToFubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) : Prop

Unit-direction quotient version of DirectionalLineScalarSlicewiseToFubiniStatement.

Equations

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

theorem AleksandrovDifferentiability.DirectionalLineScalarUnitSlicewiseToFubiniStatement.fubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarUnitSlicewiseToFubiniStatement E Ω u) : DirectionalLineScalarSlicewiseToFubiniStatement E Ω u

A unit-direction slicewise-to-Fubini transfer gives the all-directions transfer.

theorem AleksandrovDifferentiability.DirectionalLineScalarQuotientUnitSlicewiseToFubiniStatement.fubiniStatement (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} (h : DirectionalLineScalarQuotientUnitSlicewiseToFubiniStatement E Ω u) : DirectionalLineScalarQuotientSlicewiseToFubiniStatement E Ω u

Quotient version of DirectionalLineScalarUnitSlicewiseToFubiniStatement.fubiniStatement.

def AleksandrovDifferentiability.FiniteDirectionalLineScalarSlicewiseToFullMeasureStatement {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) (v : ι → E) : Prop

Finite-family version of the slicewise-to-Fubini transfer tailored to the polarization argument. It asks only for ambient full measure in the selected pure directions v i and in the off-diagonal pairwise-sum directions v i + v j.

Equations

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

def AleksandrovDifferentiability.FiniteDirectionalLineScalarQuotientSlicewiseToFullMeasureStatement {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) (v : ι → E) : Prop

Punctured normalized quotient version of FiniteDirectionalLineScalarSlicewiseToFullMeasureStatement.

Equations

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

def AleksandrovDifferentiability.CompatibleDirectionalSliceFullMeasureStatement {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) (v : ι → E) : Prop

Compatible finite-slice full-measure target: for a chosen finite direction family, the set of base points carrying scalar line estimates with one shared ambient first-order slope has full measure in the domain. This is stronger than the raw linewise Fubini target and is the natural input for compatible finite-dimensional reconstruction.

Equations

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

def AleksandrovDifferentiability.CompatibleDirectionalSliceQuotientFullMeasureStatement {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) (v : ι → E) : Prop

Punctured normalized quotient version of CompatibleDirectionalSliceFullMeasureStatement.

Equations

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

def AleksandrovDifferentiability.SymmetricCompatibleDirectionalSliceFullMeasureStatement {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) (v : ι → E) : Prop

Symmetric-compatible finite-slice full-measure target. This is the same compatible first-order finite-slice data, with pairwise-sum quadratic coefficients already symmetrized on the finite frame.

Equations

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

def AleksandrovDifferentiability.SymmetricCompatibleDirectionalSliceQuotientFullMeasureStatement {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (Ω : Set E) (u : E → ℝ) (v : ι → E) : Prop

Punctured normalized quotient version of SymmetricCompatibleDirectionalSliceFullMeasureStatement.

Equations

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

theorem AleksandrovDifferentiability.CompatibleDirectionalSliceFullMeasureStatement.quotient {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} {v : ι → E} (h : CompatibleDirectionalSliceFullMeasureStatement D E Ω u v) : CompatibleDirectionalSliceQuotientFullMeasureStatement D E Ω u v

The non-quotient compatible finite-slice full-measure target implies its quotient version.

theorem AleksandrovDifferentiability.CompatibleDirectionalSliceFullMeasureStatement.symmetric {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} {v : ι → E} (h : CompatibleDirectionalSliceFullMeasureStatement D E Ω u v) : SymmetricCompatibleDirectionalSliceFullMeasureStatement D E Ω u v

Compatible full-measure slice data implies full measure of the symmetrized compatible finite-slice locus.

theorem AleksandrovDifferentiability.CompatibleDirectionalSliceQuotientFullMeasureStatement.symmetric {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} {v : ι → E} (h : CompatibleDirectionalSliceQuotientFullMeasureStatement D E Ω u v) : SymmetricCompatibleDirectionalSliceQuotientFullMeasureStatement D E Ω u v

Compatible quotient full-measure slice data implies full measure of the symmetrized compatible quotient finite-slice locus.

theorem AleksandrovDifferentiability.CompatibleDirectionalSliceFullMeasureStatement.symmetricQuotient {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} {v : ι → E} (h : CompatibleDirectionalSliceFullMeasureStatement D E Ω u v) : SymmetricCompatibleDirectionalSliceQuotientFullMeasureStatement D E Ω u v

Non-quotient compatible full-measure slice data implies full measure of the symmetrized compatible quotient finite-slice locus.

theorem AleksandrovDifferentiability.SymmetricCompatibleDirectionalSliceFullMeasureStatement.quotient {ι : Type u_1} (D : Finset ι) (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Set E} {u : E → ℝ} {v : ι → E} (h : SymmetricCompatibleDirectionalSliceFullMeasureStatement D E Ω u v) : SymmetricCompatibleDirectionalSliceQuotientFullMeasureStatement D E Ω u v

Symmetric-compatible full-measure slice data implies its punctured normalized quotient version with the same symmetric finite-slice data.