Indicator

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

Statistics

Metric	Count
Definitions const, constL, constₗ, indicatorConstLp	4
Theorems memLp_of_hasCompactSupport, memLp_of_bound, coeFn_const, constL_apply, const_val, constₗ_apply, indicatorConstLp_compMeasurePreserving, norm_const, norm_const', norm_constL_le, norm_const_le, toLp_const, continuous_indicatorConstLp_set, dist_indicatorConstLp_eq_norm, edist_indicatorConstLp_eq_enorm, enorm_indicatorConstLp_le, exists_eLpNorm_indicator_le, indicatorConstLp_add, indicatorConstLp_coeFn, indicatorConstLp_coeFn_mem, indicatorConstLp_coeFn_notMem, indicatorConstLp_disjoint_union, indicatorConstLp_empty, indicatorConstLp_eq_toSpanSingleton_compLp, indicatorConstLp_inj, indicatorConstLp_sub, indicatorConstLp_univ, memLp_add_of_disjoint, nnnorm_indicatorConstLp_le, norm_indicatorConstLp, norm_indicatorConstLp', norm_indicatorConstLp_le, norm_indicatorConstLp_top, tendsto_indicatorConstLp_set	34
Total	38

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
memLp_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.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm	—	memLp_top_of_hasCompactSupport MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top image_eq_zero_of_notMem_tsupport LT.lt.ne IsCompact.measure_lt_top le_top

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
memLp_of_bound 📖	mathematical	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.memLp_top_of_bound MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top image_eq_zero_of_notMem_tsupport LT.lt.ne IsCompact.measure_lt_top le_top

MeasureTheory

Definitions

Name	Category	Theorems
indicatorConstLp 📖	CompOp	48 math math: integrable_indicatorConstLp, condExpInd_of_measurable, DomAddAct.mk_vadd_indicatorConstLp, norm_indicatorConstLp_le, L1.setToL1_indicatorConstLp, L2.inner_indicatorConstLp_eq_inner_setIntegral, Lp.indicatorConstLp_compMeasurePreserving, norm_indicatorConstLp, norm_indicatorConstLp_top, condExpL2_indicator_ae_eq_smul, setIntegral_condExpL2_indicator, lintegral_nnnorm_condExpL2_indicator_le, edist_indicatorConstLp_eq_enorm, setLIntegral_nnnorm_condExpL2_indicator_le, mem_lpMeas_indicatorConstLp, integral_indicatorConstLp, enorm_indicatorConstLp_le, condExpL1CLM_indicatorConstLp, indicatorConstLp_univ, lpMeasToLpTrimLie_symm_indicator, Measure.MeasureDense.indicatorConstLp_subset_closure, L2.inner_indicatorConstLp_one, L2.inner_indicatorConstLp_indicatorConstLp, DomMulAct.mk_smul_indicatorConstLp, L2.real_inner_indicatorConstLp_one_indicatorConstLp_one, condExpL2_indicator_of_measurable, indicatorConstLp_inj, condExpL2_indicator_eq_toSpanSingleton_comp, lintegral_nnnorm_condExpL2_indicator_le_real, indicatorConstLp_add, L2.inner_indicatorConstLp_eq_setIntegral_inner, nnnorm_indicatorConstLp_le, setIntegral_indicatorConstLp, indicatorConstLp_sub, integrable_condExpL2_indicator, L2.inner_indicatorConstLp_one_indicatorConstLp_one, continuous_indicatorConstLp_set, Lp.simpleFunc.coe_indicatorConst, tendsto_indicatorConstLp_set, norm_indicatorConstLp', condExpIndSMul_ae_eq_smul, indicatorConstLp_eq_toSpanSingleton_compLp, indicatorConstLp_disjoint_union, indicatorConstLp_coeFn, L1.setToL1_const, indicatorConstLp_empty, dist_indicatorConstLp_eq_norm, condExpL2_indicator_nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_indicatorConstLp_set 📖	mathematical	MeasurableSet Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff nhds ENNReal.instTopologicalSpace instZeroENNReal	Continuous AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNormedAddCommGroup indicatorConstLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_iff_continuousAt tendsto_indicatorConstLp_set
dist_indicatorConstLp_eq_norm 📖	mathematical	MeasurableSet	Dist.dist AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instDist indicatorConstLp Norm.norm Lp.instNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff MeasurableSet.symmDiff measure_symmDiff_ne_top	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasurableSet.symmDiff measure_symmDiff_ne_top Lp.dist_edist edist_indicatorConstLp_eq_enorm
edist_indicatorConstLp_eq_enorm 📖	mathematical	MeasurableSet	EDist.edist AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instEDist indicatorConstLp ENorm.enorm NNNorm.toENorm Lp.instNNNorm symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff MeasurableSet.symmDiff measure_symmDiff_ne_top	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasurableSet.symmDiff measure_symmDiff_ne_top Lp.edist_toLp_toLp eLpNorm_indicator_sub_indicator Lp.enorm_toLp
enorm_indicatorConstLp_le 📖	mathematical	MeasurableSet	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp NNNorm.toENorm Lp.instNNNorm indicatorConstLp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Real ENNReal.instPowReal DFunLike.coe Measure Set Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.enorm_def one_div ENNReal.coe_rpow_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ENNReal.coe_toNNReal ENNReal.coe_le_coe nnnorm_indicatorConstLp_le
exists_eLpNorm_indicator_le 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal ENNReal Preorder.toLE ENNReal.instPartialOrder eLpNorm 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	—	eq_or_ne zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing eLpNorm_exponent_zero ENNReal.instCanonicallyOrderedAdd bot_lt_iff_ne_bot div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_le_one Real.instZeroLEOneClass ENNReal.toReal_nonneg ENNReal.toReal_pos LT.lt.ne' ENNReal.tendsto_coe one_div NNReal.zero_rpow MulZeroClass.mul_zero Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul NNReal.instIsTopologicalSemiring ContinuousAt.tendsto NNReal.continuousAt_rpow_const Ne.bot_lt Filter.HasBasis.eventually_iff NNReal.nhds_zero_basis Filter.Tendsto.eventually_le_const instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology exists_between NNReal.instDenselyOrdered ENNReal.coe_rpow_of_nonneg le_imp_le_of_le_of_le eLpNorm_indicator_const_le le_refl mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid ENNReal.rpow_le_rpow le_of_lt div_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
indicatorConstLp_add 📖	mathematical	MeasurableSet	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.add indicatorConstLp AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MemLp.add IsTopologicalAddGroup.toContinuousAdd Set.indicator_add MemLp.toLp.congr_simp
indicatorConstLp_coeFn 📖	mathematical	MeasurableSet	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AEEqFun AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp indicatorConstLp Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	MemLp.coeFn_toLp memLp_indicator_const
indicatorConstLp_coeFn_mem 📖	mathematical	MeasurableSet	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Filter.Eventually.mono Measure.instOuterMeasureClass indicatorConstLp_coeFn Set.indicator_of_mem
indicatorConstLp_coeFn_notMem 📖	mathematical	MeasurableSet	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Filter.Eventually.mono Measure.instOuterMeasureClass indicatorConstLp_coeFn Set.indicator_of_notMem
indicatorConstLp_disjoint_union 📖	mathematical	MeasurableSet Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	indicatorConstLp Set.instUnion MeasurableSet.union AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.add	—	Lp.ext MeasurableSet.union SeminormedAddCommGroup.toIsTopologicalAddGroup Mathlib.Tactic.GCongr.rel_imp_rel Measure.instOuterMeasureClass instIsTransOfTrans Filter.EventuallyEq.refl Filter.EventuallyEq.symm Lp.coeFn_add indicatorConstLp_coeFn Filter.EventuallyEq.trans Set.indicator_union_of_disjoint Filter.EventuallyEq.fun_add
indicatorConstLp_empty 📖	mathematical	—	indicatorConstLp Set Set.instEmptyCollection MeasurableSet.empty AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.zero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasurableSet.empty MemLp.toLp.congr_simp Set.indicator_empty'
indicatorConstLp_eq_toSpanSingleton_compLp 📖	mathematical	MeasurableSet	indicatorConstLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat ContinuousLinearMap.compLp Real Real.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedField.toNormedSpace NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real.semiring RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toSpanSingleton UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Real.pseudoMetricSpace IsBoundedSMul.continuousSMul Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toIsBoundedSMul Real.instOne	—	Lp.ext Nat.instAtLeastTwoHAddOfNat RingHomIsometric.ids IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.EventuallyEq.trans Measure.instOuterMeasureClass indicatorConstLp_coeFn ContinuousLinearMap.coeFn_compLp Filter.Eventually.mono Set.indicator_of_mem one_smul Set.indicator_of_notMem zero_smul Filter.EventuallyEq.symm Filter.EventuallyEq.eq_1
indicatorConstLp_inj 📖	mathematical	MeasurableSet	indicatorConstLp Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Measure.instOuterMeasureClass Filter.indicator_const_eventuallyEq
indicatorConstLp_sub 📖	mathematical	MeasurableSet	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddSubgroup.sub indicatorConstLp SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MemLp.sub Set.indicator_sub MemLp.toLp.congr_simp
indicatorConstLp_univ 📖	mathematical	—	indicatorConstLp Set.univ MeasurableSet.univ measure_ne_top DFunLike.coe AddMonoidHom AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike Lp.const	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasurableSet.univ measure_ne_top memLp_const MemLp.toLp_const indicatorConstLp.eq_1 Set.indicator_univ MemLp.toLp.congr_simp
memLp_add_of_disjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Set.indicator_add_eq_left MemLp.indicator measurableSet_support OpensMeasurableSpace.toMeasurableSingletonClass BorelSpace.opensMeasurable T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace StronglyMeasurable.measurable PseudoEMetricSpace.pseudoMetrizableSpace Set.indicator_add_eq_right MemLp.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
nnnorm_indicatorConstLp_le 📖	mathematical	MeasurableSet	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNNNorm indicatorConstLp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Real NNReal.instPowReal ENNReal.toNNReal DFunLike.coe Measure Set ENNReal Measure.instFunLike DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	norm_indicatorConstLp_le
norm_indicatorConstLp 📖	mathematical	MeasurableSet	Norm.norm AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNorm indicatorConstLp Real Real.instMul NormedAddCommGroup.toNorm Real.instPow Measure.real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.norm_def eLpNorm_congr_ae indicatorConstLp_coeFn eLpNorm_indicator_const ENNReal.toReal_mul measureReal_def ENNReal.toReal_rpow toReal_enorm
norm_indicatorConstLp' 📖	mathematical	MeasurableSet	Norm.norm AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNorm indicatorConstLp Real Real.instMul NormedAddCommGroup.toNorm Real.instPow Measure.real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ENNReal.toReal_top div_zero Real.rpow_zero mul_one norm_indicatorConstLp_top norm_indicatorConstLp
norm_indicatorConstLp_le 📖	mathematical	MeasurableSet	Real Real.instLE Norm.norm AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Lp.instNorm indicatorConstLp Real.instMul NormedAddCommGroup.toNorm Real.instPow Measure.real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup indicatorConstLp.eq_1 Lp.norm_toLp ENNReal.toReal_le_of_le_ofReal mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg Real.rpow_nonneg measureReal_nonneg LE.le.trans_eq eLpNorm_indicator_const_le ENNReal.ofReal_mul ofReal_norm measureReal_def ENNReal.toReal_rpow ENNReal.ofReal_toReal ENNReal.rpow_ne_top_of_nonneg Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one ENNReal.toReal_nonneg
norm_indicatorConstLp_top 📖	mathematical	MeasurableSet	Norm.norm AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp Top.top ENNReal instTopENNReal Lp.instNorm indicatorConstLp NormedAddCommGroup.toNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Lp.norm_def eLpNorm_congr_ae indicatorConstLp_coeFn eLpNorm_indicator_const' ENNReal.top_ne_zero ENNReal.toReal_top div_zero ENNReal.rpow_zero mul_one toReal_enorm
tendsto_indicatorConstLp_set 📖	mathematical	MeasurableSet Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff nhds ENNReal.instTopologicalSpace instZeroENNReal	AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp indicatorConstLp Lp.instNormedAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_iff_dist_tendsto_zero LT.lt.ne' LT.lt.trans_le one_pos IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.out MeasurableSet.symmDiff measure_symmDiff_ne_top dist_indicatorConstLp_eq_norm norm_indicatorConstLp one_div Real.zero_rpow MulZeroClass.mul_zero Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds Filter.Tendsto.rpow_const Filter.Tendsto.comp ENNReal.tendsto_toReal ENNReal.zero_ne_top PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing

MeasureTheory.Lp

Definitions

Name	Category	Theorems
const 📖	CompOp	11 math math: coeFn_const, MeasureTheory.indicatorConstLp_univ, norm_const_le, constₗ_apply, norm_const', norm_const, DomAddAct.vadd_Lp_const, constL_apply, DomMulAct.smul_Lp_const, const_val, MeasureTheory.MemLp.toLp_const
constL 📖	CompOp	2 math math: norm_constL_le, constL_apply
constₗ 📖	CompOp	1 math math: constₗ_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_const 📖	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 DFunLike.coe AddMonoidHom SeminormedAddCommGroup.toIsTopologicalAddGroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike const	—	MeasureTheory.AEEqFun.coeFn_const
constL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNormedAddCommGroup instModule ContinuousLinearMap.funLike constL AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike const	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
const_val 📖	mathematical	—	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 DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike const MeasureTheory.AEEqFun.const	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
constₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring 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 ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup MeasureTheory.AEEqFun.instAddCommGroup NormedAddCommGroup.toAddCommGroup instModule LinearMap.instFunLike constₗ AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike const	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
indicatorConstLp_compMeasurePreserving 📖	mathematical	MeasurableSet MeasureTheory.MeasurePreserving	DFunLike.coe AddMonoidHom 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 AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike compMeasurePreserving MeasureTheory.indicatorConstLp Set.preimage MeasurableSet.preimage MeasureTheory.MeasurePreserving.measurable	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
norm_const 📖	mathematical	—	Norm.norm 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 instNorm DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike const Real Real.instMul NormedAddCommGroup.toNorm Real.instPow MeasureTheory.Measure.real Set.univ DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.memLp_const MeasureTheory.MemLp.toLp_const norm_toLp MeasureTheory.eLpNorm_const MeasureTheory.measureReal_def ENNReal.toReal_mul toReal_enorm ENNReal.toReal_rpow
norm_const' 📖	mathematical	—	Norm.norm 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 instNorm DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike const Real Real.instMul NormedAddCommGroup.toNorm Real.instPow MeasureTheory.Measure.real Set.univ DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.memLp_const MeasureTheory.MemLp.toLp_const norm_toLp MeasureTheory.eLpNorm_const' MeasureTheory.measureReal_def ENNReal.toReal_mul toReal_enorm ENNReal.toReal_rpow
norm_constL_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNormedAddCommGroup NormedSpace.toModule instModule NormedSpace.toIsBoundedSMul ContinuousLinearMap.hasOpNorm instNormedSpace constL Real.instPow MeasureTheory.Measure.real Set.univ DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	LinearMap.mkContinuous_norm_le NormedSpace.toIsBoundedSMul Real.rpow_nonneg MeasureTheory.measureReal_nonneg
norm_const_le 📖	mathematical	—	Real Real.instLE Norm.norm 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 instNorm DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike const Real.instMul NormedAddCommGroup.toNorm Real.instPow MeasureTheory.Measure.real Set.univ DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne ENNReal.toReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasurableSet.univ MeasureTheory.measure_ne_top MeasureTheory.indicatorConstLp_univ MeasureTheory.norm_indicatorConstLp_le

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLp_const 📖	mathematical	—	toLp MeasureTheory.memLp_const DFunLike.coe AddMonoidHom 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 AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike MeasureTheory.Lp.const	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.memLp_const

---

← Back to Index