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

Cube-local Aleksandrov statement interfaces

This file names the source-proof local targets on the normalized cubes Q_3 = (-3,3)^n and Q_1 = (-1,1)^n. These are statements and set interfaces, not axioms: the proof route will fill these targets using the upper-contact estimate from the source document.

def AleksandrovDifferentiability.firstOrderDifferentiabilitySet {n : ℕ} (u : SourceCubeSpace n → ℝ) : Set (SourceCubeSpace n)

Points where the first derivative exists in the ambient coordinate space.

Equations

• AleksandrovDifferentiability.firstOrderDifferentiabilitySet u = {x : AleksandrovDifferentiability.SourceCubeSpace n | DifferentiableAt ℝ u x}

def AleksandrovDifferentiability.finiteUpperContactOpeningSet {n : ℕ} (s : Set (SourceCubeSpace n)) (u : SourceCubeSpace n → ℝ) : Set (SourceCubeSpace n)

Points where the source upper-contact opening is finite, encoded through the project approximation-style predicate HasUpperContactOpeningAtMostOn.

Equations

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

def AleksandrovDifferentiability.upperContactOpeningBadSet (n : ℕ) (u : SourceCubeSpace n → ℝ) (A : ℝ) : Set (SourceCubeSpace n)

The source bad set where the upper-contact opening on Q_3 is not bounded by A, restricted to the conclusion cube Q_1. This represents {x in Q_1 : \overline\Theta_{u,Q_3}(x) > A} using the existing at-most-opening predicate.

Equations

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

def AleksandrovDifferentiability.cubeGoodSet (n : ℕ) (u : SourceCubeSpace n → ℝ) (A : ℝ) : Set (SourceCubeSpace n)

The cube-local good set Omega_A from the source proof: differentiability points in Q_1 whose upper-contact opening relative to Q_3 is at most A.

Equations

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

noncomputable def AleksandrovDifferentiability.sourceCubeOscillation (n : ℕ) (u : SourceCubeSpace n → ℝ) : ℝ

Oscillation of u on the large normalized source cube Q_3.

Equations

• AleksandrovDifferentiability.sourceCubeOscillation n u = AleksandrovDifferentiability.oscOn u (AleksandrovDifferentiability.sourceOpenCube n 3)

noncomputable def AleksandrovDifferentiability.frechetGradient {n : ℕ} (u : SourceCubeSpace n → ℝ) (x : SourceCubeSpace n) : SourceCubeSpace n

The source-proof gradient vector, represented as the Fréchet-Riesz vector associated to the Fréchet derivative. This names the object written grad u(x) in the source proof.

Equations

• AleksandrovDifferentiability.frechetGradient u x = (InnerProductSpace.toDual ℝ (AleksandrovDifferentiability.SourceCubeSpace n)).symm (fderiv ℝ u x)

theorem AleksandrovDifferentiability.frechetGradient_eq_gradient {n : ℕ} (u : SourceCubeSpace n → ℝ) : frechetGradient u = gradient u

The source gradient vector is Mathlib's gradient.

theorem AleksandrovDifferentiability.fderiv_apply_eq_inner_frechetGradient {n : ℕ} (u : SourceCubeSpace n → ℝ) (x z : SourceCubeSpace n) : (fderiv ℝ u x) z = inner ℝ (frechetGradient u x) z

The Fréchet derivative is represented by the source gradient vector.

theorem AleksandrovDifferentiability.ConvexOn.sourceCube_subgradientOn_frechetGradient {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hx : x ∈ interior (sourceOpenCube n 3)) (hd : DifferentiableAt ℝ u x) : SubgradientOn (sourceOpenCube n 3) u x (frechetGradient u x)

At an interior differentiability point of the source cube, the source Fréchet gradient is a subgradient on Q_3.

theorem AleksandrovDifferentiability.affineRemainder_nonneg_of_convex_of_differentiableAt_sourceCube {n : ℕ} {u : SourceCubeSpace n → ℝ} {x y : SourceCubeSpace n} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hx : x ∈ interior (sourceOpenCube n 3)) (hd : DifferentiableAt ℝ u x) (hy : y ∈ sourceOpenCube n 3) : 0 ≤ affineRemainder u x (frechetGradient u x) y

Convexity makes the source affine remainder with the Fréchet-gradient slope nonnegative on Q_3 at every interior differentiability point.

theorem AleksandrovDifferentiability.affineRemainder_nonneg_increment_of_convex_of_differentiableAt_sourceCube {n : ℕ} {u : SourceCubeSpace n → ℝ} {x z : SourceCubeSpace n} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hx : x ∈ interior (sourceOpenCube n 3)) (hd : DifferentiableAt ℝ u x) (hz : x + z ∈ sourceOpenCube n 3) : 0 ≤ affineRemainder u x (frechetGradient u x) (x + z)

Increment-coordinate version of affineRemainder_nonneg_of_convex_of_differentiableAt_sourceCube, matching the source proof's \tilde u(z) ≥ 0 normalization.

theorem AleksandrovDifferentiability.ConvexOn.sourceCube_affineRemainderIncrement_frechetGradient {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) : ConvexOn ℝ ((fun (z : SourceCubeSpace n) => x + z) ⁻¹' sourceOpenCube n 3) fun (z : SourceCubeSpace n) => affineRemainder u x (frechetGradient u x) (x + z)

The source-normalized affine remainder z ↦ u(x+z) - u(x) - grad u(x)·z is convex on the increment domain inside Q_3.

theorem AleksandrovDifferentiability.affineRemainder_coordinateLine_eq {n : ℕ} (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (i : Fin n) (r : ℝ) : affineRemainder (lineRestriction u (coordinateLineBase i x) (sourceCoordinateVector i)) (x.ofLp i) (inner ℝ p (sourceCoordinateVector i)) r = affineRemainder u x p (coordinateLinePoint i (coordinateLineBase i x) r)

Coordinate-line version of affineRemainder_lineRestriction_at, based at the coordinate line through x. This is the bookkeeping needed to turn one-dimensional estimates on the coordinate slice into estimates for the ambient normalized remainder.

theorem AleksandrovDifferentiability.affineRemainder_coordinateLine_add_eq {n : ℕ} (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (i : Fin n) (h : ℝ) : affineRemainder (lineRestriction u (coordinateLineBase i x) (sourceCoordinateVector i)) (x.ofLp i) (inner ℝ p (sourceCoordinateVector i)) (x.ofLp i + h) = affineRemainder u x p (x + h • sourceCoordinateVector i)

Positive coordinate increment form of affineRemainder_coordinateLine_eq.

theorem AleksandrovDifferentiability.affineRemainder_coordinateLine_sub_eq {n : ℕ} (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (i : Fin n) (h : ℝ) : affineRemainder (lineRestriction u (coordinateLineBase i x) (sourceCoordinateVector i)) (x.ofLp i) (inner ℝ p (sourceCoordinateVector i)) (x.ofLp i - h) = affineRemainder u x p (x - h • sourceCoordinateVector i)

Negative coordinate increment form of affineRemainder_coordinateLine_eq.

def AleksandrovDifferentiability.HasCoordinateLineEndpointQuadraticBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (ρ K : ℝ) : Prop

Coordinate-slice endpoint upper bounds, in the one-dimensional language produced by the localized maximal estimate in the source proof.

Equations

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

def AleksandrovDifferentiability.HasSourceCubeCoordinateEndpointQuadraticBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (ρ K : ℝ) : Prop

Ambient coordinate endpoint bounds for the normalized source remainder \tilde u(±h e_i).

Equations

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

def AleksandrovDifferentiability.sourceCrossPolytopeEndpointSet (n : ℕ) (h : ℝ) : Set (SourceCubeSpace n)

The endpoint set {± h e_i} used in the source proof before taking the convex hull.

Equations

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

def AleksandrovDifferentiability.sourceCrossPolytope (n : ℕ) (h : ℝ) : Set (SourceCubeSpace n)

The source cross-polytope K_h = conv {± h e_i}.

Equations

• AleksandrovDifferentiability.sourceCrossPolytope n h = (convexHull ℝ) (AleksandrovDifferentiability.sourceCrossPolytopeEndpointSet n h)

theorem AleksandrovDifferentiability.mem_sourceCrossPolytope_of_sum_abs_le {n : ℕ} {h : ℝ} (hn : 1 ≤ n) (hh : 0 < h) {z : SourceCubeSpace n} (hz : ∑ i : Fin n, |z.ofLp i| ≤ h) : z ∈ sourceCrossPolytope n h

Membership in the source cross-polytope from the coordinate l1 bound. This is the coordinate form of K_h = conv {± h e_i} used before inserting the Euclidean ball B_{h / sqrt n} in the source proof.

theorem AleksandrovDifferentiability.source_sum_abs_le_sqrt_card_mul_norm {n : ℕ} (z : SourceCubeSpace n) : ∑ i : Fin n, |z.ofLp i| ≤ √↑n * ‖z‖

Cauchy-Schwarz comparison between the coordinate l1 norm and the Euclidean norm in the source cube model.

theorem AleksandrovDifferentiability.mem_sourceCrossPolytope_of_norm_lt {n : ℕ} {h : ℝ} (hn : 1 ≤ n) (hh : 0 < h) {z : SourceCubeSpace n} (hz : ‖z‖ < h / √↑n) : z ∈ sourceCrossPolytope n h

Euclidean radius form of the source inclusion B_{h / sqrt n} ⊆ K_h.

theorem AleksandrovDifferentiability.ball_subset_sourceCrossPolytope {n : ℕ} {h : ℝ} (hn : 1 ≤ n) (hh : 0 < h) : Metric.ball 0 (h / √↑n) ⊆ sourceCrossPolytope n h

Metric-ball form of the source inclusion B_{h / sqrt n} ⊆ K_h.

theorem AleksandrovDifferentiability.HasCoordinateLineEndpointQuadraticBound.sourceCubeCoordinateEndpointQuadraticBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {ρ K : ℝ} (hline : HasCoordinateLineEndpointQuadraticBound n u x p ρ K) (hx : x ∈ sourceOpenCube n 3) : HasSourceCubeCoordinateEndpointQuadraticBound n u x p ρ K

Transfer the coordinate endpoint estimates from the one-dimensional slice language to the ambient normalized source remainder.

theorem AleksandrovDifferentiability.HasSourceCubeCoordinateEndpointQuadraticBound.mono_const {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {ρ K K' : ℝ} (h : HasSourceCubeCoordinateEndpointQuadraticBound n u x p ρ K) (hK : K ≤ K') : HasSourceCubeCoordinateEndpointQuadraticBound n u x p ρ K'

Coordinate endpoint bounds are monotone in the quadratic constant.

theorem AleksandrovDifferentiability.sourceCrossPolytopeEndpointSet_subset_incrementDomain {n : ℕ} {x : SourceCubeSpace n} {h : ℝ} (hendpoint : ∀ (i : Fin n), x + h • sourceCoordinateVector i ∈ sourceOpenCube n 3 ∧ x - h • sourceCoordinateVector i ∈ sourceOpenCube n 3) : sourceCrossPolytopeEndpointSet n h ⊆ (fun (z : SourceCubeSpace n) => x + z) ⁻¹' sourceOpenCube n 3

Endpoint membership in the increment domain for the source cross-polytope, assuming the corresponding coordinate endpoints lie in Q_3.

theorem AleksandrovDifferentiability.HasSourceCubeCoordinateEndpointQuadraticBound.affineRemainder_le_of_mem_crossPolytope {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p z : SourceCubeSpace n} {ρ K h : ℝ} (hend : HasSourceCubeCoordinateEndpointQuadraticBound n u x p ρ K) (hconv : ConvexOn ℝ ((fun (z : SourceCubeSpace n) => x + z) ⁻¹' sourceOpenCube n 3) fun (z : SourceCubeSpace n) => affineRemainder u x p (x + z)) (hhpos : 0 < h) (hhρ : h < ρ) (hendpoint : ∀ (i : Fin n), x + h • sourceCoordinateVector i ∈ sourceOpenCube n 3 ∧ x - h • sourceCoordinateVector i ∈ sourceOpenCube n 3) (hz : z ∈ sourceCrossPolytope n h) : affineRemainder u x p (x + z) ≤ K * h ^ 2

Source proof maximum-principle step on K_h = conv {± h e_i}: if the normalized affine remainder is convex and bounded by K h^2 at all coordinate endpoints, then it has the same upper bound throughout K_h.

def AleksandrovDifferentiability.HasSourceCubeAffineRemainderUpperBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (A : ℝ) : Prop

A cube-local affine-remainder upper bound with the source upper-contact normalization.

Equations

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

def AleksandrovDifferentiability.HasSourceCubeAffineRemainderOpeningAtMost (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (A : ℝ) : Prop

Approximate version of HasSourceCubeAffineRemainderUpperBound, matching HasUpperContactOpeningAtMostOn: every larger opening has the corresponding affine-remainder upper bound.

Equations

• AleksandrovDifferentiability.HasSourceCubeAffineRemainderOpeningAtMost n u x p A = ∀ (η : ℝ), 0 < η → AleksandrovDifferentiability.HasSourceCubeAffineRemainderUpperBound n u x p (A + η)

def AleksandrovDifferentiability.HasSourceCubeAffineRemainderQuadraticBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (K : ℝ) : Prop

Source-style affine-remainder bound, written as K * ‖y - x‖^2. The source proof obtains this form first, then absorbs the factor of 2 into the dimensional opening constant.

Equations

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

def AleksandrovDifferentiability.HasSourceCubeIncrementQuadraticBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (K : ℝ) : Prop

Increment-coordinate version of the source-style affine-remainder bound. This is the language of the source proof, where tilde u(z) is estimated for x + z ∈ Q_3.

Equations

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

def AleksandrovDifferentiability.HasSourceCubeSmallIncrementQuadraticBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (ρ K : ℝ) : Prop

Small-increment part of the source estimate.

Equations

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

def AleksandrovDifferentiability.HasSourceCubeAffineRemainderLinearGrowthBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (K0 K1 : ℝ) : Prop

Source large-increment input: on Q_3, the normalized affine remainder has at most affine growth in the increment size. The source obtains this from bounded oscillation and a local gradient bound.

Equations

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

def AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x : SourceCubeSpace n) (M : ℝ) : Prop

Source large-increment input before subtracting the affine part: values of u are bounded above relative to u x on Q_3. The source later obtains this from the oscillation of u on Q_3.

Equations

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

theorem AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound.affineRemainderLinearGrowthBound_of_norm_le {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {M G : ℝ} (hval : HasSourceCubeValueDifferenceUpperBound n u x M) (hp : ‖p‖ ≤ G) : HasSourceCubeAffineRemainderLinearGrowthBound n u x p M G

A value-difference bound and a slope norm bound give the linear-growth estimate for the normalized affine remainder.

theorem AleksandrovDifferentiability.sourceCube_coordinateEndpointDomain_of_mem_sourceOpenCube_one {n : ℕ} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 1) {ρ : ℝ} (hρ : ρ ≤ 1) ⦃r : ℝ⦄ : 0 < r → r < ρ → ∀ (i : Fin n), x + r • sourceCoordinateVector i ∈ sourceOpenCube n 3 ∧ x - r • sourceCoordinateVector i ∈ sourceOpenCube n 3

Points in Q_1 have all sufficiently short coordinate endpoints inside Q_3. This discharges the endpoint-domain hypothesis in the source small-increment estimate.

theorem AleksandrovDifferentiability.HasSourceCubeCoordinateEndpointQuadraticBound.smallIncrementQuadraticBound_of_convex {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {ρ K : ℝ} (hn : 1 ≤ n) (_hρ : 0 < ρ) (hend : HasSourceCubeCoordinateEndpointQuadraticBound n u x p ρ K) (hconv : ConvexOn ℝ ((fun (z : SourceCubeSpace n) => x + z) ⁻¹' sourceOpenCube n 3) fun (z : SourceCubeSpace n) => affineRemainder u x p (x + z)) (hendpoint : ∀ ⦃r : ℝ⦄, 0 < r → r < ρ → ∀ (i : Fin n), x + r • sourceCoordinateVector i ∈ sourceOpenCube n 3 ∧ x - r • sourceCoordinateVector i ∈ sourceOpenCube n 3) : HasSourceCubeSmallIncrementQuadraticBound n u x p (ρ / √↑n) (K * ↑n)

Source small-increment estimate from coordinate endpoint bounds. This packages the proof line: choose h = sqrt n * ‖z‖, use z ∈ K_h, and then apply the convex-hull endpoint bound.

def AleksandrovDifferentiability.HasSourceCubeLargeIncrementQuadraticBound (n : ℕ) (u : SourceCubeSpace n → ℝ) (x p : SourceCubeSpace n) (ρ K : ℝ) : Prop

Large-increment part of the source estimate.

Equations

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

theorem AleksandrovDifferentiability.HasSourceCubeAffineRemainderLinearGrowthBound.largeIncrementQuadraticBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {ρ K0 K1 : ℝ} (h : HasSourceCubeAffineRemainderLinearGrowthBound n u x p K0 K1) (hρ : 0 < ρ) (hK0 : 0 ≤ K0) (hK1 : 0 ≤ K1) : HasSourceCubeLargeIncrementQuadraticBound n u x p ρ (K0 / ρ ^ 2 + K1 / ρ)

Linear growth of the normalized remainder implies the source large-increment quadratic estimate once the increment norm is bounded below by a positive radius.

theorem AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound.largeIncrementQuadraticBound_of_norm_le {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {ρ M G : ℝ} (hval : HasSourceCubeValueDifferenceUpperBound n u x M) (hp : ‖p‖ ≤ G) (hρ : 0 < ρ) (hM : 0 ≤ M) (hG : 0 ≤ G) : HasSourceCubeLargeIncrementQuadraticBound n u x p ρ (M / ρ ^ 2 + G / ρ)

Value-difference control plus a slope norm bound imply the source large-increment quadratic estimate. This is the abstract Lean version of the source proof's large-z step from oscillation and the local gradient bound.

@[reducible, inline]

abbrev AleksandrovDifferentiability.CoordinateSliceBadPredicate (n : ℕ) : Type

An abstract predicate representing the localized one-dimensional maximal bad condition M μ_{i,y}(s) > t from the source proof. The arguments are the direction i, the coordinate-line base point y, the line parameter s, and the threshold t.

Equations

• AleksandrovDifferentiability.CoordinateSliceBadPredicate n = (Fin n → AleksandrovDifferentiability.SourceCubeSpace n → ℝ → ℝ → Prop)