Main result
For a sequence of real-valued measurable functions converging to
zero almost everywhere on a sigma-finite measure space, there is
a conull measurable set A and a strictly positive
measurable weight h such that f_n h
converges uniformly to zero on A, and therefore
converges to zero in measure. The Lean file also records the
real-line specialization for Lebesgue measure.
- Contribution type
- New construction; Lean formalization
- Contribution
- Explicit measurable-weight construction upgrading almost-everywhere convergence on a sigma-finite measure space to conull uniformization and convergence in measure after multiplying by a strictly positive measurable weight.
- Core mechanism
- Egorov pieces, pointwise envelope, measurable cover-index weight, convergence in measure
- Lean theorem
PointwiseWeighting.exists_conull_pos_measurable_weight_uniformOn_tendstoInMeasure_of_ae_tendsto- Real-line theorem
PointwiseWeighting.real_exists_conull_pos_measurable_weight_uniformOn_tendstoInMeasure- Dominated route
PointwiseWeighting.exists_pos_measurable_weight_tendstoInMeasure_of_ae_tendsto- Lean and mathlib
- Lean 4.29.1, mathlib v4.29.1
- Build command
lake build