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

Coordinate-slice maximal estimate assembly

theorem AleksandrovDifferentiability.coordinateSlice_measureConstant_bound {n : ℕ} {Ccoord Cmeasure osc t : ℝ} (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hosc : 0 ≤ osc) (ht : 0 < t) : ↑n * ENNReal.ofReal (Ccoord * osc / t) ≤ ENNReal.ofReal (Cmeasure * osc / t)

theorem AleksandrovDifferentiability.CoordinateSliceMaximalTotalBadSetEstimate.of_fubiniEstimate_of_measureConstant {n : ℕ} {u : SourceCubeSpace n → ℝ} {μslice : CoordinateSliceMeasureFamily n} {Cmax Ccoord Cmeasure t : ℝ} (hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0) (hmass : CoordinateSliceSourceMassBound μslice (sourceCubeOscillation n u)) (hmax : LocalizedMaximalEstimateStatement Cmax) (ht : 0 < t) (hfubini : CoordinateSliceMaximalFubiniEstimate μslice (2 * Cmax) Ccoord (sourceCubeOscillation n u) t) (hmeasure : ↑n * Ccoord ≤ Cmeasure) (hbounded : BoundedOn (sourceOpenCube n 3) u) : CoordinateSliceMaximalTotalBadSetEstimate u μslice Cmeasure t

Version of CoordinateSliceMaximalTotalBadSetEstimate.of_fubiniEstimate where the scalar measure-constant comparison is supplied in real-valued coefficient form.

theorem AleksandrovDifferentiability.two_mul_add_le_mul_add_of_two_mul_le {A B C t osc : ℝ} (hA : 2 * A ≤ C) (hB : 2 * B ≤ C) (ht : 0 ≤ t) (hosc : 0 ≤ osc) : 2 * (A * t + B * osc) ≤ C * (t + osc)

Two-term constant absorption used in the source upper-contact estimate: if a single constant dominates the t coefficient and the oscillation coefficient separately, then it dominates their sum.

theorem AleksandrovDifferentiability.maximalSlice_threshold_le_of_coefficient_bounds {n : ℕ} {C ρ K₀ t osc : ℝ} (hK : 2 * (K₀ * ↑n) ≤ C) (hoscCoeff : 2 * (1 / (ρ / √↑n) ^ 2 + 1 / (ρ / √↑n)) ≤ C) (ht : 0 ≤ t) (hosc : 0 ≤ osc) : 2 * (K₀ * t * ↑n + (osc / (ρ / √↑n) ^ 2 + osc / (ρ / √↑n))) ≤ C * (t + osc)

Constant absorption for the concrete maximal-slice threshold expression.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_maximalSliceControls {n : ℕ} {C ρ K₀ : ℝ} (hC_nonneg : 0 ≤ C) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK₀ : 0 ≤ K₀) (hslice : ∀ (u : SourceCubeSpace n → ℝ) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → ∃ (μslice : CoordinateSliceMeasureFamily n), CoordinateSliceOneDimEndpointControl u μslice ρ K₀ ∧ CoordinateSliceMaximalTotalBadSetEstimate u μslice C t ∧ 2 * (K₀ * t * ↑n + (sourceCubeOscillation n u / (ρ / √↑n) ^ 2 + sourceCubeOscillation n u / (ρ / √↑n))) ≤ C * (t + sourceCubeOscillation n u)) : ConvexUpperContactEstimateDecompositionStatement n

Source-route assembly from concrete localized-maximal slice controls to the packaged upper-contact decomposition. After this theorem, the remaining work is to construct the slice second-derivative measures, prove their one-dimensional endpoint control, prove the concrete total-bad-set estimate, and choose dimensional constants.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_maximalSliceControls_of_coefficients {n : ℕ} {C ρ K₀ : ℝ} (hC_nonneg : 0 ≤ C) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK₀ : 0 ≤ K₀) (hKcoeff : 2 * (K₀ * ↑n) ≤ C) (hoscCoeff : 2 * (1 / (ρ / √↑n) ^ 2 + 1 / (ρ / √↑n)) ≤ C) (hslice : ∀ (u : SourceCubeSpace n → ℝ) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → ∃ (μslice : CoordinateSliceMeasureFamily n), CoordinateSliceOneDimEndpointControl u μslice ρ K₀ ∧ CoordinateSliceMaximalTotalBadSetEstimate u μslice C t) : ConvexUpperContactEstimateDecompositionStatement n

Coefficient-bound version of ConvexUpperContactEstimateDecompositionStatement.of_maximalSliceControls. This is the most convenient source-route entry point after proving the concrete analytic estimates: the final pointwise threshold inequality follows from two scalar coefficient inequalities and nonnegativity of t and osc.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_maximalSliceControls_of_measureConstant {n : ℕ} {C Cmeasure ρ K₀ : ℝ} (hC_nonneg : 0 ≤ C) (hmeasure_le : Cmeasure ≤ C) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK₀ : 0 ≤ K₀) (hKcoeff : 2 * (K₀ * ↑n) ≤ C) (hoscCoeff : 2 * (1 / (ρ / √↑n) ^ 2 + 1 / (ρ / √↑n)) ≤ C) (hslice : ∀ (u : SourceCubeSpace n → ℝ) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → ∃ (μslice : CoordinateSliceMeasureFamily n), CoordinateSliceOneDimEndpointControl u μslice ρ K₀ ∧ CoordinateSliceMaximalTotalBadSetEstimate u μslice Cmeasure t) : ConvexUpperContactEstimateDecompositionStatement n

Version of ConvexUpperContactEstimateDecompositionStatement.of_maximalSliceControls_of_coefficients where the concrete total-bad-set estimate is first proved with a smaller measure constant Cmeasure, then enlarged to the final dimensional constant C.

theorem AleksandrovDifferentiability.ConvexUpperContactEstimateDecompositionStatement.of_maximalSliceControls_with_chosenConstant {n : ℕ} {Cmeasure ρ K₀ : ℝ} (hCmeasure_nonneg : 0 ≤ Cmeasure) (hρ : 0 < ρ) (hρ_le_one : ρ ≤ 1) (hK₀ : 0 ≤ K₀) (hslice : ∀ (u : SourceCubeSpace n → ℝ) (t : ℝ), 0 < t → BoundedOn (sourceOpenCube n 3) u → ConvexOn ℝ (sourceOpenCube n 3) u → ∃ (μslice : CoordinateSliceMeasureFamily n), CoordinateSliceOneDimEndpointControl u μslice ρ K₀ ∧ CoordinateSliceMaximalTotalBadSetEstimate u μslice Cmeasure t) : ConvexUpperContactEstimateDecompositionStatement n

Fully packaged constant-choice version of the concrete maximal-slice route. The final dimensional constant is chosen as the maximum of the measure constant and the two scalar coefficients needed for threshold absorption.