Commit 2022-10-30 08:20 8315f58e

View on Github →

chore(measure_theory/measure/finite_measure_weak_convergence): Change to probability theory notations. (#17231) Change notations of the underlying measurable spaces from α to Ω.

Estimated changes

Modified src/measure_theory/measure/finite_measure_weak_convergence.lean

modified theorem bounded_continuous_function.nnreal.to_ennreal_comp_measurable

modified theorem measure_theory.finite_measure.coe_add

modified def measure_theory.finite_measure.coe_add_monoid_hom

modified theorem measure_theory.finite_measure.coe_fn_add

modified theorem measure_theory.finite_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure

modified theorem measure_theory.finite_measure.coe_fn_smul

modified theorem measure_theory.finite_measure.coe_injective

modified theorem measure_theory.finite_measure.coe_normalize_eq_of_nonzero

modified theorem measure_theory.finite_measure.coe_smul

modified theorem measure_theory.finite_measure.coe_to_weak_dual_bcnn

modified theorem measure_theory.finite_measure.coe_zero

modified theorem measure_theory.finite_measure.continuous_mass

modified theorem measure_theory.finite_measure.continuous_test_against_nn_eval

modified theorem measure_theory.finite_measure.ennreal_coe_fn_eq_coe_fn_to_measure

modified theorem measure_theory.finite_measure.ennreal_mass

modified theorem measure_theory.finite_measure.extensionality

modified def measure_theory.finite_measure.mass

modified theorem measure_theory.finite_measure.mass_nonzero_iff

modified theorem measure_theory.finite_measure.mass_zero_iff

modified def measure_theory.finite_measure.normalize

modified theorem measure_theory.finite_measure.normalize_eq_of_nonzero

modified theorem measure_theory.finite_measure.normalize_test_against_nn

modified theorem measure_theory.finite_measure.self_eq_mass_mul_normalize

modified theorem measure_theory.finite_measure.smul_test_against_nn_apply

modified theorem measure_theory.finite_measure.tendsto_lintegral_nn_of_le_const

modified theorem measure_theory.finite_measure.tendsto_test_against_nn_of_le_const

modified def measure_theory.finite_measure.test_against_nn

modified theorem measure_theory.finite_measure.test_against_nn_add

modified theorem measure_theory.finite_measure.test_against_nn_coe_eq

modified theorem measure_theory.finite_measure.test_against_nn_const

modified theorem measure_theory.finite_measure.test_against_nn_eq_mass_mul

modified theorem measure_theory.finite_measure.test_against_nn_lipschitz

modified theorem measure_theory.finite_measure.test_against_nn_lipschitz_estimate

modified theorem measure_theory.finite_measure.test_against_nn_mono

modified theorem measure_theory.finite_measure.test_against_nn_one

modified theorem measure_theory.finite_measure.test_against_nn_zero

modified def measure_theory.finite_measure.to_weak_dual_bcnn

modified theorem measure_theory.finite_measure.to_weak_dual_bcnn_apply

modified theorem measure_theory.finite_measure.val_eq_to_measure

modified theorem measure_theory.finite_measure.zero.mass

modified theorem measure_theory.finite_measure.zero.test_against_nn

modified theorem measure_theory.finite_measure.zero.test_against_nn_apply

modified def measure_theory.finite_measure

modified theorem measure_theory.probability_measure.coe_comp_to_finite_measure_eq_coe

modified theorem measure_theory.probability_measure.coe_fn_comp_to_finite_measure_eq_coe_fn

modified theorem measure_theory.probability_measure.coe_fn_eq_to_nnreal_coe_fn_to_measure

modified theorem measure_theory.probability_measure.coe_fn_univ

modified theorem measure_theory.probability_measure.coe_injective

modified theorem measure_theory.probability_measure.coe_to_weak_dual_bcnn

modified theorem measure_theory.probability_measure.continuous_test_against_nn_eval

modified theorem measure_theory.probability_measure.ennreal_coe_fn_eq_coe_fn_to_measure

modified theorem measure_theory.probability_measure.extensionality

modified theorem measure_theory.probability_measure.mass_to_finite_measure

modified theorem measure_theory.probability_measure.test_against_nn_lipschitz

modified def measure_theory.probability_measure.to_finite_measure

modified theorem measure_theory.probability_measure.to_finite_measure_embedding

modified theorem measure_theory.probability_measure.to_finite_measure_nonzero

modified def measure_theory.probability_measure.to_weak_dual_bcnn

modified theorem measure_theory.probability_measure.to_weak_dual_bcnn_apply

modified theorem measure_theory.probability_measure.val_eq_to_measure

modified def measure_theory.probability_measure