Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Measure assembly for source-cube bad sets #
This file contains finite-union measure bookkeeping for the source upper-contact estimate. The analytic estimates for individual coordinate slices live elsewhere; this module packages the common finite-union step.
theorem
AleksandrovDifferentiability.volume_upperContactEstimateTotalBadSet_le_nonDifferentiable_add_sum_coordinate
{n : ℕ}
{u : SourceCubeSpace n → ℝ}
{sliceBad : CoordinateSliceBadPredicate n}
{t : ℝ}
:
MeasureTheory.volume (upperContactEstimateTotalBadSet u sliceBad t) ≤ MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) + ∑ i : Fin n, MeasureTheory.volume (coordinateSliceBadSet sliceBad i t)
The total source bad set is bounded by the non-differentiability bad set plus the sum of the coordinate bad-set measures.
theorem
AleksandrovDifferentiability.volume_upperContactEstimateTotalBadSet_le_sum_of_coordinate_bounds
{n : ℕ}
{u : SourceCubeSpace n → ℝ}
{sliceBad : CoordinateSliceBadPredicate n}
{t : ℝ}
{B : Fin n → ENNReal}
(hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0)
(hcoord : ∀ (i : Fin n), MeasureTheory.volume (coordinateSliceBadSet sliceBad i t) ≤ B i)
:
If the non-differentiability bad set is null and each coordinate bad set has a prescribed bound, then the total source bad set is bounded by the finite sum of those bounds.
theorem
AleksandrovDifferentiability.volume_upperContactEstimateTotalBadSet_le_card_mul_of_coordinate_bound
{n : ℕ}
{u : SourceCubeSpace n → ℝ}
{sliceBad : CoordinateSliceBadPredicate n}
{t : ℝ}
{B : ENNReal}
(hdiff : MeasureTheory.volume (sourceOpenCube n 1 \ firstOrderDifferentiabilitySet u) = 0)
(hcoord : ∀ (i : Fin n), MeasureTheory.volume (coordinateSliceBadSet sliceBad i t) ≤ B)
:
Constant-bound version of
volume_upperContactEstimateTotalBadSet_le_sum_of_coordinate_bounds.