Map

📁 Source: Mathlib/MeasureTheory/Measure/Map.lean

Statistics

Metric	Count
Definitions liftLinear, map, mapₗ	3
Theorems of_map_ne_zero, map_apply, map_injective, map_ae, map_apply, map_apply_eq_iff_map_symm_apply_eq, map_map_symm, map_measurableEquiv_injective, map_symm_map, le_liftLinear_apply, le_map_apply, le_map_apply_image, liftLinear_apply, liftLinear_apply₀, map_add, map_apply, map_apply_of_aemeasurable, map_apply₀, map_congr, map_def, map_eq_zero_iff, map_id, map_id', map_map, map_mono, map_ne_zero_iff, map_of_not_aemeasurable, map_smul, map_toOuterMeasure, map_zero, mapₗ_apply_of_measurable, mapₗ_congr, mapₗ_eq_zero_iff, mapₗ_mk_apply_of_aemeasurable, mapₗ_ne_zero_iff, measure_preimage_of_map_eq_self, preimage_null_of_map_null, tendsto_ae_map, ae_map_iff, ae_map_mem_range, ae_of_ae_map, mem_ae_map_iff, mem_ae_of_mem_ae_map	43
Total	46

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_map_ne_zero 📖	mathematical	—	AEMeasurable	—	not_imp_comm MeasureTheory.Measure.map_of_not_aemeasurable

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_apply 📖	mathematical	MeasurableEmbedding	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.map Set.preimage	—	le_antisymm MeasurableSet.union measurableSet_image MeasureTheory.measurableSet_toMeasurable MeasurableSet.compl measurableSet_range Set.subset_union_compl_iff_inter_subset Set.image_preimage_eq_inter_range Set.image_mono MeasureTheory.subset_toMeasurable Set.preimage_union Set.preimage_compl Set.preimage_range Set.compl_univ Set.union_empty Function.Injective.preimage_image injective MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map_apply measurable MeasureTheory.measure_toMeasurable MeasureTheory.Measure.le_map_apply Measurable.aemeasurable
map_injective 📖	mathematical	MeasurableEmbedding	MeasureTheory.Measure MeasureTheory.Measure.map	—	MeasureTheory.Measure.ext Set.preimage_image_eq injective map_apply

MeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_ae 📖	mathematical	—	Filter.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map	—	Filter.ext MeasureTheory.Measure.instOuterMeasureClass map_apply
map_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.map MeasurableEquiv EquivLike.toFunLike instEquivLike Set.preimage	—	MeasurableEmbedding.map_apply measurableEmbedding
map_apply_eq_iff_map_symm_apply_eq 📖	mathematical	—	MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike symm	—	map_measurableEquiv_injective map_map_symm
map_map_symm 📖	mathematical	—	MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike symm	—	MeasureTheory.Measure.map_map measurable self_comp_symm MeasureTheory.Measure.map_id
map_measurableEquiv_injective 📖	mathematical	—	MeasureTheory.Measure MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike	—	map_symm_map
map_symm_map 📖	mathematical	—	MeasureTheory.Measure.map DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike symm	—	MeasureTheory.Measure.map_map measurable symm_comp_self MeasureTheory.Measure.map_id

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_map_iff 📖	mathematical	AEMeasurable MeasurableSet setOf	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map	—	mem_ae_map_iff
ae_map_mem_range 📖	mathematical	MeasurableSet Set.range	Filter.Eventually Set Set.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map	—	Measure.instOuterMeasureClass mem_ae_map_iff Filter.univ_mem' Set.mem_range_self ae.congr_simp Measure.map_of_not_aemeasurable ae_zero
ae_of_ae_map 📖	—	AEMeasurable Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map	—	—	Measure.instOuterMeasureClass mem_ae_of_mem_ae_map
mem_ae_map_iff 📖	mathematical	AEMeasurable MeasurableSet	Set Filter Filter.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map Set.preimage	—	Measure.instOuterMeasureClass Measure.map_apply_of_aemeasurable MeasurableSet.compl
mem_ae_of_mem_ae_map 📖	mathematical	AEMeasurable Set Filter Filter.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map	Set.preimage	—	Measure.instOuterMeasureClass Filter.Tendsto.eventually Measure.tendsto_ae_map

MeasureTheory.Measure

Definitions

Name	Category	Theorems
liftLinear 📖	CompOp	2 math math: le_liftLinear_apply, liftLinear_apply
map 📖	CompOp	431 math math: MeasureTheory.isMulLeftInvariant_map_add_right, MeasureTheory.mulEquivHaarChar_smul_integral_map, MeasureTheory.isAddLeftInvariant_map, MeasureTheory.isMulRightInvariant_map_add_left, ProbabilityTheory.gaussianReal_map_const_mul, MeasurableEmbedding.integrableOn_map_iff, ProbabilityTheory.condDistrib_apply_of_ne_zero, MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map, Real.smul_map_volume_mul_right, swap_comp, ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq, MapLinearEquiv.isAddHaarMeasure, ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.unitInterval.cdf_eq_real, ProbabilityTheory.gaussianReal_map_neg, InnerRegular.map, MeasurableEmbedding.rnDeriv_map, ProbabilityTheory.IsGaussian.map_eq_gaussianReal, InnerRegular.map_iff, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀, ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, map_add, MeasureTheory.mem_ae_map_iff, MeasurableEquiv.map_apply, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀, MeasureTheory.absolutelyContinuous_map_add_right, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀', pi_map_piCongrLeft, ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq, ProbabilityTheory.compProd_posterior_eq_map_swap, MeasureTheory.trim_eq_map, ae_mem_finset_iff_map_eq_sum_dirac, AddEquiv.isAddHaarMeasure_map, MeasureTheory.isProjectiveLimit_nat_iff, map_conv_addMonoidHom, snd_map_swap, isAddHaarMeasure_map_of_isFiniteMeasure, MeasureTheory.map_mul_left_eq_self, MeasureTheory.mulEquivHaarChar_eq, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, MeasureTheory.pdf.eq_of_map_eq_withDensity, MeasureTheory.IsFundamentalDomain.quotientMeasure_eq, Real.smul_map_diagonal_volume_pi, map_fst_prod, ProbabilityTheory.Kernel.traj_map_updateFinset, map_id, ProbabilityTheory.Kernel.swapRight_apply, map_comp, MeasurableEmbedding.aestronglyMeasurable_map_iff, MeasurableSet.map_coe_volume, dirac_conv, MeasureTheory.instIsZeroOrProbabilityMeasureMap, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, map_mconv_monoidHom, MeasureTheory.map_smul, MeasureTheory.charFunDual_eq_charFun_map_one, MeasureTheory.hasPDF_iff, measurable_map, map_apply, MeasureTheory.map_div_right_eq_self, MeasureTheory.charFunDual_pi', MulEquiv.isHaarMeasure_map, ProbabilityTheory.covarianceBilin_apply_basisFun_self, instSFiniteMap, MeasureTheory.map_add_left_eq_self, isHaarMeasure_map_of_isFiniteMeasure, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure', LinearMap.exists_map_addHaar_eq_smul_addHaar, ProbabilityTheory.gaussianReal_map_continuousLinearMap, infinitePi_map_piCongrLeft, infinitePi_map_piCurry, MeasurableEmbedding.essSup_map_measure, Real.map_matrix_volume_pi_eq_smul_volume_pi, MeasurableEquiv.map_symm_map, ContinuousLinearEquiv.isAddHaarMeasure_map, MeasureTheory.vaddInvariantMeasure_map, MeasureTheory.isMulLeftInvariant_map_smul, InnerRegular.map_of_continuous, isFiniteMeasure_map, MeasurableEquiv.quasiMeasurePreserving_symm, snd_map_prodMk₀, restrict_map, MeasureTheory.Integrable.comp_snd_map_prodMk, MeasureTheory.addMeasure_map_restrict_apply, ProbabilityTheory.complexMGF_mul_I, map_eq_comap, fst_map_swap, Real.smul_map_volume_mul_left, MeasurableEmbedding.integral_map, IsMulRightInvariant.map_mul_right_eq_self, MeasurableEmbedding.memLp_map_measure_iff, MeasureTheory.isMulRightInvariant_map_mul_left, MeasureTheory.charFun_eq_prod_iff, map_linearMap_addHaar_eq_smul_addHaar, MeasureTheory.innerRegular_map_mul_right, join_map_map, Measurable.measurePreserving, ProbabilityTheory.variance_map_equiv, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map, map_piSingleton, ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd, ProbabilityTheory.compProd_map_condDistrib, MeasureTheory.addEquivAddHaarChar_eq, MeasureTheory.absolutelyContinuous_map_div_left, MeasureTheory.mulEquivHaarChar_smul_map, addModularCharacterFun_eq_addHaarScalarFactor, compProd_id, map_sum, ProbabilityTheory.Kernel.fst_apply, pi_prod_map_IocProdIoc, MeasureTheory.innerRegular_map_smul, ProbabilityTheory.integral_truncation_eq_intervalIntegral, essSup_map_measure_of_measurable, ProbabilityTheory.condDistrib_comp_map, ProbabilityTheory.isGaussian_map_equiv_iff, MeasureTheory.integrable_map_equiv, ae_eq_or_eq_iff_map_eq_dirac_add_dirac, MeasurableEmbedding.rnDeriv_map_aux, MeasureTheory.isAddRightInvariant_map_vadd, MeasureTheory.map_add_right_eq_self, MeasurableEquiv.restrict_map, MeasurableEmbedding.restrict_map, isHaarMeasure_map_smul, ProbabilityTheory.gaussianReal_map_linearMap, MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure', map_def, compProd_assoc', MeasureTheory.innerRegular_map_mul_left, ProbabilityTheory.Kernel.partialTraj_compProd_traj, MeasureTheory.setIntegral_map_equiv, Continuous.isOpenPosMeasure_map, comap_swap, InnerRegularWRT.map', pi_map_eval, map_mul_right_inv_eq_self, ProbabilityTheory.instIsGaussianMapHSub, map_eq_zero_iff, compProd_map, MeasureTheory.ae_map_iff, neg_def, MeasureTheory.map_eq_withDensity_pdf, MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, MeasureTheory.charFun_pi, map_eq_sum, ProbabilityTheory.Kernel.condDistrib_trajMeasure, MeasureTheory.integral_map_equiv, MeasurableEquiv.comap_symm, MeasureTheory.HasPDF.haveLebesgueDecomposition, MeasurableEmbedding.lintegral_map, map_prod_map, MeasurableEmbedding.map_injective, infinitePiNat_map_piCongrLeft, ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg, mapₗ_mk_apply_of_aemeasurable, MeasurableEmbedding.integrable_map_iff, pi_prod_map_IicProdIoc, MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id, prod_swap, map_sub_left_eq_self, OuterRegular.map, IsAddLeftInvariant.map_add_left_eq_self, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂_apply, MeasureTheory.MeasurePreserving.map_eq, Topology.IsClosedEmbedding.setIntegral_map, ProbabilityTheory.condDistrib_comp, isFiniteMeasure_map_iff, MeasureTheory.tendstoInDistribution_unique, PMF.toMeasure_map, IsometryEquiv.map_hausdorffMeasure, ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff, ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg, ProbabilityTheory.isGaussian_map, MeasurableEquiv.memLp_map_measure_iff, map_conv_continuousLinearMap, MeasureTheory.innerRegular_map_add_left, MeasureTheory.HasPDF.haveLebesgueDecomposition', ProbabilityTheory.indepFun_iff_charFunDual_prod', MeasurableEquiv.sigmaFinite_map, ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.integrable_comp_snd_map_prodMk_iff, restrict_map_of_aemeasurable, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul, ProbabilityTheory.condDistrib_snd_prod, ProbabilityTheory.isGaussian_map_of_measurable, MeasureTheory.charFunDual_map_const_add, infinitePi_map_eval, MeasureTheory.charFunDual_map_add_const, dirac_unit_compProd_const, ProbabilityTheory.indepFun_iff_charFun_prod, MeasureTheory.map_eq_setLIntegral_pdf, compProd_deterministic, MeasureTheory.smulInvariantMeasure_map, bind_dirac_eq_map, ProbabilityTheory.isProjectiveMeasureFamily_map_restrict, MeasureTheory.IsTightMeasureSet.map, MeasureTheory.measure_map_restrict_apply, tendsto_ae_map, map_id', ProbabilityTheory.moment_truncation_eq_intervalIntegral, ProbabilityTheory.gaussianReal_map_mul_const, MeasurableEmbedding.comap_map, ProbabilityTheory.IsGaussian.map_rotation_eq_self, Topology.IsClosedEmbedding.integral_map, map_add_right_neg_eq_self, ProbabilityTheory.iIndepFun_iff_charFunDual_pi, Real.hasPDF_iff, MeasurableEmbedding.integrableAtFilter_map_iff, ProbabilityTheory.covarianceBilin_apply_pi, MeasurableEmbedding.eLpNorm_map_measure, infinitePi_map_curry_symm, ProbabilityTheory.HasGaussianLaw.charFun_map_eq, dirac_prod, deterministic_comp_eq_map, MeasureTheory.innerRegular_map_add_right, join_map_dirac, QuasiMeasurePreserving.ae_map_le, ContinuousAddEquiv.isAddHaarMeasure_map, le_map_apply, ProbabilityTheory.covarianceBilin_apply_basisFun, ProbabilityTheory.instIsGaussianMapHAdd_1, MeasurableEmbedding.sigmaFinite_map, map_congr, Real.hasPDF_iff_of_aemeasurable, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, map_right_mul_eq_modularCharacterFun_smul, MeasureTheory.map_trim_comap, mapₗ_apply_of_measurable, MeasureTheory.setLIntegral_map, MeasureTheory.addEquivAddHaarChar_smul_map, MeasureTheory.integrableOn_map_equiv, prod_dirac, ProbabilityTheory.condDistrib_def, map_inv_eq_self, map_toOuterMeasure, ProbabilityTheory.gaussianReal_map_sub_const, MeasurableEquiv.map_map_symm, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map', Real.map_linearMap_volume_pi_eq_smul_volume_pi, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀', map_linearMap_addHaar_pi_eq_smul_addHaar, ProbabilityTheory.covariance_map_equiv, map_mono_of_aemeasurable, ProbabilityTheory.Kernel.map_const, MeasurableEmbedding.map_apply, isHaarMeasure_map_add_right, snd_map_prodMk, ProbabilityTheory.HasGaussianLaw.isGaussian_map, map_addHaar_smul, ProbabilityTheory.Kernel.snd_apply, MeasurableEmbedding.absolutelyContinuous_map, map_apply_of_aemeasurable, ProbabilityTheory.condDistrib_self, InnerRegularCompactLTTop.map_of_continuous, isProbabilityMeasure_map_iff, MeasureTheory.isProbabilityMeasure_map_up, MeasureTheory.withDensity_pdf_le_map, MeasureTheory.MeasurePreserving.map_of_comp, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀', MeasureTheory.locallyIntegrable_map_homeomorph, compProd_assoc, ContinuousMulEquiv.isHaarMeasure_map, InnerRegularWRT.map, MeasureTheory.setLIntegral_pdf_le_map, map_dirac, Measurable.quasiMeasurePreserving, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', ProbabilityTheory.condDistrib_comp_self, conv_dirac, ProbabilityTheory.compProd_trim_condExpKernel, MeasureTheory.TendstoInDistribution.tendsto, MeasureTheory.charFunDual_prod', QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar, fst_map_prodMk₀, ProbabilityTheory.complexMGF_id_map, infinitePi_map_pi, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun, ProbabilityTheory.covarianceBilin_map, ProbabilityTheory.gaussianReal_map_add_const, ProbabilityTheory.iIndepFun_iff_charFun_pi, isHaarMeasure_map_mul_right, aemeasurable_map_equiv_iff, le_map_apply_image, MeasureTheory.pdf_def, ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, MeasurableEmbedding.singularPart_map, MeasureTheory.map_measureReal_apply, MeasureTheory.charFunDual_eq_pi_iff', ProbabilityTheory.Kernel.traj_map_frestrictLe_apply, MeasureTheory.charFun_map_mul, MeasureTheory.pdf.eq_of_map_eq_withDensity', ProbabilityTheory.isProjectiveLimit_map, MeasurableEmbedding.mutuallySingular_map, infinitePiNat_map_restrict, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure, Regular.map, Isometry.map_hausdorffMeasure, Measurable.map_prodMk_right, MeasureTheory.Integrable.comp_snd_map_prod_id, map_div_left_eq_self, ProbabilityTheory.map_eq_of_forall_ae_eq, MeasureTheory.lintegral_map_le, map_const, essSup_comp_le_essSup_map_measure, Real.map_volume_mul_right, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul', MeasureTheory.lintegral_map, map_mono, MeasureTheory.isMulLeftInvariant_map, MeasurableEquiv.map_measurableEquiv_injective, ProbabilityTheory.gaussianReal_map_const_sub, MeasurableEmbedding.ae_map_iff, ProbabilityTheory.gaussianReal_map_const_add, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, ProbabilityTheory.mgf_id_map, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, ProbabilityTheory.map_restrict_eq_of_forall_ae_eq, ProbabilityTheory.condDistrib_const, MeasureTheory.charFunDual_map, MeasureTheory.isAddLeftInvariant_map_vadd, MeasureTheory.FiniteMeasure.toMeasure_map, ProbabilityTheory.condDistrib_fst_prod, MeasureTheory.map_vadd, ProbabilityTheory.isGaussian_map_equiv, MeasurableEmbedding.setIntegral_map, ProbabilityTheory.covarianceBilin_map_const_add, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map', ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map, infinitePi_map_restrict, map_smul, prodAssoc_prod, mconv_dirac, IsFiniteMeasureOnCompacts.map, isHaarMeasure_map, MeasurableEmbedding.map_comap, copy_comp_map, MeasureTheory.integral_map_of_stronglyMeasurable, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map, ext_of_complexMGF_eq, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map', ProbabilityTheory.HasSubgaussianMGF.id_map_iff, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, ProbabilityTheory.variance_id_map, ProbabilityTheory.instIsGaussianMapHAdd, MeasureTheory.IsFundamentalDomain.projection_respects_measure, MeasureTheory.absolutelyContinuous_map_mul_right, isAddHaarMeasure_map, MeasurableEquiv.gaussianReal_map_symm_apply, ProbabilityTheory.IdentDistrib.map_eq, Module.Basis.map_addHaar, MeasureTheory.ae_map_mem_range, fst_map_prodMk, map_comap_subtype_coe, MeasureTheory.SimpleFunc.lintegral_map, isProbabilityMeasure_map, Regular.map_iff, dirac_mconv, pi_map_piOptionEquivProd, prod_def, MeasureTheory.smulInvariantMeasure_map_smul, MeasureTheory.charFun_map_eq_charFunDual_smul, map_zero, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map, MeasurableEmbedding.eLpNormEssSup_map_measure, dirac_unit_compProd, MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure, MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk, map_right_add_eq_addModularCharacterFun_vadd, MeasureTheory.ProbabilityMeasure.toMeasure_map, ProbabilityTheory.instIsGaussianMapHSub_1, AbsolutelyContinuous.map, MeasureTheory.hasPDF_iff_of_aemeasurable, MeasureTheory.innerRegular_map_vadd, IsMulLeftInvariant.map_mul_left_eq_self, MeasureTheory.IsAddFundamentalDomain.absolutelyContinuous_map, map_map, MeasureTheory.lintegral_map_equiv, ProbabilityTheory.IndepFun.charFun_map_add_eq_mul, Measurable.map_prodMk_left, join_map_join, MeasurableEmbedding.map_withDensity_rnDeriv, MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure, MeasurableEquiv.map_ae, MeasureTheory.pdf.IsUniform.absolutelyContinuous, MeasureTheory.charFun_map_const_add, MeasureTheory.charFun_eq_pi_iff, isAddHaarMeasure_map_vadd, inv_def, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map, map_of_not_aemeasurable, MeasureTheory.vaddInvariantMeasure_map_vadd, ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, MeasureTheory.HasPDF.absolutelyContinuous', MeasureTheory.charFun_prod, infinitePi_map_piCurry_symm, MeasureTheory.charFunDual_eq_prod_iff', IsAddRightInvariant.map_add_right_eq_self, MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar, MeasureTheory.isMulRightInvariant_map_smul, MeasureTheory.charFun_map_smul, MeasureTheory.ae_map_iff_ae_trim, map_neg_eq_self, MeasureTheory.trim_comap_apply, ContinuousLinearMap.integral_id_map, MeasureTheory.lintegral_comp, MeasureTheory.map_mul_right_eq_self, map_snd_prod, MeasureTheory.absolutelyContinuous_map_sub_left, MeasureTheory.HasPDF.absolutelyContinuous, infinitePi_map_restrict', MeasurableEquiv.map_symm, LinearMap.exists_map_addHaar_eq_smul_addHaar', MeasureTheory.addEquivAddHaarChar_smul_integral_map, infinitePi_map_curry, ProbabilityTheory.instIsGaussianMapNeg, MeasureTheory.isProjectiveLimit_nat_iff', MeasureTheory.MeasurableEquiv.measurePreserving_symm, MeasureTheory.charFun_map_add_const, MeasureTheory.map_sub_right_eq_self, ProbabilityTheory.deterministic_comp_posterior, modularCharacterFun_eq_haarScalarFactor, ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀, MeasurableEmbedding.aemeasurable_map_iff, ProbabilityTheory.setBernoulli_eq_map, ProbabilityTheory.indepFun_iff_charFunDual_prod, MeasureTheory.isMulLeftInvariant_map_mul_right, Real.map_volume_mul_left, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
mapₗ 📖	CompOp	5 math math: mapₗ_congr, map_def, mapₗ_mk_apply_of_aemeasurable, mapₗ_apply_of_measurable, mapₗ_eq_zero_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_liftLinear_apply 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.OuterMeasure.caratheodory DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike toOuterMeasure	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.Measure instFunLike instAddCommMonoid instModule liftLinear	—	IsScalarTower.right MeasureTheory.le_toMeasure_apply
le_map_apply 📖	mathematical	AEMeasurable	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike Set.preimage map	—	MeasureTheory.measure_mono instOuterMeasureClass Set.preimage_mono MeasureTheory.subset_toMeasurable map_apply_of_aemeasurable MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_toMeasurable
le_map_apply_image 📖	mathematical	AEMeasurable	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike map Set.image	—	LE.le.trans MeasureTheory.measure_mono instOuterMeasureClass Set.subset_preimage_image le_map_apply
liftLinear_apply 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.OuterMeasure.caratheodory DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike toOuterMeasure MeasurableSet	MeasureTheory.Measure Set instFunLike instAddCommMonoid instModule liftLinear MeasureTheory.OuterMeasure.instFunLikeSetENNReal	—	IsScalarTower.right MeasureTheory.toMeasure_apply
liftLinear_apply₀ 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasureTheory.OuterMeasure.caratheodory DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike toOuterMeasure MeasureTheory.NullMeasurableSet MeasureTheory.Measure instAddCommMonoid instModule liftLinear	Set instFunLike MeasureTheory.OuterMeasure.instFunLikeSetENNReal	—	IsScalarTower.right MeasureTheory.toMeasure_apply₀
map_add 📖	mathematical	Measurable	map MeasureTheory.Measure instAdd	—	IsScalarTower.right mapₗ_apply_of_measurable map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
map_apply 📖	mathematical	Measurable MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike map Set.preimage	—	map_apply_of_aemeasurable Measurable.aemeasurable
map_apply_of_aemeasurable 📖	mathematical	AEMeasurable MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike map Set.preimage	—	map_apply₀ MeasurableSet.nullMeasurableSet
map_apply₀ 📖	mathematical	AEMeasurable MeasureTheory.NullMeasurableSet map	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage	—	map_def IsScalarTower.right mapₗ.eq_1 liftLinear_apply₀ MeasureTheory.measure_congr instOuterMeasureClass Filter.EventuallyEq.preimage
map_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	map	—	instOuterMeasureClass AEMeasurable.congr IsScalarTower.right mapₗ_mk_apply_of_aemeasurable mapₗ_congr Filter.EventuallyEq.trans Filter.EventuallyEq.symm aemeasurable_congr map_of_not_aemeasurable
map_def 📖	mathematical	—	map MeasureTheory.Measure AEMeasurable DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule Semiring.toModule LinearMap.instFunLike mapₗ instZero	—	—
map_eq_zero_iff 📖	mathematical	AEMeasurable	map MeasureTheory.Measure instZero	—	map_apply_of_aemeasurable MeasurableSet.univ
map_id 📖	mathematical	—	map	—	ext map_apply measurable_id
map_id' 📖	mathematical	—	map	—	map_id
map_map 📖	mathematical	Measurable	map	—	ext map_apply Measurable.comp
map_mono 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder Measurable	map	—	le_iff map_apply_of_aemeasurable Measurable.aemeasurable
map_ne_zero_iff 📖	—	AEMeasurable	—	—	Iff.not map_eq_zero_iff
map_of_not_aemeasurable 📖	mathematical	AEMeasurable	map MeasureTheory.Measure instZero	—	map_def
map_smul 📖	mathematical	—	map MeasureTheory.Measure instSMul	—	IsScalarTower.right eq_or_ne zero_smul map_zero instOuterMeasureClass ae_ennreal_smul_measure_iff mapₗ_mk_apply_of_aemeasurable MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mapₗ_congr Filter.EventuallyEq.trans Filter.EventuallyEq.symm map_of_not_aemeasurable smul_zero smul_assoc instIsScalarTower one_smul
map_toOuterMeasure 📖	mathematical	AEMeasurable	toOuterMeasure map MeasureTheory.OuterMeasure.trim DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike MeasureTheory.OuterMeasure.map	—	IsScalarTower.right trimmed MeasureTheory.OuterMeasure.trim_eq_trim_iff map_apply_of_aemeasurable
map_zero 📖	mathematical	—	map MeasureTheory.Measure instZero	—	map_def map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
mapₗ_apply_of_measurable 📖	mathematical	Measurable	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.Measure instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike mapₗ map	—	IsScalarTower.right Measurable.aemeasurable mapₗ_mk_apply_of_aemeasurable mapₗ_congr
mapₗ_congr 📖	mathematical	Measurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike mapₗ	—	instOuterMeasureClass ext IsScalarTower.right liftLinear_apply MeasureTheory.measure_congr Filter.EventuallyEq.preimage
mapₗ_eq_zero_iff 📖	mathematical	Measurable	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.Measure instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike mapₗ instZero	—	IsScalarTower.right mapₗ_apply_of_measurable map_eq_zero_iff Measurable.aemeasurable
mapₗ_mk_apply_of_aemeasurable 📖	mathematical	AEMeasurable	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.Measure instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike mapₗ map	—	IsScalarTower.right map_def
mapₗ_ne_zero_iff 📖	—	Measurable	—	—	Iff.not IsScalarTower.right mapₗ_eq_zero_iff
measure_preimage_of_map_eq_self 📖	mathematical	map MeasureTheory.NullMeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage	—	map_apply₀ map_of_not_aemeasurable
preimage_null_of_map_null 📖	mathematical	AEMeasurable DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike map instZeroENNReal	Set.preimage	—	nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd LE.le.trans_eq le_map_apply
tendsto_ae_map 📖	mathematical	AEMeasurable	Filter.Tendsto MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass map	—	instOuterMeasureClass preimage_null_of_map_null

---

← Back to Index