Commit 2023-06-04 05:44 0b92c7b7

View on Github →

style: recover Is of Foo which is ported from is_foo (#4639) I have misported is_foo to Foo because I misunderstood the rule for IsLawfulFoo. This PR recover Is of Foo which is ported from is_foo. This PR also renames some misported theorems.

Estimated changes

Modified Mathlib/Dynamics/Ergodic/Conservative.lean

Modified Mathlib/Dynamics/Ergodic/Ergodic.lean

modified theorem PreErgodic.prob_eq_zero_or_one

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

modified theorem MeasureTheory.MeasurePreserving.exists_mem_image_mem

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

added theorem Continuous.isOpenPosMeasure_map

deleted theorem Continuous.openPosMeasure_map

modified def Real.finiteSpanningSetsInIooRat

modified theorem Real.measure_ext_Ioo_rat

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

modified theorem measurable_measure_prod_mk_left_finite

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Decomposition/Jordan.lean

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

modified theorem MeasureTheory.hahn_decomposition

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae

modified theorem MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable

Modified Mathlib/MeasureTheory/Function/Egorov.lean

modified theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'

Modified Mathlib/MeasureTheory/Function/L1Space.lean

modified theorem MeasureTheory.Memℒp.integrable

modified theorem MeasureTheory.Memℒp.integrable_norm_rpow'

deleted theorem MeasureTheory.finiteMeasure_withDensity_ofReal

modified theorem MeasureTheory.hasFiniteIntegral_const

modified theorem MeasureTheory.hasFiniteIntegral_of_bounded

modified theorem MeasureTheory.integrable_average

modified theorem MeasureTheory.integrable_const

added theorem MeasureTheory.isFiniteMeasure_withDensity_ofReal

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

modified theorem AntioneOn.integrableOn_isCompact

modified theorem Antitone.locallyIntegrable

modified theorem MeasureTheory.locallyIntegrableOn_const

modified theorem MeasureTheory.locallyIntegrable_const

modified theorem Monotone.locallyIntegrable

modified theorem MonotoneOn.integrableOn_isCompact

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

modified theorem MeasureTheory.Memℒp.memℒp_of_exponent_le

modified theorem MeasureTheory.Memℒp.of_bound

modified theorem MeasureTheory.memℒp_const

modified theorem MeasureTheory.snorm'_const'

added theorem MeasureTheory.snorm'_const_of_isProbabilityMeasure

deleted theorem MeasureTheory.snorm'_const_of_probabilityMeasure

modified theorem MeasureTheory.snorm'_le_snormEssSup

modified theorem MeasureTheory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le

modified theorem MeasureTheory.snorm_le_snorm_of_exponent_le

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

modified theorem BoundedContinuousFunction.toLp_inj

modified theorem BoundedContinuousFunction.toLp_injective

modified theorem ContinuousMap.hasSum_of_hasSum_Lp

modified theorem ContinuousMap.toLp_inj

modified theorem ContinuousMap.toLp_injective

modified theorem MeasureTheory.Lp.mem_Lp_of_ae_bound

modified theorem MeasureTheory.Lp.mem_Lp_of_ae_nnnorm_bound

modified theorem MeasureTheory.Lp.mem_lp_const

modified theorem MeasureTheory.Lp.nnnorm_le_of_ae_bound

modified theorem MeasureTheory.Lp.norm_le_of_ae_bound

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

deleted theorem MeasureTheory.SimpleFunc.integrable_of_finiteMeasure

added theorem MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure

deleted theorem MeasureTheory.SimpleFunc.memℒp_of_finiteMeasure

added theorem MeasureTheory.SimpleFunc.memℒp_of_isFiniteMeasure

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

modified theorem MeasureTheory.tendstoInMeasure_iff_tendsto_Lp

modified theorem MeasureTheory.tendsto_Lp_of_tendstoInMeasure

modified theorem MeasureTheory.tendsto_Lp_of_tendsto_ae

modified theorem MeasureTheory.tendsto_Lp_of_tendsto_ae_of_meas

modified theorem MeasureTheory.uniformIntegrable_iff

modified theorem MeasureTheory.uniformIntegrable_of'

modified theorem MeasureTheory.uniformIntegrable_of

Modified Mathlib/MeasureTheory/Group/Action.lean

added theorem MeasureTheory.isLocallyFiniteMeasure_of_smulInvariant

deleted theorem MeasureTheory.locallyFiniteMeasure_of_smulInvariant

Modified Mathlib/MeasureTheory/Group/Measure.lean

deleted theorem MeasureTheory.Measure.HaarMeasure.smul

added theorem MeasureTheory.Measure.IsHaarMeasure.smul

deleted theorem MeasureTheory.Measure.haarMeasure_map

deleted theorem MeasureTheory.Measure.haarMeasure_of_isCompact_nonempty_interior

modified theorem MeasureTheory.Measure.inv_eq_self

added theorem MeasureTheory.Measure.isHaarMeasure_map

added theorem MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior

modified theorem MeasureTheory.Measure.map_div_left_ae

modified theorem MeasureTheory.Measure.map_div_left_eq_self

modified theorem MeasureTheory.Measure.map_inv_eq_self

modified theorem MeasureTheory.Measure.map_mul_right_inv_eq_self

modified theorem MeasureTheory.Measure.measurePreserving_div_left

modified theorem MeasureTheory.Measure.measurePreserving_inv

modified theorem MeasureTheory.Measure.measurePreserving_mul_right_inv

modified theorem MeasureTheory.Measure.measure_inv

modified theorem MeasureTheory.Measure.measure_preimage_inv

modified theorem MeasureTheory.MeasurePreserving.mul_left

modified theorem MeasureTheory.MeasurePreserving.mul_right

modified theorem MeasureTheory.eventually_div_right_iff

modified theorem MeasureTheory.eventually_mul_left_iff

modified theorem MeasureTheory.eventually_mul_right_iff

added theorem MeasureTheory.isMulLeftInvariant_map

added theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact

added theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular

modified theorem MeasureTheory.map_div_right_ae

modified theorem MeasureTheory.map_div_right_eq_self

modified theorem MeasureTheory.map_mul_left_ae

modified theorem MeasureTheory.map_mul_left_eq_self

modified theorem MeasureTheory.map_mul_right_ae

modified theorem MeasureTheory.map_mul_right_eq_self

modified theorem MeasureTheory.measurePreserving_div_right

modified theorem MeasureTheory.measurePreserving_mul_left

modified theorem MeasureTheory.measurePreserving_mul_right

added theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant'

added theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant

deleted theorem MeasureTheory.measure_lt_top_of_isCompact_of_mulLeftInvariant'

deleted theorem MeasureTheory.measure_lt_top_of_isCompact_of_mulLeftInvariant

added theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant

deleted theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_mulLeftInvariant

added theorem MeasureTheory.measure_pos_iff_nonempty_of_isMulLeftInvariant

deleted theorem MeasureTheory.measure_pos_iff_nonempty_of_mulLeftInvariant

modified theorem MeasureTheory.measure_preimage_mul

modified theorem MeasureTheory.measure_preimage_mul_right

added theorem MeasureTheory.measure_univ_of_isMulLeftInvariant

deleted theorem MeasureTheory.measure_univ_of_mulLeftInvariant

deleted theorem MeasureTheory.mulLeftInvariant_map

added theorem MeasureTheory.null_iff_of_isMulLeftInvariant

deleted theorem MeasureTheory.null_iff_of_mulLeftInvariant

deleted theorem MeasureTheory.openPosMeasure_of_mulLeftInvariant_of_compact

deleted theorem MeasureTheory.openPosMeasure_of_mulLeftInvariant_of_regular

Modified Mathlib/MeasureTheory/Group/Prod.lean

added theorem MeasureTheory.absolutelyContinuous_of_isMulLeftInvariant

deleted theorem MeasureTheory.absolutelyContinuous_of_mulLeftInvariant

modified theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top

modified theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero

modified theorem MeasureTheory.lintegral_lintegral_mul_inv

modified theorem MeasureTheory.measurePreserving_div_prod

modified theorem MeasureTheory.measurePreserving_mul_prod

modified theorem MeasureTheory.measurePreserving_mul_prod_inv

modified theorem MeasureTheory.measurePreserving_mul_prod_inv_right

modified theorem MeasureTheory.measurePreserving_prod_div

modified theorem MeasureTheory.measurePreserving_prod_div_swap

modified theorem MeasureTheory.measurePreserving_prod_inv_mul

modified theorem MeasureTheory.measurePreserving_prod_mul

modified theorem MeasureTheory.measurePreserving_prod_mul_right

modified theorem MeasureTheory.measurePreserving_prod_mul_swap

modified theorem MeasureTheory.measurePreserving_prod_mul_swap_right

modified theorem MeasureTheory.measure_eq_div_smul

modified theorem MeasureTheory.measure_lintegral_div_measure

modified theorem MeasureTheory.measure_mul_lintegral_eq

modified theorem MeasureTheory.measure_mul_measure_eq

modified theorem MeasureTheory.quasiMeasurePreserving_div

modified theorem MeasureTheory.quasiMeasurePreserving_div_left

modified theorem MeasureTheory.quasiMeasurePreserving_div_left_of_right_invariant

modified theorem MeasureTheory.quasiMeasurePreserving_div_of_right_invariant

modified theorem MeasureTheory.quasiMeasurePreserving_inv_of_right_invariant

modified theorem MeasureTheory.quasiMeasurePreserving_mul_left

modified theorem MeasureTheory.quasiMeasurePreserving_mul_right

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

deleted theorem MeasureTheory.exists_absolutelyContinuous_finiteMeasure

added theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure

deleted theorem MeasureTheory.finiteMeasure_withDensity

added theorem MeasureTheory.isFiniteMeasure_withDensity

modified theorem MeasureTheory.lintegral_const_lt_top

modified theorem MeasureTheory.set_lintegral_const_lt_top

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

modified theorem MeasureTheory.L1.SimpleFunc.setToL1SCLM_const

modified theorem MeasureTheory.L1.SimpleFunc.setToL1S_const

modified theorem MeasureTheory.L1.setToL1_const

modified theorem MeasureTheory.setToFun_const

Modified Mathlib/MeasureTheory/Measure/Content.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

modified theorem MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos

deleted theorem MeasureTheory.Measure.haarMeasure_eq_smul_haarMeasure

modified theorem MeasureTheory.Measure.haarMeasure_unique

added theorem MeasureTheory.Measure.isHaarMeasure_eq_smul_isHaarMeasure

added theorem MeasureTheory.Measure.regular_of_isMulLeftInvariant

deleted theorem MeasureTheory.Measure.regular_of_mulLeftInvariant

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted theorem MeasureTheory.CompactSpace.finiteMeasure

added theorem MeasureTheory.CompactSpace.isFiniteMeasure

added theorem MeasureTheory.IsProbabilityMeasure.ne_zero

deleted theorem MeasureTheory.Measure.finiteAtFilterOfFinite

added theorem MeasureTheory.Measure.finiteAtFilter_of_finite

modified theorem MeasureTheory.Measure.finiteAt_nhds

deleted theorem MeasureTheory.Measure.finiteMeasureMap

added theorem MeasureTheory.Measure.isFiniteMeasure_map

added theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_le

modified theorem MeasureTheory.Measure.le_of_add_le_add_left

deleted theorem MeasureTheory.Measure.locallyFiniteMeasure_of_le

modified theorem MeasureTheory.Measure.smul_finite

deleted theorem MeasureTheory.ProbabilityMeasure.ne_zero

modified theorem MeasureTheory.ae_eq_univ_iff_measure_eq

modified theorem MeasureTheory.ae_iff_measure_eq

modified theorem MeasureTheory.ae_mem_iff_measure_eq

modified theorem MeasureTheory.coe_measureUnivNNReal

deleted theorem MeasureTheory.finiteMeasureOfLe

added theorem MeasureTheory.isFiniteMeasure_of_le

added theorem MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts

deleted theorem MeasureTheory.isProbabilityMeasureMap

modified theorem MeasureTheory.isProbabilityMeasureSmul

added theorem MeasureTheory.isProbabilityMeasure_map

deleted theorem MeasureTheory.locallyFiniteMeasure_of_finiteMeasureOnCompacts

modified theorem MeasureTheory.measureUnivNNReal_eq_zero

modified theorem MeasureTheory.measureUnivNNReal_pos

modified theorem MeasureTheory.measure_compl_le_add_iff

modified theorem MeasureTheory.measure_compl_le_add_of_le_add

modified theorem MeasureTheory.measure_lt_top

modified theorem MeasureTheory.measure_ne_top

deleted theorem MeasureTheory.not_finiteMeasure_iff

added theorem MeasureTheory.not_isFiniteMeasure_iff

modified theorem MeasureTheory.one_le_prob_iff

modified theorem MeasureTheory.prob_add_prob_compl

modified theorem MeasureTheory.prob_compl_eq_one_iff

modified theorem MeasureTheory.prob_compl_eq_one_sub

modified theorem MeasureTheory.prob_compl_eq_zero_iff

modified theorem MeasureTheory.prob_le_one

modified theorem MeasureTheory.sigmaFinite_bot_iff

modified theorem MeasureTheory.sigmaFinite_trim_bot_iff

modified theorem MeasureTheory.summable_measure_toReal

deleted theorem finiteMeasure_iff_finiteMeasureOnCompacts_of_compactSpace

added theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace

Modified Mathlib/MeasureTheory/Measure/OpenPos.lean

modified theorem LE.le.isOpenPosMeasure

added theorem MeasureTheory.Measure.isOpenPosMeasure_smul

deleted theorem MeasureTheory.Measure.openPosMeasure_smul

Modified Mathlib/MeasureTheory/Measure/Regular.lean

modified theorem MeasureTheory.Measure.InnerRegular.weaklyRegular_of_finite

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Sub.lean

modified theorem MeasureTheory.Measure.sub_add_cancel_of_le

modified theorem MeasureTheory.Measure.sub_apply

Modified Mathlib/MeasureTheory/Measure/VectorMeasure.lean

modified def MeasureTheory.Measure.toSignedMeasure

modified theorem MeasureTheory.Measure.toSignedMeasure_add

modified theorem MeasureTheory.Measure.toSignedMeasure_apply_measurable

modified theorem MeasureTheory.Measure.toSignedMeasure_congr

modified theorem MeasureTheory.Measure.toSignedMeasure_eq_toSignedMeasure_iff

modified theorem MeasureTheory.Measure.toSignedMeasure_smul

modified theorem MeasureTheory.Measure.toSignedMeasure_sub_apply

Modified Mathlib/Probability/CondCount.lean

added theorem ProbabilityTheory.condCount_isProbabilityMeasure

deleted theorem ProbabilityTheory.condCount_probabilityMeasure

Modified Mathlib/Probability/ConditionalProbability.lean

modified theorem ProbabilityTheory.cond_add_cond_compl_eq

modified theorem ProbabilityTheory.cond_cond_eq_cond_inter

modified theorem ProbabilityTheory.cond_eq_inv_mul_cond_mul

added theorem ProbabilityTheory.cond_isProbabilityMeasure

modified theorem ProbabilityTheory.cond_mul_eq_inter

modified theorem ProbabilityTheory.cond_pos_of_inter_ne_zero

deleted theorem ProbabilityTheory.cond_probabilityMeasure

modified theorem ProbabilityTheory.cond_univ

Modified Mathlib/Probability/Independence/Basic.lean

modified theorem ProbabilityTheory.IndepSets.indep'

modified theorem ProbabilityTheory.iIndepFun.indepFun_finset

modified theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_not_mem

modified theorem ProbabilityTheory.iIndepFun.indepFun_prod

modified theorem ProbabilityTheory.iIndepFun.indepFun_prod_range_succ

modified theorem ProbabilityTheory.iIndepFun.mul

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_le_nat

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_lt

modified theorem ProbabilityTheory.iIndepSet.indep_generateFrom_of_disjoint

modified theorem ProbabilityTheory.iIndepSets.iIndep

modified theorem ProbabilityTheory.indepSet_empty_left

modified theorem ProbabilityTheory.indepSet_empty_right

modified theorem ProbabilityTheory.indepSets_piiUnionInter_of_disjoint

modified theorem ProbabilityTheory.indep_iSup_of_disjoint

Modified Mathlib/Probability/Independence/ZeroOne.lean

modified theorem ProbabilityTheory.measure_eq_zero_or_one_of_indepSetCat_self

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

modified theorem Pmf.toMeasure_eq_iff_eq_toPmf

modified theorem Pmf.toPmf_eq_iff_toMeasure_eq