Commit 2023-06-07 00:35 b1e3dbef

View on Github →

feat: port MeasureTheory.Measure.FiniteMeasure (#4747)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem BoundedContinuousFunction.NNReal.coe_ennreal_comp_measurable

added theorem BoundedContinuousFunction.NNReal.toReal_lintegral_eq_integral

added theorem BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub

added theorem Filter.Tendsto.mass

added theorem MeasureTheory.FiniteMeasure.apply_mono

added theorem MeasureTheory.FiniteMeasure.coeFn_add

added theorem MeasureTheory.FiniteMeasure.coeFn_smul

added theorem MeasureTheory.FiniteMeasure.coeFn_smul_apply

added theorem MeasureTheory.FiniteMeasure.coeFn_zero

added theorem MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN

added theorem MeasureTheory.FiniteMeasure.continuous_mass

added theorem MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval

added theorem MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure

added theorem MeasureTheory.FiniteMeasure.ennreal_mass

added theorem MeasureTheory.FiniteMeasure.eq_of_forall_apply_eq

added theorem MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq

added theorem MeasureTheory.FiniteMeasure.integrable_of_boundedContinuous_to_nnreal

added theorem MeasureTheory.FiniteMeasure.integrable_of_boundedContinuous_to_real

added theorem MeasureTheory.FiniteMeasure.lintegral_lt_top_of_boundedContinuous_to_real

added def MeasureTheory.FiniteMeasure.mass

added theorem MeasureTheory.FiniteMeasure.mass_nonzero_iff

added theorem MeasureTheory.FiniteMeasure.mass_zero_iff

added def MeasureTheory.FiniteMeasure.restrict

added theorem MeasureTheory.FiniteMeasure.restrict_apply

added theorem MeasureTheory.FiniteMeasure.restrict_apply_measure

added theorem MeasureTheory.FiniteMeasure.restrict_eq_zero_iff

added theorem MeasureTheory.FiniteMeasure.restrict_mass

added theorem MeasureTheory.FiniteMeasure.restrict_measure_eq

added theorem MeasureTheory.FiniteMeasure.restrict_nonzero_iff

added theorem MeasureTheory.FiniteMeasure.smul_testAgainstNN_apply

added theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_iff_weak_star_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const

added theorem MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_of_le_const

added theorem MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const

added theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_le_const

added theorem MeasureTheory.FiniteMeasure.tendsto_zero_of_tendsto_zero_mass

added theorem MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass

added def MeasureTheory.FiniteMeasure.testAgainstNN

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_add

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_const

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz_estimate

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_mono

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_one

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_smul

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_zero

added def MeasureTheory.FiniteMeasure.toMeasure

added def MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom

added theorem MeasureTheory.FiniteMeasure.toMeasure_add

added theorem MeasureTheory.FiniteMeasure.toMeasure_injective

added theorem MeasureTheory.FiniteMeasure.toMeasure_smul

added theorem MeasureTheory.FiniteMeasure.toMeasure_zero

added def MeasureTheory.FiniteMeasure.toWeakDualBCNN

added theorem MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply

added theorem MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous

added theorem MeasureTheory.FiniteMeasure.val_eq_toMeasure

added theorem MeasureTheory.FiniteMeasure.zero_mass

added theorem MeasureTheory.FiniteMeasure.zero_testAgainstNN

added theorem MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply

added def MeasureTheory.FiniteMeasure

added theorem MeasureTheory.lintegral_lt_top_of_boundedContinuous_to_nnreal