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 Set.range 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 📖	mathematical	AEMeasurable Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	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 Filter Filter.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set.preimage	—	Measure.instOuterMeasureClass Filter.Tendsto.eventually Measure.tendsto_ae_map

MeasureTheory.Measure

Definitions

Name	Category	Theorems
liftLinear 📖	CompOp	3 math math: liftLinear_apply₀, le_liftLinear_apply, liftLinear_apply
map 📖	CompOp	501 math math: MeasureTheory.isMulLeftInvariant_map_add_right, MeasureTheory.mulEquivHaarChar_smul_integral_map, EuclideanGeometry.euclideanHausdorffMeasure_eq, 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, MeasureTheory.taylor_charFun_two, Real.smul_map_volume_mul_right, MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map, 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.IndepFun.charFunDual_map_fun_add_eq_mul, 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, ProbabilityTheory.iIndepFun.charFunDual_map_finset_sum_eq_prod, map_comp, MeasurableEmbedding.aestronglyMeasurable_map_iff, MeasurableSet.map_coe_volume, dirac_conv, MeasureTheory.instIsZeroOrProbabilityMeasureMap, ProbabilityTheory.iIndepFun.charFunDual_map_fun_sum_eq_prod, 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.integral_map, MeasureTheory.hasPDF_iff, measurable_map, map_apply, MeasureTheory.map_div_right_eq_self, MeasureTheory.charFunDual_pi', MulEquiv.isHaarMeasure_map, essSup_map_measure, 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, MeasureTheory.Integrable.integral_norm_condDistrib_map, infinitePi_map_piCurry, MeasurableEmbedding.essSup_map_measure, exists_measurable_map_eq, 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, ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd, QuotientGroup.integral_eq_integral_automorphize, 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, essSup_comp_quotientAddGroup_mk, Continuous.isOpenPosMeasure_map, ProbabilityTheory.map_pi_eq_stdGaussian, MeasureTheory.setIntegral_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, SimpleGraph.binomialRandom_eq_map, 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, Function.Injective.map_count_le, 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, ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prod, 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, pi_map_pi, 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, AEMeasurable.map_add₀, ProbabilityTheory.charFun_map_add_prod_eq_mul, MeasureTheory.innerRegular_map_add_left, MeasureTheory.Integrable.integral_condDistrib_map, MeasureTheory.HasPDF.haveLebesgueDecomposition', ProbabilityTheory.iIndepFun.charFunDual_map_sum_eq_prod, ProbabilityTheory.indepFun_iff_charFunDual_prod', MeasurableEquiv.sigmaFinite_map, ProbabilityTheory.gaussianReal_map_div_const, ProbabilityTheory.charFun_map_sum_pi_eq_prod, 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.Kernel.exists_measurable_map_eq_unitInterval, ProbabilityTheory.iIndepFun.charFun_map_sum_eq_prod, ProbabilityTheory.isGaussian_map_of_measurable, MeasureTheory.charFunDual_map_const_add, infinitePi_map_eval, MeasureTheory.charFunDual_map_add_const, dirac_unit_compProd_const, MeasureTheory.eLpNormEssSup_map_measure, ProbabilityTheory.indepFun_iff_charFun_prod, ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable, MeasureTheory.map_eq_setLIntegral_pdf, compProd_deterministic, MeasureTheory.smulInvariantMeasure_map, bind_dirac_eq_map, ProbabilityTheory.isProjectiveMeasureFamily_map_restrict, MeasureTheory.IsTightMeasureSet.map, map_dirac', 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, QuotientAddGroup.integral_eq_integral_automorphize, MeasureTheory.Integrable.norm_integral_condDistrib_map, addHaarScalarFactor_map, infinitePi_map_curry_symm, ProbabilityTheory.HasGaussianLaw.charFun_map_eq, dirac_prod, deterministic_comp_eq_map, MeasureTheory.innerRegular_map_add_right, join_map_dirac, MeasureTheory.rnDeriv_map_ae_eq_trim, QuasiMeasurePreserving.ae_map_le, ContinuousAddEquiv.isAddHaarMeasure_map, le_map_apply, ProbabilityTheory.covarianceBilin_apply_basisFun, ProbabilityTheory.instIsGaussianMapHAdd_1, MeasurableEmbedding.sigmaFinite_map, map_congr, ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun, Real.hasPDF_iff_of_aemeasurable, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, ProbabilityTheory.iIndepFun.charFun_map_fun_finset_sum_eq_prod, map_right_mul_eq_modularCharacterFun_smul, MeasureTheory.map_trim_comap, mapₗ_apply_of_measurable, MeasureTheory.setLIntegral_map, MeasureTheory.addEquivAddHaarChar_smul_map, ProbabilityTheory.variance_map, MeasureTheory.integrableOn_map_equiv, prod_dirac, ProbabilityTheory.condDistrib_def, essSup_comp_quotientGroup_mk, map_inv_eq_self, map_toOuterMeasure, MeasureTheory.toReal_rnDeriv_map_ae_eq_trim, ProbabilityTheory.gaussianReal_map_sub_const, MeasurableEquiv.map_map_symm, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map', ProbabilityTheory.charFun_inv_sqrt_mul_sum, 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.stdGaussian_map, MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff, 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, ProbabilityTheory.charFunDual_map_sum_pi_eq_prod, 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₀', ProbabilityTheory.mgf_map, MeasureTheory.locallyIntegrable_map_homeomorph, compProd_assoc, MeasureTheory.taylorWithinEval_charFun_two_zero, ProbabilityTheory.iIndepFun.charFun_map_finset_sum_eq_prod, 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, MeasureTheory.charFun_map_mul_comp, 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, Isometry.map_euclideanHausdorffMeasure, le_map_apply_image, MeasureTheory.pdf_def, ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, ProbabilityTheory.charFunDual_map_add_prod_eq_mul, 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, AEMeasurable.map_map_of_aemeasurable, 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, ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow, MeasureTheory.charFun_map_smul_comp, ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis, map_mono, MeasureTheory.isMulLeftInvariant_map, MeasurableEquiv.map_measurableEquiv_injective, ProbabilityTheory.gaussianReal_map_const_sub, MeasurableEmbedding.ae_map_iff, ProbabilityTheory.iIndepFun.charFunDual_map_fun_finset_sum_eq_prod, ProbabilityTheory.gaussianReal_map_const_add, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, ProbabilityTheory.mgf_id_map, MeasureTheory.taylorWithinEval_charFun_two_zero', 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, MeasureTheory.eLpNorm_map_measure, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map', ProbabilityTheory.HasSubgaussianMGF.id_map_iff, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, QuotientAddGroup.integral_mul_eq_integral_automorphize_mul, ProbabilityTheory.variance_id_map, ProbabilityTheory.condDistrib_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, map_apply₀, pi_map_piOptionEquivProd, MeasureTheory.rnDeriv_map, 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.integrable_map_measure, MeasureTheory.lintegral_map', MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk, map_right_add_eq_addModularCharacterFun_vadd, MeasureTheory.ProbabilityMeasure.toMeasure_map, ProbabilityTheory.instIsGaussianMapHSub_1, AbsolutelyContinuous.map, ProbabilityTheory.IndepFun.charFun_map_fun_add_eq_mul, 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, MeasureTheory.Integrable.condDistrib_ae_map, 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, QuotientGroup.integral_mul_eq_integral_automorphize_mul, MeasureTheory.toReal_rnDeriv_map, MeasureTheory.ae_map_iff_ae_trim, map_neg_eq_self, haarScalarFactor_map, MeasureTheory.trim_comap_apply, ProbabilityTheory.covariance_map, 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, MeasureTheory.memLp_map_measure_iff, 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.covariance_map_fun, 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	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike toOuterMeasure 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	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike liftLinear MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule toOuterMeasure	—	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	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike liftLinear MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.OuterMeasure.addCommMonoid MeasureTheory.OuterMeasure.instModule toOuterMeasure	—	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 map 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	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder 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 MeasureTheory.Measure 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	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.preimage instZeroENNReal	—	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