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

Core Aleksandrov Theorem Statements

def ViscositySolns.AleksandrovSecondDifferentiabilityByJetsTheorem (n : ℕ) : Prop

Aleksandrov's theorem in the jet-based form needed by the proof of Jensen's matrix lemma.

In quantified mathematical form, this says: if f : R^n -> R is semiconvex, then the set of points at which f has no second-order jet has Lebesgue measure zero.

Equations

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

def ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexTheorem (n : ℕ) : Prop

Global Aleksandrov theorem for convex functions.

This is the direct global form of the Mignot proof before the local closed-ball and semiconvex reductions.

Equations

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

theorem ViscositySolns.volume_eq_zero_of_closedBall_add_one_inter_eq_zero {n : ℕ} {s : Set (Point n)} (hnull : ∀ (k : ℕ), MeasureTheory.volume (Metric.closedBall 0 (↑k + 1) ∩ s) = 0) : MeasureTheory.volume s = 0

If a set is null on every closed ball centered at the origin with radius k + 1, then it is null on all of coordinate space.

def ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n : ℕ) : Prop

Localized Aleksandrov second-differentiability theorem on a closed ball.

In quantified mathematical form, this says: if f : R^n -> R is coordinate semiconvex on closedBall x0 r and 0 < r, then the set of points in closedBall x0 r at which f has no second-order jet has Lebesgue measure zero.

Equations

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

def ViscositySolns.CoordinateSemiconvexClosedBallExtensionHypothesis (n : ℕ) : Prop

Local semiconvex functions on closed balls admit globally semiconvex representatives on the corresponding open balls.

Equations

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

def ViscositySolns.CoordinateSemiconvexInteriorClosedBallExtensionHypothesis (n : ℕ) : Prop

Interior version of the local/global semiconvex bridge.

The extension is only required on a smaller open ball ball x0 r whose radius is strictly below the radius R on which semiconvexity is known.

Equations

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

theorem ViscositySolns.ball_subset_iUnion_closedBall_shrink {n : ℕ} (x0 : Point n) {R : ℝ} (hR : 0 < R) : Metric.ball x0 R ⊆ ⋃ (k : ℕ), Metric.closedBall x0 (R - R / (↑k + 2))

The open ball is covered by the countable exhaustion of closed balls with radii R - R / (k + 2).

theorem ViscositySolns.volume_sphere_eq_zero_of_pos {n : ℕ} (x0 : Point n) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (Metric.sphere x0 r) = 0

A metric sphere in coordinate space has zero Lebesgue measure as soon as the radius is positive.

theorem ViscositySolns.volume_closedBall_inter_eq_zero_of_ball_inter_eq_zero {n : ℕ} {s : Set (Point n)} {x0 : Point n} {r : ℝ} (hr : 0 < r) (hball : MeasureTheory.volume (Metric.ball x0 r ∩ s) = 0) : MeasureTheory.volume (Metric.closedBall x0 r ∩ s) = 0

To prove a bad set is null on a closed ball, it suffices to prove it is null on the corresponding open ball: the boundary sphere is null.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_openBall {n : ℕ} (hAleksandrov : ∀ (f : Point n → ℝ) (x0 : Point n) (r : ℝ), 0 < r → (∃ (lambda : ℝ), CoordinateSemiconvexOn lambda (Metric.closedBall x0 r) f) → MeasureTheory.volume (Metric.ball x0 r ∩ {x : Point n | ¬HasSomeSecondOrderJet f x}) = 0) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

Open-ball version of localized Aleksandrov implies the closed-ball statement.

This isolates the boundary-null reduction needed to pass from arguments on the interior of a ball to the closed-ball theorem consumed by Jensen's lemma.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsTheorem n) (hext : CoordinateSemiconvexClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The global semiconvex Aleksandrov theorem implies the local closed-ball theorem, provided each locally semiconvex function has a globally semiconvex representative agreeing with it on the open ball.

This is the semiconvex local/global bridge for the source proof: ordinary jets are local, and the closed-ball boundary has zero measure.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global_extension {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsTheorem n) (hext : CoordinateSemiconvexClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

Named-hypothesis version of the global-to-local semiconvex bridge.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global_interiorExtension {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsTheorem n) (hext : CoordinateSemiconvexInteriorClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The global semiconvex Aleksandrov theorem implies the local closed-ball theorem from the interior local/global extension bridge.

This avoids requiring an extension all the way up to the boundary of the original closed ball: the open ball is exhausted by smaller closed balls, and the boundary sphere is null.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexTheorem.to_semiconvex {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexTheorem n) : AleksandrovSecondDifferentiabilityByJetsTheorem n

The global convex Aleksandrov theorem implies the global semiconvex Aleksandrov theorem by adding the convexifying quadratic.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.to_global {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n) : AleksandrovSecondDifferentiabilityByJetsTheorem n

The localized closed-ball semiconvex Aleksandrov theorem implies the global semiconvex Aleksandrov theorem by covering coordinate space with closed balls.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global_convex_semiconvex {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexTheorem n) (hext : CoordinateSemiconvexClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The global convex source-proof theorem implies the local closed-ball semiconvex theorem whenever local semiconvex functions admit globally semiconvex representatives on the open ball.

def ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem (n : ℕ) : Prop

Localized Aleksandrov second-differentiability theorem for convex functions on a closed ball.

This is the convex target produced by the source proof after reducing a semiconvex function to its convexification.

Equations

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

def ViscositySolns.ConvexClosedBallExtensionHypothesis (n : ℕ) : Prop

Local convex functions on closed balls admit globally convex representatives on the corresponding open balls.

Equations

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

def ViscositySolns.ConvexInteriorClosedBallExtensionHypothesis (n : ℕ) : Prop

Interior version of the convex local/global bridge.

The globally convex representative is only required to agree with the local convex function on a smaller open ball.

Equations

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

theorem ViscositySolns.ConvexClosedBallExtensionHypothesis.to_coordinateSemiconvex {n : ℕ} (hext : ConvexClosedBallExtensionHypothesis n) : CoordinateSemiconvexClosedBallExtensionHypothesis n

A convex closed-ball extension theorem implies the corresponding semiconvex closed-ball extension theorem by extending the convexification and subtracting the same quadratic globally.

theorem ViscositySolns.ConvexInteriorClosedBallExtensionHypothesis.to_coordinateSemiconvex {n : ℕ} (hext : ConvexInteriorClosedBallExtensionHypothesis n) : CoordinateSemiconvexInteriorClosedBallExtensionHypothesis n

A convex interior closed-ball extension theorem implies the corresponding semiconvex interior extension theorem by extending the convexification and subtracting the same quadratic globally.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global_convexExtension {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsTheorem n) (hext : ConvexClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The global semiconvex Aleksandrov theorem implies the local closed-ball theorem from the more primitive convex extension bridge.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global_convexInteriorExtension {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsTheorem n) (hext : ConvexInteriorClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The global semiconvex Aleksandrov theorem implies the local closed-ball theorem from the more primitive convex interior extension bridge.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global_convexInterior {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexTheorem n) (hext : ConvexInteriorClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The global convex Aleksandrov theorem implies the local closed-ball theorem from the convex interior extension bridge.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem.of_openBall {n : ℕ} (hAleksandrov : ∀ (f : Point n → ℝ) (x0 : Point n) (r : ℝ), 0 < r → ConvexOn ℝ (Metric.closedBall x0 r) f → MeasureTheory.volume (Metric.ball x0 r ∩ {x : Point n | ¬HasSomeSecondOrderJet f x}) = 0) : AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem n

Open-ball version of the convex localized Aleksandrov theorem implies the closed-ball convex statement.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem.to_semiconvex {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The convex localized Aleksandrov theorem implies the semiconvex localized Aleksandrov theorem by adding the convexifying quadratic.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_convex_openBall {n : ℕ} (hAleksandrov : ∀ (g : Point n → ℝ) (x0 : Point n) (r : ℝ), 0 < r → ConvexOn ℝ (Metric.closedBall x0 r) g → MeasureTheory.volume (Metric.ball x0 r ∩ {x : Point n | ¬HasSomeSecondOrderJet g x}) = 0) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

An open-ball convex Aleksandrov theorem implies the closed-ball semiconvex Aleksandrov theorem.

This composes two local reductions: the boundary sphere is null, and semiconvexity becomes convexity after adding the standard quadratic.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem.to_global {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem n) : AleksandrovSecondDifferentiabilityByJetsForConvexTheorem n

The localized convex closed-ball theorem implies the global convex theorem by covering coordinate space with the closed balls closedBall 0 (k + 1).

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem.of_global {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexTheorem n) (hext : ConvexClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem n

The global convex Aleksandrov theorem implies the local closed-ball convex theorem, provided each closed-ball convex function has a globally convex representative agreeing with it on the open ball.

This is the formal local/global bridge for the source proof: ordinary jets are local, and the boundary sphere of the closed ball is null.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem.of_global_extension {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexTheorem n) (hext : ConvexClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsForConvexOnClosedBallTheorem n

Named-hypothesis version of the global-to-local convex bridge.

theorem ViscositySolns.AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem.of_global_convex {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsForConvexTheorem n) (hext : ConvexClosedBallExtensionHypothesis n) : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem n

The global convex source-proof theorem, plus a local globally convex representative on open balls, implies the closed-ball semiconvex Aleksandrov theorem.