Count

📁 Source: Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean

Statistics

Metric	Count
Definitions	0
Theorems eLpNorm_count_lt_top, eLpNorm_count_lt_top_of_lt, eLpNorm_dirac, enorm_le_eLpNorm_count	4
Total	4

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eLpNorm_count_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm Measure.count Top.top instTopENNReal ENorm.enorm	—	LE.le.trans_lt enorm_le_eLpNorm_count eLpNorm_count_lt_top_of_lt
eLpNorm_count_lt_top_of_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm Top.top instTopENNReal	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm Measure.count Top.top instTopENNReal	—	ENNReal.zero_lt_top LE.le.trans_lt essSup_le_of_ae_le Filter.univ_mem' Measure.instOuterMeasureClass Finset.le_sup Finset.mem_univ Finset.sup_lt_iff ENNReal.rpow_lt_top_iff_of_pos one_div inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ENNReal.toReal_pos lintegral_count tsum_eq_sum instIsEmptyFalse SummationFilter.instLeAtTopUnconditional
eLpNorm_dirac 📖	mathematical	—	eLpNorm ContinuousENorm.toENorm Measure.dirac ENorm.enorm	—	Measure.instOuterMeasureClass ae_dirac_eq csInf_Ici lintegral_dirac one_div ENNReal.rpow_rpow_inv
enorm_le_eLpNorm_count 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm eLpNorm Measure.count	—	eLpNorm_dirac IsScalarTower.right Measure.restrict_singleton Measure.count_singleton' one_smul eLpNorm_restrict_le

---

← Back to Index