Representation

📁 Source: Mathlib/Probability/Kernel/Representation.lean

Statistics

Metric	Count
Definitions Representation	1
Theorems exists_measurable_map_eq, exists_measurable_map_eq_unitInterval	2
Total	3

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_measurable_map_eq 📖	mathematical	—	Measurable Set.Elem Real unitInterval Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace map MeasureTheory.MeasureSpace.toMeasurableSpace unitInterval.instMeasureSpaceElemReal MeasureTheory.MeasureSpace.volume	—	ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval ProbabilityTheory.Kernel.const.instIsMarkovKernel Measurable.fun_comp Measurable.prodMk measurable_const measurable_id'

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_measurable_map_eq_unitInterval 📖	mathematical	—	Measurable Set.Elem Real unitInterval Prod.instMeasurableSpace Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace MeasureTheory.Measure.map MeasureTheory.MeasureSpace.toMeasurableSpace unitInterval.instMeasureSpaceElemReal MeasureTheory.MeasureSpace.volume DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	measurableEmbedding_sigmoid_comp_embeddingReal IsMarkovKernel.map MeasurableEmbedding.measurable map_comp_right MeasurableEmbedding.measurable_invFun MeasurableEmbedding.leftInverse_invFun map_id Measurable.fun_comp map_apply MeasureTheory.Measure.map_map Measurable.prodMk measurable_const measurable_id'

(root)

Definitions

Name	Category	Theorems
Representation 📖	CompOp	128 math math: Rep.trivial_ρ, groupCohomology.mem_cocycles₂_def, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, groupCohomology.d₂₃_hom_apply, Rep.resCoindToHom_hom_apply_coe, groupHomology.d₃₂_single, Representation.finsupp_apply, Representation.Coinvariants.mk_inv_tmul, Representation.asAlgebraHom_single, Representation.freeLift_single_single, Representation.asGroupHom_apply, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, Representation.linearize_single, groupHomology.mem_cycles₂_iff, groupCohomology.d₁₂_hom_apply, Representation.directSum_apply, groupCohomology.d₀₁_hom_apply, Representation.ofMulAction_apply, groupHomology.d₃₂_single_one_thd, Representation.apply_sub_id_partialSum_eq, Representation.Coinvariants.mk_tmul_inv, groupCohomology.mem_cocycles₁_def, Representation.Coinvariants.le_comap_ker, Representation.ofMulAction_single, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, Representation.ofDistribMulAction_apply_apply, groupHomology.d₂₁_single_inv_mul_ρ_add_single, Representation.Coinvariants.sub_mem_ker, Representation.single_smul, Representation.prod_apply_apply, Representation.tprod_apply, Representation.IntertwiningMap.isIntertwiningMap_of_mem_center, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, Representation.Coinvariants.mk_self_apply, Rep.applyAsHom_comm_apply, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupCohomology.cocycles₂_map_one_snd, Representation.mem_invariants_iff_of_forall_mem_zpowers, Representation.ofQuotient_coe_apply, Representation.mem_invariants, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, Rep.ofMulDistribMulAction_ρ_apply_apply, Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, TannakaDuality.FiniteGroup.leftRegular_apply, Representation.apply_bijective, Representation.linHom_apply, Rep.trivial_ρ_apply, groupCohomology.cocycles₁_map_inv, Rep.indToCoindAux_mul_fst, Representation.asAlgebraHom_single_one, Rep.ihom_obj_ρ_apply, Representation.finsupp_single, groupCohomology.mem_cocycles₂_iff, Rep.ofDistribMulAction_ρ_apply_apply, groupCohomology.mem_cocycles₁_iff, Representation.norm_comp_self, groupHomology.inhomogeneousChains.d_single, Subrepresentation.apply_mem_toSubmodule, Representation.asModuleEquiv_symm_map_rho, Representation.freeLift_toLinearMap, Representation.ofModule_asModule_act, Rep.indToCoindAux_mul_snd, Representation.asAlgebraHom_of, Rep.coe_res_obj_ρ', inhomogeneousCochains.d_hom_apply, Rep.ρ_mul, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, Representation.isTrivial_def, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, Rep.leftRegularHom_hom_single, Representation.free_single_single, Representation.IntertwiningMap.isIntertwining', Representation.le_comap_invariants, Representation.invariants_eq_inter, Representation.subrepresentation_apply, Representation.norm_self_apply, Representation.smul_tprod_one_asModule, Representation.self_inv_apply, LinearEquiv.isIntertwining_symm_isIntertwining, Representation.isTrivial_apply, Representation.IsIntertwiningMap.isIntertwining, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, Rep.unit_iso_comm, Rep.leftRegularHomEquiv_symm_single, Representation.IntertwiningMap.isIntertwining_assoc, Rep.hom_comm_apply, Representation.toCoinvariants_mk, Representation.IsTrivial.out, Representation.mem_coindV, Representation.quotient_apply, Representation.ind_mk, groupHomology.d₂₁_single_one_snd, groupHomology.d₃₂_single_one_snd, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Representation.linHom.mem_invariants_iff_comm, Rep.indResHomEquiv_symm_apply, Representation.IntertwiningMap.isIntertwining, groupHomology.d₁₀_single_inv, Representation.ofMulDistribMulAction_apply_apply, Representation.smul_one_tprod_asModule, Rep.applyAsHom_apply, Representation.leftRegularMapEquiv_symm_single, groupHomology.d₂₁_single, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, Representation.dual_apply, Representation.dualTensorHom_comm, groupHomology.single_mem_cycles₂_iff, Representation.isIntertwiningMap_iff, Representation.self_comp_norm, Representation.inv_self_apply, Representation.apply_eq_of_coe_eq, Representation.Equiv.conj_apply_self, groupHomology.single_mem_cycles₁_iff, groupHomology.d₂₁_single_ρ_add_single_inv_mul, Representation.mem_linHom_invariants_iff_isIntertwining, Representation.mem_invtSubmodule, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, TannakaDuality.FiniteGroup.rightRegular_apply, groupHomology.mem_cycles₁_iff, Representation.trivial_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, Representation.linearizeTrivial_def, Representation.self_norm_apply, Representation.leftRegularMapEquiv_symm_apply_toFun, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, Representation.ofMulAction_def

---

← Back to Index