Indicator

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

Statistics

Metric	Count
Definitions	0
Theorems exists_eLpNorm_indicator_compl_lt, indicator, piecewise, eLpNormEssSup_indicator_const_eq, eLpNormEssSup_indicator_const_le, eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict, eLpNormEssSup_indicator_le, eLpNormEssSup_piecewise, eLpNorm_indicator_const, eLpNorm_indicator_const', eLpNorm_indicator_const_le, eLpNorm_indicator_const₀, eLpNorm_indicator_eq_eLpNorm_restrict, eLpNorm_indicator_le, eLpNorm_indicator_sub_le_of_dist_bdd, eLpNorm_restrict_le, eLpNorm_sub_le_of_dist_bdd, eLpNorm_top_piecewise, memLp_indicator_const, memLp_indicator_iff_restrict	20
Total	20

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eLpNormEssSup_indicator_const_eq 📖	mathematical	—	eLpNormEssSup ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENorm.enorm	—	le_antisymm eLpNormEssSup_indicator_const_le Measure.instOuterMeasureClass ae_iff ae_lt_of_essSup_lt Filter.isBounded_le_of_top measure_mono_null Set.mem_setOf_eq Set.indicator_of_mem le_refl
eLpNormEssSup_indicator_const_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNormEssSup ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENorm.enorm	—	eLpNormEssSup_measure_zero zero_le ENNReal.instCanonicallyOrderedAdd LE.le.trans eLpNormEssSup_indicator_le Eq.le eLpNormEssSup_const
eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict 📖	mathematical	MeasurableSet	eLpNormEssSup ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Measure.restrict	—	eLpNorm_indicator_eq_eLpNorm_restrict
eLpNormEssSup_indicator_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNormEssSup ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid	—	essSup_mono_ae Filter.Eventually.of_forall Measure.instOuterMeasureClass enorm_indicator_eq_indicator_enorm Set.indicator_le_self ENNReal.instCanonicallyOrderedAdd
eLpNormEssSup_piecewise 📖	mathematical	MeasurableSet	eLpNormEssSup ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.piecewise ENNReal ENNReal.instMax Measure.restrict Compl.compl Set Set.instCompl	—	ENNReal.essSup_piecewise Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem
eLpNorm_indicator_const 📖	mathematical	MeasurableSet	eLpNorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENorm.enorm Real ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	eLpNorm_indicator_const₀ MeasurableSet.nullMeasurableSet
eLpNorm_indicator_const' 📖	mathematical	MeasurableSet	eLpNorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENorm.enorm Real ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	eLpNorm_exponent_top eLpNormEssSup_indicator_const_eq div_zero ENNReal.rpow_zero mul_one eLpNorm_indicator_const
eLpNorm_indicator_const_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENorm.enorm Real ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	eq_or_ne eLpNorm_exponent_zero div_zero ENNReal.rpow_zero mul_one ENNReal.instCanonicallyOrderedAdd eLpNorm_exponent_top eLpNormEssSup_indicator_const_le eLpNorm_mono_enorm enorm_indicator_le_of_subset subset_toMeasurable eLpNorm_indicator_const measurableSet_toMeasurable measure_toMeasurable
eLpNorm_indicator_const₀ 📖	mathematical	NullMeasurableSet	eLpNorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENorm.enorm Real ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	ENNReal.toReal_pos eLpNorm_eq_lintegral_rpow_enorm_toReal Set.comp_indicator_const enorm_zero ENNReal.zero_rpow_of_pos lintegral_indicator_const₀ ENNReal.mul_rpow_of_nonneg le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one ENNReal.rpow_mul mul_one_div_cancel LT.lt.ne' ENNReal.rpow_one
eLpNorm_indicator_eq_eLpNorm_restrict 📖	mathematical	MeasurableSet	eLpNorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid Measure.restrict	—	eLpNorm_exponent_zero eLpNorm_exponent_top enorm_indicator_eq_indicator_enorm ENNReal.essSup_indicator_eq_essSup_restrict eLpNorm_eq_lintegral_rpow_enorm_toReal lintegral_indicator Set.indicator_comp_of_zero ENNReal.zero_rpow_of_pos ENNReal.toReal_pos
eLpNorm_indicator_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid	—	eLpNorm_mono_ae' Filter.Eventually.of_forall Measure.instOuterMeasureClass enorm_indicator_eq_indicator_enorm Set.indicator_le_self ENNReal.instCanonicallyOrderedAdd
eLpNorm_indicator_sub_le_of_dist_bdd 📖	mathematical	MeasurableSet Real Real.instLE Real.instZero Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	eLpNorm_exponent_zero div_zero ENNReal.rpow_zero mul_one ENNReal.instCanonicallyOrderedAdd Set.indicator_of_mem Pi.sub_apply dist_eq_norm Real.norm_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.indicator_of_notMem norm_zero le_imp_le_of_le_of_le eLpNorm_mono le_refl eLpNorm_indicator_const ofReal_norm_eq_enorm
eLpNorm_restrict_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm Measure.restrict	—	eLpNorm_mono_measure Measure.restrict_le_self
eLpNorm_sub_le_of_dist_bdd 📖	mathematical	MeasurableSet Real Real.instLE Real.instZero Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instHasSubset Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal ENNReal.instPowReal DFunLike.coe Measure Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	Set.indicator_eq_self HasSubset.Subset.trans Set.instIsTransSubset Function.support_sub Set.union_subset eLpNorm_indicator_sub_le_of_dist_bdd
eLpNorm_top_piecewise 📖	mathematical	MeasurableSet	eLpNorm ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.piecewise Top.top ENNReal instTopENNReal ENNReal.instMax Measure.restrict Compl.compl Set Set.instCompl	—	eLpNormEssSup_piecewise
memLp_indicator_const 📖	mathematical	MeasurableSet NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Set.indicator	—	memLp_indicator_iff_restrict MemLp.zero Ne.lt_top memLp_const Restrict.isFiniteMeasure
memLp_indicator_iff_restrict 📖	mathematical	MeasurableSet	MemLp ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid Measure.restrict	—	aestronglyMeasurable_indicator_iff eLpNorm_indicator_eq_eLpNorm_restrict

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eLpNorm_indicator_compl_lt 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Top.top instTopENNReal MeasureTheory.eLpNorm Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Compl.compl Set.instCompl	—	eq_or_ne MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass Set.compl_empty Set.indicator_univ MeasureTheory.eLpNorm_exponent_zero pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd MeasureTheory.exists_setLIntegral_compl_lt LT.lt.ne MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict MeasurableSet.compl MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal one_div ENNReal.rpow_inv_lt_iff
indicator 📖	mathematical	MeasurableSet MeasureTheory.MemLp ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm	Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid	—	MeasureTheory.AEStronglyMeasurable.indicator aestronglyMeasurable lt_of_le_of_lt MeasureTheory.eLpNorm_indicator_le Ne.lt_top eLpNorm_ne_top
piecewise 📖	mathematical	MeasurableSet MeasureTheory.MemLp ContinuousENorm.toENorm ESeminormedAddMonoid.toContinuousENorm MeasureTheory.Measure.restrict Compl.compl Set Set.instCompl	Set.piecewise	—	MeasureTheory.AEStronglyMeasurable.piecewise eq_or_ne MeasureTheory.eLpNorm_top_piecewise max_lt MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top MeasureTheory.lintegral_add_compl ENNReal.add_lt_top Set.piecewise_eq_of_mem MeasureTheory.setLIntegral_congr_fun MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top Set.piecewise_eq_of_notMem MeasurableSet.compl

---

← Back to Index