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

Oscillation bounds on source cubes

This file records source-cube order estimates involving oscOn. These are used in the large-increment part of the upper-contact estimate.

theorem AleksandrovDifferentiability.BoundedOn.bddAbove_image {E : Type u_1} {s : Set E} {u : E → ℝ} (h : BoundedOn s u) : BddAbove (u '' s)

Project-local bridge from bornological boundedness of real values to order-boundedness above.

theorem AleksandrovDifferentiability.BoundedOn.bddBelow_image {E : Type u_1} {s : Set E} {u : E → ℝ} (h : BoundedOn s u) : BddBelow (u '' s)

Project-local bridge from bornological boundedness of real values to order-boundedness below.

theorem AleksandrovDifferentiability.sourceCubeOscillation_nonneg_of_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} (hbounded : BoundedOn (sourceOpenCube n 3) u) : 0 ≤ sourceCubeOscillation n u

The source-cube oscillation is nonnegative under the boundedness hypothesis used by the normalized cube theorem.

theorem AleksandrovDifferentiability.measure_eq_zero_of_forall_le_ofReal_const_div_nat {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {K : ℝ} (hK : 0 ≤ K) (hbound : ∀ (m : ℕ), 0 < m → μ s ≤ ENNReal.ofReal (K / ↑m)) : μ s = 0

ENNReal squeeze lemma for estimates bounded by K / m for every positive natural m.

theorem AleksandrovDifferentiability.sourceOpenCube_diff_finiteUpperContactOpeningSet_subset_upperContactOpeningBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} (A : ℝ) : sourceOpenCube n 1 \ finiteUpperContactOpeningSet (sourceOpenCube n 3) u ⊆ upperContactOpeningBadSet n u A

Points in Q_1 without finite upper-contact opening lie in every upper-contact bad set.

theorem AleksandrovDifferentiability.ConvexFiniteUpperContactOpeningAEOnCubeStatement.of_upperContactEstimate {n : ℕ} (hestimate : ConvexUpperContactEstimateStatement n) : ConvexFiniteUpperContactOpeningAEOnCubeStatement n

The upper-contact estimate implies that the upper-contact opening is finite a.e. on Q_1.

This is the limiting step in the source proof: the exceptional set is contained in every bad set {Θ > C(t + osc)}, while the estimate bounds those bad sets by C osc / t, which tends to zero as t tends to infinity.

theorem AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound.of_sourceCubeOscillation {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 3) (hupper : BddAbove (u '' sourceOpenCube n 3)) (hlower : BddBelow (u '' sourceOpenCube n 3)) : HasSourceCubeValueDifferenceUpperBound n u x (sourceCubeOscillation n u)

If the values of u on Q_3 are order-bounded above and below, then the oscillation on Q_3 bounds all value differences from a fixed base point in Q_3.

theorem AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound.of_boundedOn_sourceCubeOscillation {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} (hx : x ∈ sourceOpenCube n 3) (hbounded : BoundedOn (sourceOpenCube n 3) u) : HasSourceCubeValueDifferenceUpperBound n u x (sourceCubeOscillation n u)

Boundedness of u on Q_3, in the project-local BoundedOn sense, supplies the order-boundedness needed to bound value differences by the source-cube oscillation.

theorem AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound.subgradient_norm_le_of_mem_sourceOpenCube_one {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {M : ℝ} (hval : HasSourceCubeValueDifferenceUpperBound n u x M) (hp : SubgradientOn (sourceOpenCube n 3) u x p) (hx : x ∈ sourceOpenCube n 1) : ‖p‖ ≤ M

Cube-local form of the source local gradient bound, stated for any subgradient. If values above u x are bounded by M on Q_3 and x ∈ Q_1, then a subgradient at x has norm at most M. The proof tests the supporting inequality in the normalized direction of the subgradient.

theorem AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound.subgradient_norm_le_of_mem_three_halves {n : ℕ} {u : SourceCubeSpace n → ℝ} {x p : SourceCubeSpace n} {M : ℝ} (hval : HasSourceCubeValueDifferenceUpperBound n u x M) (hp : SubgradientOn (sourceOpenCube n 3) u x p) (hx : x ∈ sourceOpenCube n (3 / 2)) : ‖p‖ ≤ M

Variant of the source local gradient bound for points in Q_{3/2}. The proof tests the supporting inequality in a normalized direction for length 3 / 2, which still remains inside Q_3.

theorem AleksandrovDifferentiability.HasSourceCubeValueDifferenceUpperBound.subgradient_set_isBounded_of_mem_three_halves {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} {M : ℝ} (hval : HasSourceCubeValueDifferenceUpperBound n u x M) (hx : x ∈ sourceOpenCube n (3 / 2)) : Bornology.IsBounded {p : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u x p}

The source local subgradient bound gives bornological boundedness of the full subdifferential at points in Q_{3/2}.

theorem AleksandrovDifferentiability.sourceCube_subgradient_set_isBounded_of_boundedOn_three_halves {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} (hbounded : BoundedOn (sourceOpenCube n 3) u) (hx : x ∈ sourceOpenCube n (3 / 2)) : Bornology.IsBounded {p : SourceCubeSpace n | SubgradientOn (sourceOpenCube n 3) u x p}

Boundedness of u on Q_3 gives boundedness of every subdifferential at points in Q_{3/2}. This is the cube-local boundedness input for compact subdifferential extrema.

theorem AleksandrovDifferentiability.ConvexOn.norm_frechetGradient_le_sourceCubeOscillation_of_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hx : x ∈ sourceOpenCube n 1) (hderiv : DifferentiableAt ℝ u x) : ‖frechetGradient u x‖ ≤ sourceCubeOscillation n u

Source-cube local gradient bound in the form used by the large-increment estimate.

theorem AleksandrovDifferentiability.ConvexOn.norm_frechetGradient_le_sourceCubeOscillation_of_boundedOn_three_halves {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hx : x ∈ sourceOpenCube n (3 / 2)) (hderiv : DifferentiableAt ℝ u x) : ‖frechetGradient u x‖ ≤ sourceCubeOscillation n u

Source-cube local gradient bound for differentiability points in Q_{3/2}.

theorem AleksandrovDifferentiability.ConvexOn.sourceCube_largeIncrementQuadraticBound_of_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} {ρ : ℝ} (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hx : x ∈ sourceOpenCube n 1) (hderiv : DifferentiableAt ℝ u x) (hρ : 0 < ρ) : HasSourceCubeLargeIncrementQuadraticBound n u x (frechetGradient u x) ρ (sourceCubeOscillation n u / ρ ^ 2 + sourceCubeOscillation n u / ρ)

Large-increment estimate in the exact source-cube form obtained from oscillation and the local gradient bound.

theorem AleksandrovDifferentiability.ConvexOn.sourceCube_affineRemainderQuadraticBound_of_endpoint_of_boundedOn {n : ℕ} {u : SourceCubeSpace n → ℝ} {x : SourceCubeSpace n} {ρ K : ℝ} (hn : 1 ≤ n) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK : 0 ≤ K) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hx : x ∈ sourceOpenCube n 1) (hderiv : DifferentiableAt ℝ u x) (hend : HasSourceCubeCoordinateEndpointQuadraticBound n u x (frechetGradient u x) ρ K) : HasSourceCubeAffineRemainderQuadraticBound n u x (frechetGradient u x) (K * ↑n + (sourceCubeOscillation n u / (ρ / √↑n) ^ 2 + sourceCubeOscillation n u / (ρ / √↑n)))

Source-cube pointwise quadratic affine-remainder estimate obtained by combining the coordinate endpoint bounds, the convexity maximum-principle step on the cross-polytope, and the large-increment estimate from oscillation and the local gradient bound.

theorem AleksandrovDifferentiability.CoordinateSliceEndpointQuadraticControl.sourceCubeCoordinateEndpointQuadraticBound {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {x : SourceCubeSpace n} {ρ K t : ℝ} (hcontrol : CoordinateSliceEndpointQuadraticControl u sliceBad ρ K t) (hxQ : x ∈ sourceOpenCube n 1) (hxE : x ∉ upperContactEstimateTotalBadSet u sliceBad t) : HasSourceCubeCoordinateEndpointQuadraticBound n u x (frechetGradient u x) ρ K

At a point of Q_1 \ E(t), the abstract endpoint-control property of the slice bad predicate supplies the coordinate endpoint bounds needed by the combined source estimate.

theorem AleksandrovDifferentiability.ConvexOn.sourceCube_affineRemainderQuadraticBound_of_sliceControl_of_not_mem_totalBadSet {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {x : SourceCubeSpace n} {ρ K t : ℝ} (hn : 1 ≤ n) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK : 0 ≤ K) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hcontrol : CoordinateSliceEndpointQuadraticControl u sliceBad ρ K t) (hxQ : x ∈ sourceOpenCube n 1) (hxE : x ∉ upperContactEstimateTotalBadSet u sliceBad t) : HasSourceCubeAffineRemainderQuadraticBound n u x (frechetGradient u x) (K * ↑n + (sourceCubeOscillation n u / (ρ / √↑n) ^ 2 + sourceCubeOscillation n u / (ρ / √↑n)))

Source-good-point pointwise affine-remainder estimate, with the coordinate endpoint bounds derived from the abstract non-bad slice condition.

theorem AleksandrovDifferentiability.upperContactOpeningBadSet_subset_totalBadSet_of_sliceEndpointControl {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {ρ K t : ℝ} (hn : 1 ≤ n) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK : 0 ≤ K) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hcontrol : CoordinateSliceEndpointQuadraticControl u sliceBad ρ K t) : upperContactOpeningBadSet n u (2 * (K * ↑n + (sourceCubeOscillation n u / (ρ / √↑n) ^ 2 + sourceCubeOscillation n u / (ρ / √↑n)))) ⊆ upperContactEstimateTotalBadSet u sliceBad t

Inclusion half of the source upper-contact estimate, assuming the abstract slice bad predicate has the one-dimensional endpoint-control property. The factor 2 converts the source-style K * ‖y - x‖^2 affine-remainder bound to the project's opening convention.

theorem AleksandrovDifferentiability.upperContactOpeningBadSet_subset_totalBadSet_of_sliceEndpointControl_of_le {n : ℕ} {u : SourceCubeSpace n → ℝ} {sliceBad : CoordinateSliceBadPredicate n} {ρ K t A : ℝ} (hn : 1 ≤ n) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK : 0 ≤ K) (hu : ConvexOn ℝ (sourceOpenCube n 3) u) (hbounded : BoundedOn (sourceOpenCube n 3) u) (hcontrol : CoordinateSliceEndpointQuadraticControl u sliceBad ρ K t) (hA : 2 * (K * ↑n + (sourceCubeOscillation n u / (ρ / √↑n) ^ 2 + sourceCubeOscillation n u / (ρ / √↑n))) ≤ A) : upperContactOpeningBadSet n u A ⊆ upperContactEstimateTotalBadSet u sliceBad t

Variant of upperContactOpeningBadSet_subset_totalBadSet_of_sliceEndpointControl with a larger externally supplied opening threshold. This is the constant-absorption form needed when the final dimensional constant is chosen after combining the measure and inclusion estimates.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_sliceEndpointControl {n : ℕ} {C ρ : ℝ} (hC_nonneg : 0 ≤ C) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hslice : ∀ (u : SourceCubeSpace n → ℝ) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → ∃ (sliceBad : CoordinateSliceBadPredicate n) (K : ℝ), 0 ≤ K ∧ CoordinateSliceEndpointQuadraticControl u sliceBad ρ K t ∧ MeasureTheory.volume (upperContactEstimateTotalBadSet u sliceBad t) ≤ ENNReal.ofReal (C * sourceCubeOscillation n u / t) ∧ 2 * (K * ↑n + (sourceCubeOscillation n u / (ρ / √↑n) ^ 2 + sourceCubeOscillation n u / (ρ / √↑n))) ≤ C * (t + sourceCubeOscillation n u)) : ConvexUpperContactEstimateDecompositionStatement n

Assembly theorem for the upper-contact estimate decomposition from a source-route coordinate-slice construction. A future maximal-function proof should instantiate sliceBad and provide:

• endpoint quadratic control outside the slice bad sets,
• the Fubini/weak-type measure bound for E(t), and
• the dimensional constant inequality comparing the source pointwise opening estimate with C * (t + osc).