Trim

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

Statistics

Metric	Count
Definitions trim	1
Theorems trim, of_trim, ae_eq_of_ae_eq_trim, ae_le_of_ae_le_trim, ae_map_iff_ae_trim, ae_of_ae_trim, isFiniteMeasure_trim, le_trim, map_trim_comap, measure_eq_zero_of_trim_eq_zero, measure_trim_toMeasurable_eq_zero, restrict_trim, sigmaFiniteTrim_mono, sigmaFinite_trim_bot_iff, toOuterMeasure_trim_eq_trim_toOuterMeasure, trim_add, trim_comap_apply, trim_eq_map, trim_eq_self, trim_measurableSet_eq, trim_trim, zero_trim, ae_eq_trim_of_measurable	23
Total	24

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_of_ae_eq_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.trim	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass measure_eq_zero_of_trim_eq_zero
ae_le_of_ae_le_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Filter.EventuallyLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.trim	Filter.EventuallyLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass measure_eq_zero_of_trim_eq_zero
ae_map_iff_ae_trim 📖	mathematical	Measurable MeasurableSet setOf	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.map MeasurableSpace.comap Measure.trim Measurable.comap_le	—	Measure.instOuterMeasureClass Measurable.comap_le map_trim_comap ae_map_iff Measurable.aemeasurable Measurable.of_comap_le le_rfl
ae_of_ae_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.trim	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass measure_eq_zero_of_trim_eq_zero
isFiniteMeasure_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	IsFiniteMeasure Measure.trim	—	trim_measurableSet_eq MeasurableSet.univ measure_lt_top
le_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Measure.trim	—	le_toMeasure_apply
map_trim_comap 📖	mathematical	Measurable	Measure.map MeasurableSpace.comap Measure.trim Measurable.comap_le	—	Measure.ext Measurable.comap_le Measure.map_apply Measurable.of_comap_le le_rfl trim_measurableSet_eq
measure_eq_zero_of_trim_eq_zero 📖	mathematical	MeasurableSpace MeasurableSpace.instLE DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.trim instZeroENNReal	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	—	le_antisymm LE.le.trans le_trim le_of_eq zero_le ENNReal.instCanonicallyOrderedAdd
measure_trim_toMeasurable_eq_zero 📖	mathematical	MeasurableSpace MeasurableSpace.instLE DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.trim instZeroENNReal	DFunLike.coe Measure Set ENNReal Measure.instFunLike toMeasurable Measure.trim instZeroENNReal	—	measure_eq_zero_of_trim_eq_zero measure_toMeasurable
restrict_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	Measure.restrict Measure.trim	—	Measure.ext Measure.restrict_apply trim_measurableSet_eq MeasurableSet.inter
sigmaFiniteTrim_mono 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	SigmaFinite Measure.trim	—	LE.le.trans Set.mem_univ trim_measurableSet_eq measurableSet_spanningSets trim_trim measure_spanningSets_lt_top iUnion_spanningSets
sigmaFinite_trim_bot_iff 📖	mathematical	—	SigmaFinite Bot.bot MeasurableSpace OrderBot.toBot MeasurableSpace.instLE BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder MeasurableSpace.instCompleteLattice Measure.trim bot_le IsFiniteMeasure	—	bot_le sigmaFinite_bot_iff IsFiniteMeasure.measure_univ_lt_top trim_measurableSet_eq MeasurableSet.univ
toOuterMeasure_trim_eq_trim_toOuterMeasure 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Measure.toOuterMeasure Measure.trim OuterMeasure.trim	—	Measure.trim.eq_1 toMeasure_toOuterMeasure
trim_add 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Measure.trim Measure Measure.instAdd	—	Measure.ext trim_measurableSet_eq
trim_comap_apply 📖	mathematical	Measurable MeasurableSet	DFunLike.coe Measure MeasurableSpace.comap Set ENNReal Measure.instFunLike Measure.trim Measurable.comap_le Set.preimage Measure.map	—	Measurable.comap_le map_trim_comap Measure.map_apply Measurable.of_comap_le le_rfl
trim_eq_map 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Measure.trim Measure.map	—	Measure.ext Measure.map_apply measurable_id'' trim_measurableSet_eq Set.preimage_id
trim_eq_self 📖	mathematical	—	Measure.trim le_rfl MeasurableSpace PartialOrder.toPreorder MeasurableSpace.instPartialOrder	—	le_rfl toOuterMeasure_toMeasure
trim_measurableSet_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.trim	—	Measure.trim.eq_1 toMeasure_apply Measure.coe_toOuterMeasure
trim_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Measure.trim LE.le.trans MeasurableSpace PartialOrder.toPreorder MeasurableSpace.instPartialOrder	—	Measure.ext LE.le.trans trim_measurableSet_eq
zero_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	Measure.trim Measure Measure.instZero	—	OuterMeasure.toMeasure_zero

MeasureTheory.Measure

Definitions

Name	Category	Theorems
trim 📖	CompOp	87 math math: MeasureTheory.toReal_rnDeriv_trim, MeasureTheory.lpMeasSubgroupToLpTrim_neg, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.trim_eq_map, MeasureTheory.setLIntegral_trim, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, ProbabilityTheory.condExpKernel_comp_trim, MeasureTheory.condExpL1_measure_zero, MeasureTheory.condExp_congr_ae_trim, MeasureTheory.sigmaFiniteTrim_mono, MeasureTheory.setIntegral_trim, MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration, MeasureTheory.eLpNorm'_trim, ProbabilityTheory.HasSubgaussianMGF.trim, MeasureTheory.condLExp_congr_ae_trim, MeasureTheory.essSup_trim, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel, MeasureTheory.zero_trim, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable, ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time, MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time_of_le, MeasureTheory.eLpNorm_trim, MeasureTheory.trim_eq_self, MeasureTheory.eLpNorm_trim_ae, MeasureTheory.condExp_def, MeasureTheory.lpMeasSubgroupToLpTrim_sub, MeasureTheory.limsup_trim, MeasureTheory.rnDeriv_trim, MeasureTheory.lpMeasSubgroupToLpTrim_right_inv, MeasureTheory.eLpNormEssSup_trim, MeasureTheory.StronglyMeasurable.ae_le_trim_iff, MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim, MeasureTheory.lpMeasSubgroupToLpTrim_add, MeasureTheory.lpMeasSubgroupToLpTrim_left_inv, MeasureTheory.SigmaFiniteFiltration.SigmaFinite, MeasureTheory.rnDeriv_ae_eq_condExp, MeasureTheory.lintegral_trim, ProbabilityTheory.aestronglyMeasurable_trim_condExpKernel, MeasureTheory.rnDeriv_map_ae_eq_trim, ProbabilityTheory.condExpKernel_ae_eq_trim_condExp, MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous, MeasureTheory.map_trim_comap, MeasureTheory.toReal_rnDeriv_map_ae_eq_trim, MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure, MeasureTheory.le_trim, MeasureTheory.trim_measurableSet_eq, MeasureTheory.measure_trim_toMeasurable_eq_zero, MeasureTheory.lpMeasSubgroupToLpTrim_norm_map, MeasureTheory.lpTrimToLpMeas_ae_eq, ProbabilityTheory.HasCondSubgaussianMGF.cgf_le, ProbabilityTheory.compProd_trim_condExpKernel, MeasureTheory.trim_trim, MeasureTheory.trim_withDensity, MeasureTheory.integral_trim_simpleFunc, MeasureTheory.restrict_trim, MeasureTheory.setLIntegral_trim_ae, MeasureTheory.condLExp_def, MeasureTheory.sigmaFinite_trim_bot_iff, AbsolutelyContinuous.trim, ae_eq_trim_of_measurable, MeasureTheory.lintegral_trim_ae, MeasureTheory.isometry_lpMeasSubgroupToLpTrim, MeasureTheory.lpMeasToLpTrim_ae_eq, MeasureTheory.lpMeasToLpTrim_smul, MeasureTheory.lpMeas.ae_fin_strongly_measurable', MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd, MeasureTheory.StronglyMeasurable.ae_eq_trim_iff, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq, MeasureTheory.StronglyMeasurable.ae_le_trim_of_stronglyMeasurable, ProbabilityTheory.HasCondSubgaussianMGF.mgf_le, ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le, MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup, MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable, MeasureTheory.integral_trim_ae, MeasureTheory.condLExp_of_not_sub_sigma_measurable, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, MeasureTheory.ae_map_iff_ae_trim, MeasureTheory.trim_comap_apply, MeasureTheory.trim_add, MeasureTheory.isFiniteMeasure_trim, MeasureTheory.Integrable.trim, MeasureTheory.setLIntegral_condLExp_trim, MeasureTheory.integral_trim

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trim 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasurableSpace MeasurableSpace.instLE	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.trim	—	MeasureTheory.trim_measurableSet_eq

MeasureTheory.SigmaFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	MeasureTheory.SigmaFinite	—	le_rfl MeasureTheory.trim_eq_self MeasureTheory.sigmaFiniteTrim_mono

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_trim_of_measurable 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.trim	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.eq_1 MeasureTheory.ae_iff MeasureTheory.trim_measurableSet_eq Measurable.not Measurable.eq

---

← Back to Index