LocallyIntegrable

📁 Source: Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Statistics

Metric	Count
Definitions `LocallyIntegrable`, `LocallyIntegrableOn`	2
Theorems `locallyIntegrable`, `integrableOn_isCompact`, `integrableOn_of_measure_ne_top`, `memLp_isCompact`, `memLp_of_measure_ne_top`, `memLp_top`, `integrableOn_Icc`, `integrableOn_Ioc`, `integrableOn_uIcc`, `integrableOn_uIoc`, `integrable_of_hasCompactSupport`, `locallyIntegrable`, `integrableOn_Icc`, `integrableOn_compact`, `integrableOn_compact'`, `integrableOn_of_subset_isCompact`, `integrableOn_uIcc`, `locallyIntegrableOn`, `locallyIntegrable`, `continuousOn_mul`, `continuousOn_mul_of_subset`, `continuousOn_smul`, `continuousOn_smul_of_subset`, `locallyIntegrableOn`, `mul_continuousOn`, `mul_continuousOn_of_subset`, `smul_continuousOn`, `smul_continuousOn_of_subset`, `add`, `aestronglyMeasurable`, `exists_nat_integrableOn`, `indicator`, `integrableOn_isCompact`, `integrableOn_nhds_isCompact`, `integrable_smul_left_of_hasCompactSupport`, `integrable_smul_right_of_hasCompactSupport`, `locallyIntegrableOn`, `mono`, `mono_enorm`, `neg`, `smul`, `sub`, `add`, `aestronglyMeasurable`, `continuousOn_mul`, `continuousOn_smul`, `enorm`, `exists_countable_integrableOn`, `exists_nat_integrableOn`, `integrableOn_compact_subset`, `integrableOn_isCompact`, `mono`, `mono_enorm`, `mono_set`, `mul_continuousOn`, `neg`, `norm`, `smul_continuousOn`, `sub`, `locallyIntegrable`, `integrableOn_Ici_iff_integrableAtFilter_atTop`, `integrableOn_Iic_iff_integrableAtFilter_atBot`, `integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin`, `integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin`, `integrable_iff_integrableAtFilter_atBot`, `integrable_iff_integrableAtFilter_atBot_atTop`, `integrable_iff_integrableAtFilter_atTop`, `integrable_iff_integrableAtFilter_cocompact`, `locallyIntegrableOn_const`, `locallyIntegrableOn_const_enorm`, `locallyIntegrableOn_iff`, `locallyIntegrableOn_iff_locallyIntegrable_restrict`, `locallyIntegrableOn_of_locallyIntegrable_restrict`, `locallyIntegrableOn_univ`, `locallyIntegrableOn_zero`, `locallyIntegrable_comap`, `locallyIntegrable_const`, `locallyIntegrable_const_enorm`, `locallyIntegrable_finset_sum`, `locallyIntegrable_finset_sum'`, `locallyIntegrable_iff`, `locallyIntegrable_map_homeomorph`, `locallyIntegrable_zero`, `locallyIntegrable`, `integrableOn_isCompact`, `integrableOn_of_measure_ne_top`, `memLp_isCompact`, `memLp_of_measure_ne_top`, `memLp_top`	89
Total	91

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyIntegrable` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`Monotone.locallyIntegrable` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual` `dual_right`

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrableOn_isCompact` 📖	mathematical	`IsCompact` `AntitoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.memLp_one_iff_integrable` `memLp_isCompact`
`integrableOn_of_measure_ne_top` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `IsLeast` `Preorder.toLE` `IsGreatest` `MeasurableSet`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.memLp_one_iff_integrable` `memLp_of_measure_ne_top`
`memLp_isCompact` 📖	mathematical	`IsCompact` `AntitoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.Measure.restrict`	—	`MonotoneOn.memLp_isCompact` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`memLp_of_measure_ne_top` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `IsLeast` `Preorder.toLE` `IsGreatest` `MeasurableSet`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.Measure.restrict`	—	`MonotoneOn.memLp_of_measure_ne_top` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`
`memLp_top` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `IsLeast` `Preorder.toLE` `IsGreatest` `MeasurableSet`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `Top.top` `ENNReal` `instTopENNReal` `MeasureTheory.Measure.restrict`	—	`MonotoneOn.memLp_top` `instOrderTopologyOrderDual` `instSecondCountableTopologyOrderDual`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrableOn_Icc` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Icc`	—	`ContinuousOn.integrableOn_Icc` `continuousOn`
`integrableOn_Ioc` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.Ioc`	—	`MeasureTheory.IntegrableOn.mono_set` `integrableOn_Icc` `Set.Ioc_subset_Icc_self`
`integrableOn_uIcc` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`integrableOn_Icc`
`integrableOn_uIoc` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.uIoc`	—	`integrableOn_Ioc`
`integrable_of_hasCompactSupport` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasCompactSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.integrableOn_iff_integrable_of_support_subset` `PseudoEMetricSpace.pseudoMetrizableSpace` `subset_tsupport` `ContinuousOn.integrableOn_compact'` `IsClosed.measurableSet` `isClosed_tsupport` `continuousOn`
`locallyIntegrable` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.LocallyIntegrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrableAt_nhds`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrableOn_Icc` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.Icc`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrableOn_compact` `CompactIccSpace.isCompact_Icc`
`integrableOn_compact` 📖	mathematical	`IsCompact` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrableOn_compact'` `IsCompact.measurableSet`
`integrableOn_compact'` 📖	mathematical	`IsCompact` `MeasurableSet` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrableOn_of_subset_isCompact` `Set.Subset.rfl` `IsCompact.measure_ne_top`
`integrableOn_of_subset_isCompact` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `IsCompact` `MeasurableSet` `Set` `Set.instHasSubset`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`aestronglyMeasurable_of_subset_isCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `Ne.lt_top` `Bornology.IsBounded.exists_norm_le` `IsCompact.isBounded` `IsCompact.image_of_continuousOn` `MeasureTheory.HasFiniteIntegral.of_bounded` `MeasureTheory.Restrict.isFiniteMeasure` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_mem` `Filter.univ_mem'` `Set.mem_image_of_mem`
`integrableOn_uIcc` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrableOn_Icc`
`locallyIntegrableOn` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasurableSet`	`MeasureTheory.LocallyIntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrableAt_nhdsWithin`

MeasureTheory

Definitions

Name	Category	Theorems
`LocallyIntegrable` 📖	MathDef	18 math math: `MemLp.locallyIntegrable`, `integrable_iff_integrableAtFilter_atBot`, `Monotone.locallyIntegrable`, `integrable_iff_integrableAtFilter_cocompact`, `integrable_iff_integrableAtFilter_atBot_atTop`, `Antitone.locallyIntegrable`, `integrable_iff_integrableAtFilter_atTop`, `locallyIntegrable_const`, `locallyIntegrableOn_iff_locallyIntegrable_restrict`, `Integrable.locallyIntegrable`, `LipschitzWith.locallyIntegrable_lineDeriv`, `locallyIntegrable_map_homeomorph`, `locallyIntegrable_comap`, `Continuous.locallyIntegrable`, `locallyIntegrable_iff`, `locallyIntegrable_zero`, `locallyIntegrableOn_univ`, `locallyIntegrable_const_enorm`
`LocallyIntegrableOn` 📖	MathDef	18 math math: `locallyIntegrableOn_iff`, `locallyIntegrableOn_of_locallyIntegrable_restrict`, `WeakFEPair.hf_modif_int`, `locallyIntegrableOn_const`, `IntegrableOn.locallyIntegrableOn`, `locallyIntegrableOn_iff_locallyIntegrable_restrict`, `integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin`, `ContinuousOn.locallyIntegrableOn`, `integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin`, `locallyIntegrable_comap`, `integrableOn_Ici_iff_integrableAtFilter_atTop`, `integrableOn_Iic_iff_integrableAtFilter_atBot`, `WeakFEPair.hg_int`, `locallyIntegrableOn_const_enorm`, `WeakFEPair.hf_int`, `LocallyIntegrable.locallyIntegrableOn`, `locallyIntegrableOn_univ`, `locallyIntegrableOn_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrableOn_Ici_iff_integrableAtFilter_atTop` 📖	mathematical	—	`IntegrableOn` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IntegrableAtFilter` `Filter.atTop` `LocallyIntegrableOn`	—	`integrableOn_Iic_iff_integrableAtFilter_atBot` `instCompactIccSpaceOrderDual`
`integrableOn_Iic_iff_integrableAtFilter_atBot` 📖	mathematical	—	`IntegrableOn` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IntegrableAtFilter` `Filter.atBot` `LocallyIntegrableOn`	—	`Filter.Iic_mem_atBot` `IntegrableOn.locallyIntegrableOn` `Filter.mem_atBot_sets` `SemilatticeInf.instIsCodirectedOrder` `IntegrableOn.mono` `integrableOn_union` `le_rfl` `LocallyIntegrableOn.integrableOn_compact_subset` `Set.Icc_subset_Iic_self` `CompactIccSpace.isCompact_Icc` `Set.Iic_subset_Iic_union_Icc`
`integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin` 📖	mathematical	—	`IntegrableOn` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IntegrableAtFilter` `Filter.atBot` `nhdsWithin` `LocallyIntegrableOn`	—	`Filter.Iio_mem_atBot` `instNoBotOrderOfNoMinOrder` `self_mem_nhdsWithin` `IntegrableOn.locallyIntegrableOn` `mem_nhdsLT_iff_exists_Ioo_subset` `IntegrableOn.mono` `integrableOn_union` `integrableOn_Iic_iff_integrableAtFilter_atBot` `LocallyIntegrableOn.mono_set` `Set.Iic_subset_Iio` `le_rfl` `Set.Iio_subset_Iic_union_Ioo`
`integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin` 📖	mathematical	—	`IntegrableOn` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IntegrableAtFilter` `Filter.atTop` `nhdsWithin` `LocallyIntegrableOn`	—	`integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin` `instCompactIccSpaceOrderDual` `OrderDual.noMinOrder` `instOrderTopologyOrderDual`
`integrable_iff_integrableAtFilter_atBot` 📖	mathematical	—	`Integrable` `IntegrableAtFilter` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LocallyIntegrable`	—	`Integrable.integrableAtFilter` `Integrable.locallyIntegrable` `integrable_iff_integrableAtFilter_cocompact` `IntegrableAtFilter.filter_mono` `cocompact_le_atBot`
`integrable_iff_integrableAtFilter_atBot_atTop` 📖	mathematical	—	`Integrable` `ESeminormedAddMonoid.toContinuousENorm` `IntegrableAtFilter` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop` `LocallyIntegrable`	—	`Integrable.integrableAtFilter` `Integrable.locallyIntegrable` `integrable_iff_integrableAtFilter_cocompact` `IntegrableAtFilter.filter_mono` `cocompact_le_atBot_atTop` `IntegrableAtFilter.sup_iff`
`integrable_iff_integrableAtFilter_atTop` 📖	mathematical	—	`Integrable` `IntegrableAtFilter` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LocallyIntegrable`	—	`integrable_iff_integrableAtFilter_atBot` `instCompactIccSpaceOrderDual`
`integrable_iff_integrableAtFilter_cocompact` 📖	mathematical	—	`Integrable` `IntegrableAtFilter` `Filter.cocompact` `LocallyIntegrable`	—	`Integrable.integrableAtFilter` `Integrable.locallyIntegrable` `Filter.mem_cocompact'` `integrableOn_univ` `Set.compl_union_self` `integrableOn_union` `IntegrableOn.mono` `LocallyIntegrable.integrableOn_isCompact` `le_rfl`
`locallyIntegrableOn_const` 📖	mathematical	—	`LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`locallyIntegrableOn_const_enorm` `enorm_ne_top`
`locallyIntegrableOn_const_enorm` 📖	mathematical	—	`LocallyIntegrableOn`	—	`LocallyIntegrable.locallyIntegrableOn` `locallyIntegrable_const_enorm`
`locallyIntegrableOn_iff` 📖	mathematical	`IsLocallyClosed`	`LocallyIntegrableOn` `IntegrableOn`	—	`LocallyIntegrableOn.integrableOn_compact_subset` `exists_compact_subset` `nhdsWithin_inter_of_mem` `nhdsWithin_le_nhds` `IsOpen.mem_nhds` `inter_mem_nhdsWithin` `mem_interior_iff_mem_nhds` `IsCompact.inter_left`
`locallyIntegrableOn_iff_locallyIntegrable_restrict` 📖	mathematical	—	`LocallyIntegrableOn` `LocallyIntegrable` `Measure.restrict`	—	`mem_nhdsWithin` `IsOpen.mem_nhds` `IntegrableOn.eq_1` `Measure.restrict_restrict` `IsOpen.measurableSet` `IntegrableOn.mono_set` `isOpen_compl_iff` `Set.inter_comm` `Set.inter_compl_self` `integrableOn_empty` `locallyIntegrableOn_of_locallyIntegrable_restrict`
`locallyIntegrableOn_of_locallyIntegrable_restrict` 📖	mathematical	`LocallyIntegrable` `Measure.restrict`	`LocallyIntegrableOn`	—	`mem_nhds_iff` `inter_mem_nhdsWithin` `IsOpen.mem_nhds` `Measure.restrict_restrict` `IsOpen.measurableSet` `Set.inter_comm` `IntegrableOn.mono_set`
`locallyIntegrableOn_univ` 📖	mathematical	—	`LocallyIntegrableOn` `Set.univ` `LocallyIntegrable`	—	`nhdsWithin_univ`
`locallyIntegrableOn_zero` 📖	mathematical	—	`LocallyIntegrableOn` `ESeminormedAddMonoid.toContinuousENorm` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid`	—	`LocallyIntegrable.locallyIntegrableOn` `locallyIntegrable_zero`
`locallyIntegrable_comap` 📖	mathematical	`MeasurableSet`	`LocallyIntegrable` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `instTopologicalSpaceSubtype` `Measure.comap` `LocallyIntegrableOn`	—	`MeasurableEmbedding.integrableAtFilter_iff_comap` `MeasurableEmbedding.subtype_coe`
`locallyIntegrable_const` 📖	mathematical	—	`LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`locallyIntegrable_const_enorm` `enorm_ne_top`
`locallyIntegrable_const_enorm` 📖	mathematical	—	`LocallyIntegrable`	—	`MemLp.locallyIntegrable` `memLp_top_const_enorm` `le_top`
`locallyIntegrable_finset_sum` 📖	mathematical	`LocallyIntegrable` `ESeminormedAddMonoid.toContinuousENorm` `ESeminormedAddCommMonoid.toESeminormedAddMonoid`	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`locallyIntegrable_finset_sum'`
`locallyIntegrable_finset_sum'` 📖	mathematical	`LocallyIntegrable` `ESeminormedAddMonoid.toContinuousENorm` `ESeminormedAddCommMonoid.toESeminormedAddMonoid`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`Finset.sum_induction` `LocallyIntegrable.add` `locallyIntegrable_zero`
`locallyIntegrable_iff` 📖	mathematical	—	`LocallyIntegrable` `IntegrableOn`	—	`LocallyIntegrable.integrableOn_isCompact` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace`
`locallyIntegrable_map_homeomorph` 📖	mathematical	—	`LocallyIntegrable` `ESeminormedAddMonoid.toContinuousENorm` `Measure.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`ContinuousAt.preimage_mem_nhds` `Continuous.continuousAt` `Homeomorph.continuous` `integrableOn_map_equiv` `Set.ext` `Homeomorph.symm_apply_apply`
`locallyIntegrable_zero` 📖	mathematical	—	`LocallyIntegrable` `ESeminormedAddMonoid.toContinuousENorm` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid`	—	`Integrable.locallyIntegrable` `integrable_zero`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyIntegrable` 📖	mathematical	`MeasureTheory.Integrable`	`MeasureTheory.LocallyIntegrable`	—	`integrableAtFilter`

MeasureTheory.IntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_mul` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsCompact`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`continuousOn_mul_of_subset` `IsCompact.measurableSet` `Set.Subset.rfl`
`continuousOn_mul_of_subset` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `IsCompact` `MeasurableSet` `Set` `Set.instHasSubset`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`IsCompact.exists_bound_of_continuousOn` `MeasureTheory.Integrable.bdd_mul` `ContinuousOn.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousOn.mono` `MeasureTheory.ae_restrict_of_forall_mem`
`continuousOn_smul` 📖	mathematical	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousOn` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `IsCompact`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`continuousOn_smul_of_subset` `IsCompact.measurableSet` `Set.Subset.rfl`
`continuousOn_smul_of_subset` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MeasureTheory.IntegrableOn` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `IsCompact` `MeasurableSet` `Set` `Set.instHasSubset`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`IsCompact.exists_bound_of_continuousOn` `MeasureTheory.Integrable.bdd_smul` `NormSMulClass.toIsBoundedSMul` `ContinuousOn.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousOn.mono` `MeasureTheory.ae_restrict_of_forall_mem`
`locallyIntegrableOn` 📖	mathematical	`MeasureTheory.IntegrableOn`	`MeasureTheory.LocallyIntegrableOn`	—	`self_mem_nhdsWithin`
`mul_continuousOn` 📖	mathematical	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `ContinuousOn` `IsCompact`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`mul_continuousOn_of_subset` `IsCompact.measurableSet` `Set.Subset.refl`
`mul_continuousOn_of_subset` 📖	mathematical	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `ContinuousOn` `MeasurableSet` `IsCompact` `Set` `Set.instHasSubset`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`IsCompact.exists_bound_of_continuousOn` `MeasureTheory.Integrable.mul_bdd` `ContinuousOn.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousOn.mono` `MeasureTheory.ae_restrict_of_forall_mem`
`smul_continuousOn` 📖	mathematical	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `ContinuousOn` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `IsCompact`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`smul_continuousOn_of_subset` `IsCompact.measurableSet` `Set.Subset.refl`
`smul_continuousOn_of_subset` 📖	mathematical	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `ContinuousOn` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasurableSet` `IsCompact` `Set` `Set.instHasSubset`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`IsCompact.exists_bound_of_continuousOn` `MeasureTheory.Integrable.smul_bdd` `NormSMulClass.toIsBoundedSMul` `ContinuousOn.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousOn.mono` `MeasureTheory.ae_restrict_of_forall_mem`

MeasureTheory.LocallyIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `ESeminormedAddMonoid.toContinuousENorm`	`Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid`	—	`MeasureTheory.IntegrableAtFilter.add`
`aestronglyMeasurable` 📖	mathematical	`MeasureTheory.LocallyIntegrable`	`MeasureTheory.AEStronglyMeasurable`	—	`MeasureTheory.Measure.restrict_univ` `MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable` `MeasureTheory.locallyIntegrableOn_univ`
`exists_nat_integrableOn` 📖	mathematical	`MeasureTheory.LocallyIntegrable`	`IsOpen` `Set.iUnion` `Set.univ` `MeasureTheory.IntegrableOn`	—	`MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn` `locallyIntegrableOn` `Set.eq_univ_of_univ_subset` `Set.inter_univ`
`indicator` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `ESeminormedAddMonoid.toContinuousENorm` `MeasurableSet`	`Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid`	—	`MeasureTheory.IntegrableOn.indicator`
`integrableOn_isCompact` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `IsCompact`	`MeasureTheory.IntegrableOn`	—	`MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact` `locallyIntegrableOn`
`integrableOn_nhds_isCompact` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `IsCompact`	`IsOpen` `Set` `Set.instHasSubset` `MeasureTheory.IntegrableOn`	—	`IsCompact.induction_on` `isOpen_empty` `Set.Subset.rfl` `MeasureTheory.integrableOn_empty` `HasSubset.Subset.trans` `Set.instIsTransSubset` `IsOpen.union` `Set.union_subset_union` `MeasureTheory.IntegrableOn.union` `mem_nhds_iff` `nhdsWithin_le_nhds` `IsOpen.mem_nhds` `MeasureTheory.IntegrableOn.mono_set`
`integrable_smul_left_of_hasCompactSupport` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Continuous` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `HasCompactSupport` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`MeasureTheory.Integrable` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`Set.indicator_eq_self` `Function.support_subset_iff'` `image_eq_zero_of_notMem_tsupport` `zero_smul` `Set.indicator_smul` `MeasureTheory.Integrable.smul_of_top_right` `MeasureTheory.integrable_indicator_iff` `IsCompact.measurableSet` `integrableOn_isCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `Continuous.memLp_top_of_hasCompactSupport`
`integrable_smul_right_of_hasCompactSupport` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `Continuous` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `HasCompactSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`MeasureTheory.Integrable` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`Set.indicator_eq_self` `Function.support_subset_iff'` `image_eq_zero_of_notMem_tsupport` `smul_zero` `Set.indicator_smul_left` `MeasureTheory.Integrable.smul_of_top_left` `MeasureTheory.integrable_indicator_iff` `IsCompact.measurableSet` `integrableOn_isCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `Continuous.memLp_top_of_hasCompactSupport`
`locallyIntegrableOn` 📖	mathematical	`MeasureTheory.LocallyIntegrable`	`MeasureTheory.LocallyIntegrableOn`	—	`MeasureTheory.IntegrableAtFilter.filter_mono` `nhdsWithin_le_nhds`
`mono` 📖	—	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.AEStronglyMeasurable` `Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.locallyIntegrableOn_univ` `MeasureTheory.LocallyIntegrableOn.mono`
`mono_enorm` 📖	—	`MeasureTheory.LocallyIntegrable` `MeasureTheory.AEStronglyMeasurable` `Filter.Eventually` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousENorm.toENorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.locallyIntegrableOn_univ` `MeasureTheory.LocallyIntegrableOn.mono_enorm`
`neg` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.IntegrableAtFilter.neg`
`smul` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Function.hasSMul` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.IntegrableAtFilter.smul`
`sub` 📖	mathematical	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`MeasureTheory.IntegrableAtFilter.sub`

MeasureTheory.LocallyIntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `ESeminormedAddMonoid.toContinuousENorm`	`Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid`	—	`MeasureTheory.IntegrableAtFilter.add`
`aestronglyMeasurable` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn`	`MeasureTheory.AEStronglyMeasurable` `MeasureTheory.Measure.restrict`	—	`exists_nat_integrableOn` `Set.iUnion_inter` `Set.inter_eq_right` `aestronglyMeasurable_iUnion_iff` `instCountableNat` `MeasureTheory.Integrable.aestronglyMeasurable`
`continuousOn_mul` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `ContinuousOn` `IsLocallyClosed`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`MeasureTheory.locallyIntegrableOn_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.IntegrableOn.continuousOn_mul` `ContinuousOn.mono`
`continuousOn_smul` 📖	mathematical	`IsLocallyClosed` `MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousOn` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`MeasureTheory.locallyIntegrableOn_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.IntegrableOn.continuousOn_smul` `ContinuousOn.mono`
`enorm` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn`	`ENNReal` `ENNReal.instTopologicalSpace` `ESeminormedAddMonoid.toContinuousENorm` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `instENormedAddCommMonoidENNReal` `ENorm.enorm` `ContinuousENorm.toENorm`	—	`MeasureTheory.Integrable.enorm`
`exists_countable_integrableOn` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn`	`Set.Countable` `Set` `IsOpen` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `MeasureTheory.IntegrableOn` `Set.instInter`	—	`mem_nhdsWithin` `MeasureTheory.IntegrableOn.mono_set` `Set.mem_iUnion_of_mem` `TopologicalSpace.isOpen_iUnion_countable` `Set.Countable.image` `Set.biUnion_image`
`exists_nat_integrableOn` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn`	`IsOpen` `Set` `Set.instHasSubset` `Set.iUnion` `MeasureTheory.IntegrableOn` `Set.instInter`	—	`exists_countable_integrableOn` `Set.Countable.insert` `Set.Countable.exists_eq_range` `Set.mem_range_self` `Set.mem_insert_iff` `isOpen_empty` `Set.subset_insert` `Set.mem_iUnion_of_mem` `Set.empty_inter`
`integrableOn_compact_subset` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `Set` `Set.instHasSubset` `IsCompact`	`MeasureTheory.IntegrableOn`	—	`integrableOn_isCompact` `mono_set`
`integrableOn_isCompact` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `IsCompact`	`MeasureTheory.IntegrableOn`	—	`IsCompact.induction_on` `MeasureTheory.integrableOn_empty` `MeasureTheory.IntegrableOn.mono_set` `MeasureTheory.integrableOn_union`
`mono` 📖	—	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.AEStronglyMeasurable` `Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable.mono` `MeasureTheory.AEStronglyMeasurable.restrict` `MeasureTheory.ae_restrict_of_ae`
`mono_enorm` 📖	—	`MeasureTheory.LocallyIntegrableOn` `MeasureTheory.AEStronglyMeasurable` `Filter.Eventually` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousENorm.toENorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable.mono_enorm` `MeasureTheory.AEStronglyMeasurable.restrict` `MeasureTheory.ae_restrict_of_ae`
`mono_set` 📖	—	`MeasureTheory.LocallyIntegrableOn` `Set` `Set.instHasSubset`	—	—	`MeasureTheory.IntegrableAtFilter.filter_mono` `nhdsWithin_mono`
`mul_continuousOn` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `ContinuousOn` `IsLocallyClosed`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`MeasureTheory.locallyIntegrableOn_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.IntegrableOn.mul_continuousOn` `ContinuousOn.mono`
`neg` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.IntegrableAtFilter.neg`
`norm` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Real` `Real.pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`MeasureTheory.Integrable.norm`
`smul_continuousOn` 📖	mathematical	`IsLocallyClosed` `MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `ContinuousOn` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`MeasureTheory.locallyIntegrableOn_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.IntegrableOn.smul_continuousOn` `ContinuousOn.mono`
`sub` 📖	mathematical	`MeasureTheory.LocallyIntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`MeasureTheory.IntegrableAtFilter.sub`

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyIntegrable` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`MeasureTheory.LocallyIntegrable`	—	`MeasureTheory.Measure.finiteAt_nhds` `MeasureTheory.IntegrableOn.eq_1` `MeasureTheory.memLp_one_iff_integrable` `mono_exponent` `MeasureTheory.Restrict.isFiniteMeasure` `restrict`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyIntegrable` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`MeasureTheory.LocallyIntegrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.Measure.finiteAt_nhds` `exists_Icc_mem_subset_of_mem_nhds` `LE.le.trans` `MonotoneOn.integrableOn_of_measure_ne_top` `monotoneOn` `isLeast_Icc` `isGreatest_Icc` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `measurableSet_Icc` `BorelSpace.opensMeasurable` `OrderTopology.to_orderClosedTopology`

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrableOn_isCompact` 📖	mathematical	`IsCompact` `MonotoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.memLp_one_iff_integrable` `memLp_isCompact`
`integrableOn_of_measure_ne_top` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `IsLeast` `Preorder.toLE` `IsGreatest` `MeasurableSet`	`MeasureTheory.IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.memLp_one_iff_integrable` `memLp_of_measure_ne_top`
`memLp_isCompact` 📖	mathematical	`IsCompact` `MonotoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.Measure.restrict`	—	`Set.eq_empty_or_nonempty` `MeasureTheory.Measure.restrict_empty` `memLp_of_measure_ne_top` `IsCompact.isLeast_sInf` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `IsCompact.isGreatest_sSup` `instClosedIciTopology` `LT.lt.ne` `IsCompact.measure_lt_top` `IsCompact.measurableSet` `BorelSpace.opensMeasurable` `T25Space.t2Space` `T3Space.t25Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space`
`memLp_of_measure_ne_top` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `IsLeast` `Preorder.toLE` `IsGreatest` `MeasurableSet`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top` `memLp_top` `instIsEmptyFalse` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `le_top`
`memLp_top` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `IsLeast` `Preorder.toLE` `IsGreatest` `MeasurableSet`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `Top.top` `ENNReal` `instTopENNReal` `MeasureTheory.Measure.restrict`	—	`Metric.isBounded_of_bddAbove_of_bddBelow` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `isBounded_iff_forall_norm_le` `MeasureTheory.memLp_top_const` `MeasureTheory.MemLp.mono` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `aemeasurable_restrict_of_monotoneOn` `OrderTopology.to_orderClosedTopology` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_iff'` `MeasureTheory.ae_of_all` `LE.le.trans` `Set.mem_image_of_mem` `le_abs_self`

---

← Back to Index