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

Cube-local bad sets and estimates

def AleksandrovDifferentiability.CoordinateSliceBadPredicateMeasurable {n : ℕ} (sliceBad : CoordinateSliceBadPredicate n) (t : ℝ) : Prop

The bad-set predicate is jointly measurable in the transverse point and line parameter.

Equations

• AleksandrovDifferentiability.CoordinateSliceBadPredicateMeasurable sliceBad t = ∀ (i : Fin n), MeasurableSet {p : AleksandrovDifferentiability.SourceCubeSpace n × ℝ | sliceBad i p.1 p.2 t}

def AleksandrovDifferentiability.CoordinateSliceEndpointQuadraticControl {n : ℕ} (u : SourceCubeSpace n → ℝ) (sliceBad : CoordinateSliceBadPredicate n) (ρ K t : ℝ) : Prop

Analytic content required from the coordinate slice bad predicate: outside the slice bad sets, the one-dimensional estimates give quadratic endpoint bounds for the ambient Fréchet-gradient affine remainder on each coordinate line.

This is the source line where the localized one-dimensional maximal estimate gives 0 ≤ \tilde u(± h e_i) ≤ C t h^2. The actual maximal-function instantiation of sliceBad will prove this interface later.

Equations

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

def AleksandrovDifferentiability.coordinateSliceBadSet {n : ℕ} (sliceBad : CoordinateSliceBadPredicate n) (i : Fin n) (t : ℝ) : Set (SourceCubeSpace n)

The source bad set E_i(t) associated to a coordinate direction and an abstract slice bad predicate. A point x in Q_1 is tested by writing it as coordinateLineBase i x + (x i) e_i.

Equations

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

def AleksandrovDifferentiability.upperContactEstimateTotalBadSet {n : ℕ} (u : SourceCubeSpace n → ℝ) (sliceBad : CoordinateSliceBadPredicate n) (t : ℝ) : Set (SourceCubeSpace n)

The total source bad set E(t) = (Q_1 \ D) ∪ ⋃_i E_i(t), where D is the differentiability set.

Equations

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

def AleksandrovDifferentiability.ConvexAleksandrovNormalizedCubeStatement (n : ℕ) : Prop

Source-local normalized cube theorem. This corresponds to the preparatory convex source note's normalized cube theorem, formulated for global functions restricted to Q_3.

Equations

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

def AleksandrovDifferentiability.ConvexUpperContactEstimateStatement (n : ℕ) : Prop

Source-local upper-contact estimate target, corresponding to Proposition p.upper-contact-estimate. The constant is packaged existentially as a dimensional constant.

Equations

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

def AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement (n : ℕ) : Prop

Source-proof decomposition of the upper-contact estimate. For each convex bounded u and threshold t, one supplies an abstract coordinate-slice bad predicate such that:

• the total bad set E(t) has the desired measure bound, and
• the upper-contact bad set is contained in E(t).

The next formalization work is to instantiate this predicate using the localized maximal function of the one-dimensional second-derivative measure.

Equations

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

def AleksandrovDifferentiability.ConvexFiniteUpperContactOpeningAEOnCubeStatement (n : ℕ) : Prop

The limiting consequence of the upper-contact estimate: the upper-contact opening relative to Q_3 is finite almost everywhere in Q_1.

Equations

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

@[simp]

theorem AleksandrovDifferentiability.mem_firstOrderDifferentiabilitySet {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} : x ∈ firstOrderDifferentiabilitySet u ↔ DifferentiableAt ℝ u x

@[simp]

theorem AleksandrovDifferentiability.mem_finiteUpperContactOpeningSet {n : ℕ} {s : Set (SourceCubeSpace n)} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} : x ∈ finiteUpperContactOpeningSet s u ↔ ∃ (A : ℝ), HasUpperContactOpeningAtMostOn s u x A

@[simp]

theorem AleksandrovDifferentiability.mem_upperContactOpeningBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {A : ℝ} {x : SourceCubeSpace n} : x ∈ upperContactOpeningBadSet n u A ↔ x ∈ sourceOpenCube n 1 ∧ ¬HasUpperContactOpeningAtMostOn (sourceOpenCube n 3) u x A

@[simp]

theorem AleksandrovDifferentiability.mem_cubeGoodSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {A : ℝ} {x : SourceCubeSpace n} : x ∈ cubeGoodSet n u A ↔ x ∈ sourceOpenCube n 1 ∧ DifferentiableAt ℝ u x ∧ HasUpperContactOpeningAtMostOn (sourceOpenCube n 3) u x A

@[simp]

theorem AleksandrovDifferentiability.mem_coordinateSliceBadSet {n : ℕ} {sliceBad : CoordinateSliceBadPredicate n} {i : Fin n} {t : ℝ} {x : SourceCubeSpace n} : x ∈ coordinateSliceBadSet sliceBad i t ↔ x ∈ sourceOpenCube n 1 ∧ sliceBad i (coordinateLineBase i x) (x.ofLp i) t

@[simp]

theorem AleksandrovDifferentiability.mem_upperContactEstimateTotalBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {t : ℝ} {x : SourceCubeSpace n} : x ∈ upperContactEstimateTotalBadSet u sliceBad t ↔ x ∈ sourceOpenCube n 1 ∧ ¬DifferentiableAt ℝ u x ∨ ∃ (i : Fin n), x ∈ coordinateSliceBadSet sliceBad i t

theorem AleksandrovDifferentiability.cubeGoodSet_subset_sourceOpenCube {n : ℕ} {u : SourceCubeSpace n → ℝ} {A : ℝ} : cubeGoodSet n u A ⊆ sourceOpenCube n 1

theorem AleksandrovDifferentiability.cubeGoodSet_subset_finiteUpperContactOpeningSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {A : ℝ} : cubeGoodSet n u A ⊆ finiteUpperContactOpeningSet (sourceOpenCube n 3) u

theorem AleksandrovDifferentiability.coordinateSliceBadSet_subset_sourceOpenCube {n : ℕ} {sliceBad : CoordinateSliceBadPredicate n} {i : Fin n} {t : ℝ} : coordinateSliceBadSet sliceBad i t ⊆ sourceOpenCube n 1

theorem AleksandrovDifferentiability.MeasurableSet.coordinateSliceBadSet_of_product {n : ℕ} {sliceBad : CoordinateSliceBadPredicate n} {i : Fin n} {t : ℝ} (hbad : MeasurableSet {p : SourceCubeSpace n × ℝ | sliceBad i p.1 p.2 t}) : MeasurableSet (coordinateSliceBadSet sliceBad i t)

Product-coordinate measurability of a slice bad predicate implies measurability of the ambient coordinate bad set E_i(t).

theorem AleksandrovDifferentiability.CoordinateSliceBadPredicateMeasurable.coordinateSliceBadSet {n : ℕ} {sliceBad : CoordinateSliceBadPredicate n} {t : ℝ} (hbad : CoordinateSliceBadPredicateMeasurable sliceBad t) (i : Fin n) : MeasurableSet (AleksandrovDifferentiability.coordinateSliceBadSet sliceBad i t)

Named-obligation version of MeasurableSet.coordinateSliceBadSet_of_product, for all coordinate directions.

theorem AleksandrovDifferentiability.upperContactOpeningBadSet_mono_bound {n : ℕ} {u : SourceCubeSpace n → ℝ} {A B : ℝ} (hAB : A ≤ B) : upperContactOpeningBadSet n u B ⊆ upperContactOpeningBadSet n u A

The upper-contact bad set is antitone in the opening threshold: a larger allowed opening leaves fewer bad points.

theorem AleksandrovDifferentiability.coordinateSliceBadSet_base_mem_sourceOpenCube {n : ℕ} {sliceBad : CoordinateSliceBadPredicate n} {i : Fin n} {t : ℝ} {x : SourceCubeSpace n} (hx : x ∈ coordinateSliceBadSet sliceBad i t) : coordinateLineBase i x ∈ sourceOpenCube n 1

theorem AleksandrovDifferentiability.upperContactEstimateTotalBadSet_subset_sourceOpenCube {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {t : ℝ} : upperContactEstimateTotalBadSet u sliceBad t ⊆ sourceOpenCube n 1

theorem AleksandrovDifferentiability.differentiableAt_of_mem_sourceOpenCube_of_not_mem_totalBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {t : ℝ} {x : SourceCubeSpace n} (hxQ : x ∈ sourceOpenCube n 1) (hxE : x ∉ upperContactEstimateTotalBadSet u sliceBad t) : DifferentiableAt ℝ u x

If a point of Q_1 is not in the source total bad set E(t), then it belongs to the differentiability set D.

theorem AleksandrovDifferentiability.not_sliceBad_of_mem_sourceOpenCube_of_not_mem_totalBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {t : ℝ} {x : SourceCubeSpace n} (hxQ : x ∈ sourceOpenCube n 1) (hxE : x ∉ upperContactEstimateTotalBadSet u sliceBad t) (i : Fin n) : ¬sliceBad i (coordinateLineBase i x) (x.ofLp i) t

If a point of Q_1 is not in the source total bad set E(t), then no coordinate slice is bad at the corresponding base/parameter pair.

theorem AleksandrovDifferentiability.ConvexOn.sourceCube_subgradientOn_frechetGradient_of_not_mem_totalBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {x : SourceCubeSpace n} {t : ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hxQ : x ∈ sourceOpenCube n 1) (hxE : x ∉ upperContactEstimateTotalBadSet u sliceBad t) : SubgradientOn (sourceOpenCube n 3) u x (frechetGradient u x)

At a source-good point x ∈ Q_1 \ E(t), convexity makes the source Fréchet gradient a subgradient on Q_3.

theorem AleksandrovDifferentiability.affineRemainder_nonneg_increment_of_convex_of_not_mem_totalBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {x z : SourceCubeSpace n} {t : ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hxQ : x ∈ sourceOpenCube n 1) (hxE : x ∉ upperContactEstimateTotalBadSet u sliceBad t) (hz : x + z ∈ sourceOpenCube n 3) : 0 ≤ affineRemainder u x (frechetGradient u x) (x + z)

Source-good-point version of the affine-remainder nonnegativity: if x ∈ Q_1 is outside the total bad set E(t), then x is differentiable, lies in the interior of Q_3, and convexity gives the lower support for the source normalized remainder.

theorem AleksandrovDifferentiability.HasSourceCubeAffineRemainderUpperBound.hasUpperContactWithSlopeOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {A : ℝ} (h : HasSourceCubeAffineRemainderUpperBound n u x p A) : HasUpperContactWithSlopeOn (sourceOpenCube n 3) u x p A

A source-normalized affine-remainder upper bound is exactly an upper contact with the same opening and slope.

theorem AleksandrovDifferentiability.HasSourceCubeIncrementQuadraticBound.affineRemainderQuadraticBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {K : ℝ} (h : HasSourceCubeIncrementQuadraticBound n u x p K) : HasSourceCubeAffineRemainderQuadraticBound n u x p K

Increment-coordinate bounds imply pointwise source-style bounds on Q_3.

theorem AleksandrovDifferentiability.HasSourceCubeAffineRemainderQuadraticBound.incrementQuadraticBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {K : ℝ} (h : HasSourceCubeAffineRemainderQuadraticBound n u x p K) : HasSourceCubeIncrementQuadraticBound n u x p K

Pointwise source-style bounds on Q_3 imply the increment-coordinate formulation.

theorem AleksandrovDifferentiability.HasSourceCubeSmallIncrementQuadraticBound.combine_large {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {ρ Ksmall Klarge K : ℝ} (hsmall : HasSourceCubeSmallIncrementQuadraticBound n u x p ρ Ksmall) (hlarge : HasSourceCubeLargeIncrementQuadraticBound n u x p ρ Klarge) (hKsmall : Ksmall ≤ K) (hKlarge : Klarge ≤ K) : HasSourceCubeIncrementQuadraticBound n u x p K

Combine the small- and large-increment cases from the source proof into a global increment-coordinate quadratic bound.

theorem AleksandrovDifferentiability.HasSourceCubeSmallIncrementQuadraticBound.affineRemainderQuadraticBound_of_large {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {ρ Ksmall Klarge K : ℝ} (hsmall : HasSourceCubeSmallIncrementQuadraticBound n u x p ρ Ksmall) (hlarge : HasSourceCubeLargeIncrementQuadraticBound n u x p ρ Klarge) (hKsmall : Ksmall ≤ K) (hKlarge : Klarge ≤ K) : HasSourceCubeAffineRemainderQuadraticBound n u x p K

Combine the small- and large-increment source estimates directly into the pointwise source-style affine-remainder bound on Q_3.

theorem AleksandrovDifferentiability.HasSourceCubeAffineRemainderQuadraticBound.upperBound_two_mul {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {K : ℝ} (h : HasSourceCubeAffineRemainderQuadraticBound n u x p K) : HasSourceCubeAffineRemainderUpperBound n u x p (2 * K)

Source-style K * ‖y - x‖^2 control gives the normalized opening 2*K.

theorem AleksandrovDifferentiability.HasSourceCubeAffineRemainderQuadraticBound.openingAtMost_two_mul {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {K : ℝ} (h : HasSourceCubeAffineRemainderQuadraticBound n u x p K) : HasSourceCubeAffineRemainderOpeningAtMost n u x p (2 * K)

Source-style K * ‖y - x‖^2 control gives approximate opening at most 2*K.

theorem AleksandrovDifferentiability.HasSourceCubeAffineRemainderOpeningAtMost.hasUpperContactWithSlopeOpeningAtMostOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {A : ℝ} (h : HasSourceCubeAffineRemainderOpeningAtMost n u x p A) : HasUpperContactWithSlopeOpeningAtMostOn (sourceOpenCube n 3) u x p A

Approximate affine-remainder opening bounds give the project upper-contact-opening predicate with fixed slope.

theorem AleksandrovDifferentiability.HasSourceCubeAffineRemainderOpeningAtMost.hasUpperContactOpeningAtMostOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {A : ℝ} (h : HasSourceCubeAffineRemainderOpeningAtMost n u x p A) : HasUpperContactOpeningAtMostOn (sourceOpenCube n 3) u x A

Approximate affine-remainder opening bounds give the slope-free upper-contact-opening predicate used in the upper-contact bad set.

theorem AleksandrovDifferentiability.not_mem_upperContactOpeningBadSet_of_affineRemainderOpeningAtMost {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {A : ℝ} (h : HasSourceCubeAffineRemainderOpeningAtMost n u x p A) : x ∉ upperContactOpeningBadSet n u A

If a point in Q_1 carries an approximate source affine-remainder upper bound with opening A, then it is not in the source upper-contact bad set at threshold A.

theorem AleksandrovDifferentiability.upperContactOpeningBadSet_subset_totalBadSet_of_affineRemainderOpeningAtMost {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {A t : ℝ} (hgood : ∀ ⦃x : SourceCubeSpace n⦄, x ∈ sourceOpenCube n 1 → x ∉ upperContactEstimateTotalBadSet u sliceBad t → ∃ (p : SourceCubeSpace n), HasSourceCubeAffineRemainderOpeningAtMost n u x p A) : upperContactOpeningBadSet n u A ⊆ upperContactEstimateTotalBadSet u sliceBad t

Source inclusion principle: to prove the upper-contact bad set is contained in E(t), it suffices to construct the affine-remainder opening bound at each point of Q_1 \ E(t). This packages the contradiction step at the end of the source proof of Proposition p.upper-contact-estimate.

theorem AleksandrovDifferentiability.upperContactOpeningBadSet_subset_totalBadSet_of_affineRemainderQuadraticBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {K t : ℝ} (hgood : ∀ ⦃x : SourceCubeSpace n⦄, x ∈ sourceOpenCube n 1 → x ∉ upperContactEstimateTotalBadSet u sliceBad t → ∃ (p : SourceCubeSpace n), HasSourceCubeAffineRemainderQuadraticBound n u x p K) : upperContactOpeningBadSet n u (2 * K) ⊆ upperContactEstimateTotalBadSet u sliceBad t

Source-style inclusion principle with the bound as it appears in the proof: affineRemainder <= K * ‖y - x‖^2. The resulting upper-contact opening threshold is 2*K; the factor is later absorbed into the dimensional constant.

theorem AleksandrovDifferentiability.measure_upperContactOpeningBadSet_le_of_subset_totalBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {C t bound : ℝ} (hsubset : upperContactOpeningBadSet n u (C * (t + sourceCubeOscillation n u)) ⊆ upperContactEstimateTotalBadSet u sliceBad t) (hmeasure : MeasureTheory.volume (upperContactEstimateTotalBadSet u sliceBad t) ≤ ENNReal.ofReal bound) : MeasureTheory.volume (upperContactOpeningBadSet n u (C * (t + sourceCubeOscillation n u))) ≤ ENNReal.ofReal bound

The source proof reduces the upper-contact estimate to the inclusion {Theta > C(t + osc)} ⊆ E(t) and the total bad-set estimate for E(t).

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateStatement.of_decomposition {n : ℕ} (h : ConvexUpperContactEstimateDecompositionStatement n) : ConvexUpperContactEstimateStatement n

The decomposition used in the source proof implies the packaged upper-contact estimate.