Norm

Statistics

Metric	Count
Definitions	0
Theorems `lintegral_enorm_of_ae_nonneg`, `lintegral_enorm_of_nonneg`, `lintegral_ofReal_le_lintegral_enorm`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`lintegral_enorm_of_ae_nonneg` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `Real.instZero`	`lintegral` `ENorm.enorm` `NNNorm.toENorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.normedAddCommGroup` `ENNReal.ofReal`	—	`Measure.instOuterMeasureClass` `lintegral_congr_ae` `Filter.mp_mem` `Filter.univ_mem'` `Real.enorm_eq_ofReal`
`lintegral_enorm_of_nonneg` 📖	mathematical	`Pi.hasLe` `Real` `Real.instLE` `Pi.instZero` `Real.instZero`	`lintegral` `ENorm.enorm` `NNNorm.toENorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.normedAddCommGroup` `ENNReal.ofReal`	—	`lintegral_enorm_of_ae_nonneg` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`lintegral_ofReal_le_lintegral_enorm` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `ENNReal.ofReal` `ENorm.enorm` `Real` `NNNorm.toENorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.normedAddCommGroup`	—	`lintegral_mono` `ENNReal.ofReal_le_ofReal` `Real.norm_eq_abs` `le_abs_self`

---