Documentation Verification Report

LpOrder

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

Statistics

Metric	Count
Definitions `instLattice`	1
Theorems `coeFn_abs`, `coeFn_inf`, `coeFn_le`, `coeFn_nonneg`, `coeFn_sup`, `instAddLeftMono`, `instHasSolidNorm`, `instIsOrderedAddMonoid`, `instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology`, `abs`, `inf`, `sup`	12
Total	13

MeasureTheory.Lp

Definitions

Name	Category	Theorems
`instLattice` 📖	CompOp	4 math math: `instHasSolidNorm`, `coeFn_sup`, `coeFn_abs`, `coeFn_inf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_abs` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `abs` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instLattice` `AddSubgroup.toAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun.coeFn_abs` `HasSolidNorm.toTopologicalLattice`
`coeFn_inf` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `instLattice` `Pi.instMinForall_mathlib`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun.coeFn_inf` `TopologicalLattice.toContinuousInf` `HasSolidNorm.toTopologicalLattice`
`coeFn_le` 📖	mathematical	—	`Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun.instPreorder`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.instOuterMeasureClass` `Subtype.coe_le_coe` `MeasureTheory.AEEqFun.coeFn_le`
`coeFn_nonneg` 📖	mathematical	—	`Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun.instPreorder` `AddSubgroup.zero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.instOuterMeasureClass` `coeFn_le` `coeFn_zero` `Filter.mp_mem` `Filter.univ_mem'`
`coeFn_sup` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instLattice` `Pi.instMaxForall_mathlib`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun.coeFn_sup` `TopologicalLattice.toContinuousSup` `HasSolidNorm.toTopologicalLattice`
`instAddLeftMono` 📖	mathematical	—	`AddLeftMono` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `AddSubgroup.add` `Preorder.toLE` `MeasureTheory.AEEqFun.instPreorder` `PartialOrder.toPreorder`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.instOuterMeasureClass` `coeFn_le` `Filter.mp_mem` `coeFn_add` `Filter.univ_mem'` `Pi.add_apply` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `le_rfl`
`instHasSolidNorm` 📖	mathematical	—	`HasSolidNorm` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instNormedAddCommGroup` `instLattice`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `ENNReal.toReal_le_toReal` `eLpNorm_ne_top` `MeasureTheory.eLpNorm_mono_ae` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `coeFn_abs` `coeFn_le` `Filter.univ_mem'` `HasSolidNorm.solid`
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `AddCommGroup.toAddCommMonoid` `AddSubgroup.toAddCommGroup` `MeasureTheory.AEEqFun.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `Subtype.partialOrder` `MeasureTheory.AEEqFun.instPartialOrder`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `add_le_add_left` `covariant_swap_add_of_covariant_add` `instAddLeftMono`
`instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology` 📖	mathematical	—	`OrderClosedTopology` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instNormedAddCommGroup` `Subtype.preorder` `MeasureTheory.AEEqFun.instPreorder` `PartialOrder.toPreorder`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `isClosed_le_of_isClosed_nonneg` `instIsOrderedAddMonoid` `IsTopologicalAddGroup.to_continuousSub` `IsSeqClosed.isClosed` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae` `MeasureTheory.tendstoInMeasure_of_tendsto_Lp` `Filter.mp_mem` `countable_iInter_mem` `MeasureTheory.instCountableInterFilter` `instCountableNat` `Filter.univ_mem'` `ge_of_tendsto'` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Set.mem_iInter`

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`abs` `Pi.instLattice` `Pi.addGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sup` `neg`
`inf` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`mono'` `add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `norm` `MeasureTheory.AEStronglyMeasurable.inf` `TopologicalLattice.toContinuousInf` `HasSolidNorm.toTopologicalLattice` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `norm_inf_le_add`
`sup` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`mono'` `add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `norm` `MeasureTheory.AEStronglyMeasurable.sup` `TopologicalLattice.toContinuousSup` `HasSolidNorm.toTopologicalLattice` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `norm_sup_le_add`

---

← Back to Index