Trim

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

Statistics

Metric	Count
Definitions `trim`	1
Theorems `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`	22
Total	23

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_of_ae_eq_trim` 📖	—	`MeasurableSpace` `MeasurableSpace.instLE` `Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.trim`	—	—	`Measure.instOuterMeasureClass` `measure_eq_zero_of_trim_eq_zero`
`ae_le_of_ae_le_trim` 📖	—	`MeasurableSpace` `MeasurableSpace.instLE` `Filter.EventuallyLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.trim`	—	—	`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` 📖	—	`MeasurableSpace` `MeasurableSpace.instLE` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.trim`	—	—	`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` 📖	—	`MeasurableSpace` `MeasurableSpace.instLE` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Measure.trim` `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`	`toMeasurable`	—	`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` `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	77 math math: `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.condExp_def`, `MeasureTheory.lpMeasSubgroupToLpTrim_sub`, `MeasureTheory.limsup_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`, `ProbabilityTheory.condExpKernel_ae_eq_trim_condExp`, `MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous`, `MeasureTheory.map_trim_comap`, `MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure`, `MeasureTheory.le_trim`, `MeasureTheory.trim_measurableSet_eq`, `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.condLExp_def`, `MeasureTheory.sigmaFinite_trim_bot_iff`, `AbsolutelyContinuous.trim`, `ae_eq_trim_of_measurable`, `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.condLExp_of_not_sub_sigma_measurable`, `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.trim`	—	`MeasureTheory.trim_measurableSet_eq`

(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`	`MeasureTheory.Measure.trim`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.eq_1` `MeasureTheory.ae_iff` `MeasureTheory.trim_measurableSet_eq` `Measurable.not` `Measurable.eq`

---

← Back to Index