Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-05 17:02 96e43cce

View on Github →

chore(measure_theory/measure/finite_measure_weak_convergence): Split one file to three. (#17332) Split the file measure_theory/measure/finite_measure_weak_convergence.lean into three files in the same folder: finite_measure.lean, probability_measure.lean, and portmanteau.lean.

Estimated changes

Created src/measure_theory/measure/finite_measure.lean

added theorem bounded_continuous_function.integral_eq_integral_nnreal_part_sub

added theorem bounded_continuous_function.nnreal.to_ennreal_comp_measurable

added theorem bounded_continuous_function.nnreal.to_real_lintegral_eq_integral

added theorem filter.tendsto.mass

added theorem measure_theory.finite_measure.coe_add

added def measure_theory.finite_measure.coe_add_monoid_hom

added theorem measure_theory.finite_measure.coe_fn_add

added theorem measure_theory.finite_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure

added theorem measure_theory.finite_measure.coe_fn_smul

added theorem measure_theory.finite_measure.coe_fn_smul_apply

added theorem measure_theory.finite_measure.coe_fn_zero

added theorem measure_theory.finite_measure.coe_injective

added theorem measure_theory.finite_measure.coe_smul

added theorem measure_theory.finite_measure.coe_to_weak_dual_bcnn

added theorem measure_theory.finite_measure.coe_zero

added theorem measure_theory.finite_measure.continuous_mass

added theorem measure_theory.finite_measure.continuous_test_against_nn_eval

added theorem measure_theory.finite_measure.ennreal_coe_fn_eq_coe_fn_to_measure

added theorem measure_theory.finite_measure.ennreal_mass

added theorem measure_theory.finite_measure.extensionality

added theorem measure_theory.finite_measure.integrable_of_bounded_continuous_to_nnreal

added theorem measure_theory.finite_measure.integrable_of_bounded_continuous_to_real

added theorem measure_theory.finite_measure.lintegral_lt_top_of_bounded_continuous_to_real

added def measure_theory.finite_measure.mass

added theorem measure_theory.finite_measure.mass_nonzero_iff

added theorem measure_theory.finite_measure.mass_zero_iff

added theorem measure_theory.finite_measure.smul_test_against_nn_apply

added theorem measure_theory.finite_measure.tendsto_iff_forall_integral_tendsto

added theorem measure_theory.finite_measure.tendsto_iff_forall_lintegral_tendsto

added theorem measure_theory.finite_measure.tendsto_iff_forall_test_against_nn_tendsto

added theorem measure_theory.finite_measure.tendsto_iff_forall_to_weak_dual_bcnn_tendsto

added theorem measure_theory.finite_measure.tendsto_iff_weak_star_tendsto

added theorem measure_theory.finite_measure.tendsto_lintegral_nn_filter_of_le_const

added theorem measure_theory.finite_measure.tendsto_lintegral_nn_of_le_const

added theorem measure_theory.finite_measure.tendsto_of_forall_integral_tendsto

added theorem measure_theory.finite_measure.tendsto_test_against_nn_filter_of_le_const

added theorem measure_theory.finite_measure.tendsto_test_against_nn_of_le_const

added theorem measure_theory.finite_measure.tendsto_zero_of_tendsto_zero_mass

added theorem measure_theory.finite_measure.tendsto_zero_test_against_nn_of_tendsto_zero_mass

added def measure_theory.finite_measure.test_against_nn

added theorem measure_theory.finite_measure.test_against_nn_add

added theorem measure_theory.finite_measure.test_against_nn_coe_eq

added theorem measure_theory.finite_measure.test_against_nn_const

added theorem measure_theory.finite_measure.test_against_nn_lipschitz

added theorem measure_theory.finite_measure.test_against_nn_lipschitz_estimate

added theorem measure_theory.finite_measure.test_against_nn_mono

added theorem measure_theory.finite_measure.test_against_nn_one

added theorem measure_theory.finite_measure.test_against_nn_smul

added theorem measure_theory.finite_measure.test_against_nn_zero

added def measure_theory.finite_measure.to_weak_dual_bcnn

added theorem measure_theory.finite_measure.to_weak_dual_bcnn_apply

added theorem measure_theory.finite_measure.to_weak_dual_bcnn_continuous

added theorem measure_theory.finite_measure.val_eq_to_measure

added theorem measure_theory.finite_measure.zero.mass

added theorem measure_theory.finite_measure.zero.test_against_nn

added theorem measure_theory.finite_measure.zero.test_against_nn_apply

added def measure_theory.finite_measure

added theorem measure_theory.lintegral_lt_top_of_bounded_continuous_to_nnreal

Deleted src/measure_theory/measure/finite_measure_weak_convergence.lean

deleted theorem bounded_continuous_function.integral_eq_integral_nnreal_part_sub

deleted theorem bounded_continuous_function.nnreal.to_ennreal_comp_measurable

deleted theorem bounded_continuous_function.nnreal.to_real_lintegral_eq_integral

deleted theorem filter.tendsto.mass

deleted theorem measure_theory.finite_measure.average_eq_integral_normalize

deleted theorem measure_theory.finite_measure.coe_add

deleted def measure_theory.finite_measure.coe_add_monoid_hom

deleted theorem measure_theory.finite_measure.coe_fn_add

deleted theorem measure_theory.finite_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure

deleted theorem measure_theory.finite_measure.coe_fn_smul

deleted theorem measure_theory.finite_measure.coe_fn_smul_apply

deleted theorem measure_theory.finite_measure.coe_fn_zero

deleted theorem measure_theory.finite_measure.coe_injective

deleted theorem measure_theory.finite_measure.coe_normalize_eq_of_nonzero

deleted theorem measure_theory.finite_measure.coe_smul

deleted theorem measure_theory.finite_measure.coe_to_weak_dual_bcnn

deleted theorem measure_theory.finite_measure.coe_zero

deleted theorem measure_theory.finite_measure.continuous_mass

deleted theorem measure_theory.finite_measure.continuous_test_against_nn_eval

deleted theorem measure_theory.finite_measure.ennreal_coe_fn_eq_coe_fn_to_measure

deleted theorem measure_theory.finite_measure.ennreal_mass

deleted theorem measure_theory.finite_measure.extensionality

deleted theorem measure_theory.finite_measure.integrable_of_bounded_continuous_to_nnreal

deleted theorem measure_theory.finite_measure.integrable_of_bounded_continuous_to_real

deleted theorem measure_theory.finite_measure.limsup_measure_closed_le_of_tendsto

deleted theorem measure_theory.finite_measure.lintegral_lt_top_of_bounded_continuous_to_real

deleted def measure_theory.finite_measure.mass

deleted theorem measure_theory.finite_measure.mass_nonzero_iff

deleted theorem measure_theory.finite_measure.mass_zero_iff

deleted def measure_theory.finite_measure.normalize

deleted theorem measure_theory.finite_measure.normalize_eq_inv_mass_smul_of_nonzero

deleted theorem measure_theory.finite_measure.normalize_eq_of_nonzero

deleted theorem measure_theory.finite_measure.normalize_test_against_nn

deleted theorem measure_theory.finite_measure.self_eq_mass_mul_normalize

deleted theorem measure_theory.finite_measure.self_eq_mass_smul_normalize

deleted theorem measure_theory.finite_measure.smul_test_against_nn_apply

deleted theorem measure_theory.finite_measure.tendsto_iff_forall_integral_tendsto

deleted theorem measure_theory.finite_measure.tendsto_iff_forall_lintegral_tendsto

deleted theorem measure_theory.finite_measure.tendsto_iff_forall_test_against_nn_tendsto

deleted theorem measure_theory.finite_measure.tendsto_iff_forall_to_weak_dual_bcnn_tendsto

deleted theorem measure_theory.finite_measure.tendsto_iff_weak_star_tendsto

deleted theorem measure_theory.finite_measure.tendsto_lintegral_nn_filter_of_le_const

deleted theorem measure_theory.finite_measure.tendsto_lintegral_nn_of_le_const

deleted theorem measure_theory.finite_measure.tendsto_normalize_iff_tendsto

deleted theorem measure_theory.finite_measure.tendsto_normalize_of_tendsto

deleted theorem measure_theory.finite_measure.tendsto_normalize_test_against_nn_of_tendsto

deleted theorem measure_theory.finite_measure.tendsto_of_forall_integral_tendsto

deleted theorem measure_theory.finite_measure.tendsto_of_tendsto_normalize_test_against_nn_of_tendsto_mass

deleted theorem measure_theory.finite_measure.tendsto_test_against_nn_filter_of_le_const

deleted theorem measure_theory.finite_measure.tendsto_test_against_nn_of_le_const

deleted theorem measure_theory.finite_measure.tendsto_test_against_nn_of_tendsto_normalize_test_against_nn_of_tendsto_mass

deleted theorem measure_theory.finite_measure.tendsto_zero_of_tendsto_zero_mass

deleted theorem measure_theory.finite_measure.tendsto_zero_test_against_nn_of_tendsto_zero_mass

deleted def measure_theory.finite_measure.test_against_nn

deleted theorem measure_theory.finite_measure.test_against_nn_add

deleted theorem measure_theory.finite_measure.test_against_nn_coe_eq

deleted theorem measure_theory.finite_measure.test_against_nn_const

deleted theorem measure_theory.finite_measure.test_against_nn_eq_mass_mul

deleted theorem measure_theory.finite_measure.test_against_nn_lipschitz

deleted theorem measure_theory.finite_measure.test_against_nn_lipschitz_estimate

deleted theorem measure_theory.finite_measure.test_against_nn_mono

deleted theorem measure_theory.finite_measure.test_against_nn_one

deleted theorem measure_theory.finite_measure.test_against_nn_smul

deleted theorem measure_theory.finite_measure.test_against_nn_zero

deleted def measure_theory.finite_measure.to_weak_dual_bcnn

deleted theorem measure_theory.finite_measure.to_weak_dual_bcnn_apply

deleted theorem measure_theory.finite_measure.to_weak_dual_bcnn_continuous

deleted theorem measure_theory.finite_measure.val_eq_to_measure

deleted theorem measure_theory.finite_measure.zero.mass

deleted theorem measure_theory.finite_measure.zero.test_against_nn

deleted theorem measure_theory.finite_measure.zero.test_against_nn_apply

deleted def measure_theory.finite_measure

deleted theorem measure_theory.le_measure_compl_liminf_of_limsup_measure_le

deleted theorem measure_theory.le_measure_liminf_of_limsup_measure_compl_le

deleted theorem measure_theory.limsup_measure_closed_le_iff_liminf_measure_open_ge

deleted theorem measure_theory.limsup_measure_compl_le_of_le_liminf_measure

deleted theorem measure_theory.limsup_measure_le_of_le_liminf_measure_compl

deleted theorem measure_theory.lintegral_lt_top_of_bounded_continuous_to_nnreal

deleted theorem measure_theory.measure_of_cont_bdd_of_tendsto_filter_indicator

deleted theorem measure_theory.measure_of_cont_bdd_of_tendsto_indicator

deleted theorem measure_theory.probability_measure.coe_comp_to_finite_measure_eq_coe

deleted theorem measure_theory.probability_measure.coe_fn_comp_to_finite_measure_eq_coe_fn

deleted theorem measure_theory.probability_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure

deleted theorem measure_theory.probability_measure.coe_fn_univ

deleted theorem measure_theory.probability_measure.coe_injective

deleted theorem measure_theory.probability_measure.coe_to_weak_dual_bcnn

deleted theorem measure_theory.probability_measure.continuous_test_against_nn_eval

deleted theorem measure_theory.probability_measure.ennreal_coe_fn_eq_coe_fn_to_measure

deleted theorem measure_theory.probability_measure.extensionality

deleted theorem measure_theory.probability_measure.le_liminf_measure_open_of_tendsto

deleted theorem measure_theory.probability_measure.limsup_measure_closed_le_of_tendsto

deleted theorem measure_theory.probability_measure.mass_to_finite_measure

deleted theorem measure_theory.probability_measure.tendsto_iff_forall_integral_tendsto

deleted theorem measure_theory.probability_measure.tendsto_iff_forall_lintegral_tendsto

deleted theorem measure_theory.probability_measure.tendsto_measure_of_null_frontier_of_tendsto'

deleted theorem measure_theory.probability_measure.tendsto_measure_of_null_frontier_of_tendsto

deleted theorem measure_theory.probability_measure.tendsto_nhds_iff_to_finite_measures_tendsto_nhds

deleted theorem measure_theory.probability_measure.test_against_nn_lipschitz

deleted def measure_theory.probability_measure.to_finite_measure

deleted theorem measure_theory.probability_measure.to_finite_measure_continuous

deleted theorem measure_theory.probability_measure.to_finite_measure_embedding

deleted theorem measure_theory.probability_measure.to_finite_measure_nonzero

deleted def measure_theory.probability_measure.to_weak_dual_bcnn

deleted theorem measure_theory.probability_measure.to_weak_dual_bcnn_apply

deleted theorem measure_theory.probability_measure.to_weak_dual_bcnn_continuous

deleted theorem measure_theory.probability_measure.val_eq_to_measure

deleted def measure_theory.probability_measure

deleted theorem measure_theory.tendsto_lintegral_thickened_indicator_of_is_closed

deleted theorem measure_theory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le

deleted theorem measure_theory.tendsto_measure_of_null_frontier

deleted theorem probability_measure.to_finite_measure_normalize_eq_self

Created src/measure_theory/measure/portmanteau.lean

added theorem measure_theory.finite_measure.limsup_measure_closed_le_of_tendsto

added theorem measure_theory.le_measure_compl_liminf_of_limsup_measure_le

added theorem measure_theory.le_measure_liminf_of_limsup_measure_compl_le

added theorem measure_theory.limsup_measure_closed_le_iff_liminf_measure_open_ge

added theorem measure_theory.limsup_measure_compl_le_of_le_liminf_measure

added theorem measure_theory.limsup_measure_le_of_le_liminf_measure_compl

added theorem measure_theory.measure_of_cont_bdd_of_tendsto_filter_indicator

added theorem measure_theory.measure_of_cont_bdd_of_tendsto_indicator

added theorem measure_theory.probability_measure.le_liminf_measure_open_of_tendsto

added theorem measure_theory.probability_measure.limsup_measure_closed_le_of_tendsto

added theorem measure_theory.probability_measure.tendsto_measure_of_null_frontier_of_tendsto'

added theorem measure_theory.probability_measure.tendsto_measure_of_null_frontier_of_tendsto

added theorem measure_theory.tendsto_lintegral_thickened_indicator_of_is_closed

added theorem measure_theory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le

added theorem measure_theory.tendsto_measure_of_null_frontier

Created src/measure_theory/measure/probability_measure.lean

added theorem measure_theory.finite_measure.average_eq_integral_normalize

added theorem measure_theory.finite_measure.coe_normalize_eq_of_nonzero

added def measure_theory.finite_measure.normalize

added theorem measure_theory.finite_measure.normalize_eq_inv_mass_smul_of_nonzero

added theorem measure_theory.finite_measure.normalize_eq_of_nonzero

added theorem measure_theory.finite_measure.normalize_test_against_nn

added theorem measure_theory.finite_measure.self_eq_mass_mul_normalize

added theorem measure_theory.finite_measure.self_eq_mass_smul_normalize

added theorem measure_theory.finite_measure.tendsto_normalize_iff_tendsto

added theorem measure_theory.finite_measure.tendsto_normalize_of_tendsto

added theorem measure_theory.finite_measure.tendsto_normalize_test_against_nn_of_tendsto

added theorem measure_theory.finite_measure.tendsto_of_tendsto_normalize_test_against_nn_of_tendsto_mass

added theorem measure_theory.finite_measure.tendsto_test_against_nn_of_tendsto_normalize_test_against_nn_of_tendsto_mass

added theorem measure_theory.finite_measure.test_against_nn_eq_mass_mul

added theorem measure_theory.probability_measure.coe_comp_to_finite_measure_eq_coe

added theorem measure_theory.probability_measure.coe_fn_comp_to_finite_measure_eq_coe_fn

added theorem measure_theory.probability_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure

added theorem measure_theory.probability_measure.coe_fn_univ

added theorem measure_theory.probability_measure.coe_injective

added theorem measure_theory.probability_measure.coe_to_weak_dual_bcnn

added theorem measure_theory.probability_measure.continuous_test_against_nn_eval

added theorem measure_theory.probability_measure.ennreal_coe_fn_eq_coe_fn_to_measure

added theorem measure_theory.probability_measure.extensionality

added theorem measure_theory.probability_measure.mass_to_finite_measure

added theorem measure_theory.probability_measure.tendsto_iff_forall_integral_tendsto

added theorem measure_theory.probability_measure.tendsto_iff_forall_lintegral_tendsto

added theorem measure_theory.probability_measure.tendsto_nhds_iff_to_finite_measures_tendsto_nhds

added theorem measure_theory.probability_measure.test_against_nn_lipschitz

added def measure_theory.probability_measure.to_finite_measure

added theorem measure_theory.probability_measure.to_finite_measure_continuous

added theorem measure_theory.probability_measure.to_finite_measure_embedding

added theorem measure_theory.probability_measure.to_finite_measure_nonzero

added def measure_theory.probability_measure.to_weak_dual_bcnn

added theorem measure_theory.probability_measure.to_weak_dual_bcnn_apply

added theorem measure_theory.probability_measure.to_weak_dual_bcnn_continuous

added theorem measure_theory.probability_measure.val_eq_to_measure

added def measure_theory.probability_measure

added theorem probability_measure.to_finite_measure_normalize_eq_self