LpNorm

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

Statistics

Metric	Count
Definitions	0
Theorems ae_le_lpNorm_exponent_top, lpNorm_abs, lpNorm_add_le, lpNorm_add_le', lpNorm_conj, lpNorm_const, lpNorm_const', lpNorm_const_smul, lpNorm_div_natCast, lpNorm_eq_integral_norm_rpow_toReal, lpNorm_eq_zero, lpNorm_expect_le, lpNorm_exponent_top_eq_essSup, lpNorm_exponent_zero, lpNorm_fun_abs, lpNorm_fun_div_natCast, lpNorm_fun_mul_natCast, lpNorm_fun_natCast_mul, lpNorm_fun_neg, lpNorm_fun_zero, lpNorm_le_add_lpNorm_add, lpNorm_le_lpNorm_add_lpNorm_sub, lpNorm_le_lpNorm_add_lpNorm_sub', lpNorm_measure_zero, lpNorm_mono_real, lpNorm_mul_natCast, lpNorm_natCast_mul, lpNorm_neg, lpNorm_nnreal_eq_integral_norm_rpow, lpNorm_nonneg, lpNorm_norm, lpNorm_nsmul, lpNorm_of_isEmpty, lpNorm_of_not_aestronglyMeasurable, lpNorm_of_not_memLp, lpNorm_one, lpNorm_one', lpNorm_one_eq_integral_norm, lpNorm_smul_measure_of_ne_top, lpNorm_smul_measure_of_ne_zero, lpNorm_sub_comm, lpNorm_sub_le, lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub, lpNorm_sum_le, lpNorm_zero, ofReal_lpNorm, toReal_eLpNorm	47
Total	47

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_le_lpNorm_exponent_top 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Top.top ENNReal instTopENNReal	Filter.Eventually Real Real.instLE Norm.norm NormedAddCommGroup.toNorm lpNorm ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass toReal_eLpNorm MemLp.aestronglyMeasurable ENNReal.ofReal_le_iff_le_toReal LT.lt.ne ofReal_norm ae_le_eLpNormEssSup
lpNorm_abs 📖	mathematical	AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	lpNorm Real.normedAddCommGroup abs Pi.instLattice Real.lattice Pi.addGroup Real.instAddGroup	—	lpNorm_norm
lpNorm_add_le 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAdd	—	toReal_eLpNorm MemLp.aestronglyMeasurable MemLp.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup ENNReal.toReal_add MemLp.eLpNorm_ne_top ENNReal.toReal_mono ENNReal.add_ne_top eLpNorm_add_le lpNorm_of_not_memLp add_sub_cancel_left MemLp.sub add_zero
lpNorm_add_le' 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAdd	—	add_comm lpNorm_add_le
lpNorm_conj 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.commSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd Pi.starRing' RCLike.toStarRing	—	lpNorm_norm AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable RCLike.borelSpace secondCountable_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real Measurable.comp_aemeasurable Continuous.measurable ContinuousStar.continuous_star RCLike.instContinuousStar AEStronglyMeasurable.aemeasurable RCLike.norm_conj lpNorm_of_not_aestronglyMeasurable RingHomCompTriple.comp_apply RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd
lpNorm_const 📖	mathematical	—	lpNorm Real Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instPow Measure.real Set.univ Real.instInv ENNReal.toReal	—	eLpNorm_const one_div ENNReal.toReal_mul toReal_enorm ENNReal.toReal_rpow
lpNorm_const' 📖	mathematical	—	lpNorm Real Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instPow Measure.real Set.univ Real.instInv ENNReal.toReal	—	eLpNorm_const' one_div ENNReal.toReal_mul toReal_enorm ENNReal.toReal_rpow
lpNorm_const_smul 📖	mathematical	—	lpNorm Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid Real Real.instMul NNReal.toReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	AEStronglyMeasurable.const_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormSMulClass.toIsBoundedSMul eLpNorm_const_smul ENNReal.toReal_mul toReal_enorm eq_or_ne zero_smul lpNorm_zero nnnorm_zero MulZeroClass.zero_mul lpNorm_of_not_aestronglyMeasurable inv_smul_smul₀ MulZeroClass.mul_zero
lpNorm_div_natCast 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Pi.instDiv DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Pi.instNatCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instDivInvMonoid Real.instNatCast	—	eq_div_iff ne_of_gt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd lpNorm_mul_natCast IsUnit.div_mul_cancel
lpNorm_eq_integral_norm_rpow_toReal 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lpNorm Real Real.instPow integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal Real.instInv	—	toReal_eLpNorm eLpNorm_eq_lintegral_rpow_enorm_toReal ENNReal.toReal_rpow integral_toReal AEMeasurable.pow_const ENNReal.hasMeasurablePow AEMeasurable.ennreal_ofReal AEMeasurable.norm BorelSpace.opensMeasurable AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Filter.Eventually.of_forall Measure.instOuterMeasureClass ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg toReal_enorm one_div
lpNorm_eq_zero 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	lpNorm Real Real.instZero Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Measure.instOuterMeasureClass toReal_eLpNorm MemLp.aestronglyMeasurable eLpNorm_eq_zero_iff MemLp.eLpNorm_ne_top
lpNorm_expect_le 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Finset.expect Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.Function.module NNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Real.instAddCommMonoid Algebra.toModule instCommSemiringNNRat Real.semiring DivisionSemiring.toNNRatAlgebra Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike	—	RCLike.charZero_rclike Finset.eq_empty_or_nonempty Finset.expect_empty lpNorm_zero le_inv_smul_iff_of_pos PosSMulMono.nnrat_of_rat IsScalarTower.nnrat Rat.instCharZero PosSMulStrictMono.toPosSMulMono LinearOrderedField.toPosSMulStrictMono_rat Real.instIsStrictOrderedRing PosSMulReflectLT.toPosSMulReflectLE instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors PosSMulMono.toPosSMulReflectLT Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one NNRat.instCharZero Finset.Nonempty.card_pos Nat.cast_smul_eq_nsmul lpNorm_nsmul Finset.card_smul_expect lpNorm_sum_le
lpNorm_exponent_top_eq_essSup 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace Top.top ENNReal instTopENNReal	lpNorm essSup Real ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder Norm.norm NormedAddCommGroup.toNorm	—	toReal_eLpNorm MemLp.aestronglyMeasurable eLpNorm_exponent_top ENNReal.toReal_essSup Measure.instOuterMeasureClass ae_le_lpNorm_exponent_top
lpNorm_exponent_zero 📖	mathematical	—	lpNorm ENNReal instZeroENNReal Real Real.instZero	—	eLpNorm_exponent_zero
lpNorm_fun_abs 📖	mathematical	AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	lpNorm Real.normedAddCommGroup abs Real.lattice Real.instAddGroup	—	lpNorm_abs
lpNorm_fun_div_natCast 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instDivInvMonoid Real.instNatCast	—	lpNorm_div_natCast
lpNorm_fun_mul_natCast 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instMul Real.instNatCast	—	lpNorm_mul_natCast
lpNorm_fun_natCast_mul 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instMul Real.instNatCast	—	lpNorm_natCast_mul
lpNorm_fun_neg 📖	mathematical	—	lpNorm NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	lpNorm_neg
lpNorm_fun_zero 📖	mathematical	—	lpNorm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instZero	—	eLpNorm_zero'
lpNorm_le_add_lpNorm_add 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Real.instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	add_neg_cancel_right lpNorm_neg lpNorm_add_le' MemLp.neg
lpNorm_le_lpNorm_add_lpNorm_sub 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Real.instAdd Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	neg_add_eq_sub sub_sub_cancel_left lpNorm_neg lpNorm_add_le MemLp.neg
lpNorm_le_lpNorm_add_lpNorm_sub' 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Real.instAdd Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	add_sub_cancel lpNorm_add_le
lpNorm_measure_zero 📖	mathematical	—	lpNorm Measure Measure.instZero Real Real.instZero	—	eLpNorm_measure_zero
lpNorm_mono_real 📖	mathematical	MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace Real.instLE Norm.norm NormedAddCommGroup.toNorm	lpNorm Real.normedAddCommGroup	—	toReal_eLpNorm MemLp.aestronglyMeasurable ENNReal.toNNReal_mono MemLp.eLpNorm_ne_top eLpNorm_mono_real lpNorm_of_not_aestronglyMeasurable
lpNorm_mul_natCast 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Pi.instNatCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instMul Real.instNatCast	—	mul_comm lpNorm_natCast_mul
lpNorm_natCast_mul 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Pi.instNatCast AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instMul Real.instNatCast	—	nsmul_eq_mul lpNorm_nsmul
lpNorm_neg 📖	mathematical	—	lpNorm Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	AEStronglyMeasurable.neg IsTopologicalAddGroup.toContinuousNeg SeminormedAddCommGroup.toIsTopologicalAddGroup eLpNorm_neg lpNorm_of_not_aestronglyMeasurable neg_neg
lpNorm_nnreal_eq_integral_norm_rpow 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lpNorm ENNReal.ofNNReal Real Real.instPow integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Norm.norm NormedAddCommGroup.toNorm NNReal.toReal Real.instInv	—	lpNorm_eq_integral_norm_rpow_toReal ne_of_gt ENNReal.coe_pos lt_of_le_of_ne' zero_le NNReal.instCanonicallyOrderedAdd
lpNorm_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero lpNorm	—	—
lpNorm_norm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lpNorm Real Real.normedAddCommGroup Norm.norm NormedAddCommGroup.toNorm	—	toReal_eLpNorm AEStronglyMeasurable.norm eLpNorm_norm
lpNorm_nsmul 📖	mathematical	—	lpNorm AddMonoid.toNatSMul Pi.addMonoid ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real Real.instAddMonoid	—	nsmul_eq_mul Nat.cast_smul_eq_nsmul Real.nnnorm_natCast NNReal.coe_natCast lpNorm_const_smul NormedSpace.toNormSMulClass
lpNorm_of_isEmpty 📖	mathematical	—	lpNorm Real Real.instZero	—	Unique.instSubsingleton lpNorm_zero
lpNorm_of_not_aestronglyMeasurable 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lpNorm Real Real.instZero	—	—
lpNorm_of_not_memLp 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	lpNorm Real Real.instZero	—	—
lpNorm_one 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instPow Measure.real Set.univ Real.instInv ENNReal.toReal	—	lpNorm_const NormOneClass.norm_one NormedDivisionRing.to_normOneClass ENNReal.toReal_rpow one_mul
lpNorm_one' 📖	mathematical	—	lpNorm NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing Real Real.instPow Measure.real Set.univ Real.instInv ENNReal.toReal	—	lpNorm_const' NormOneClass.norm_one NormedDivisionRing.to_normOneClass ENNReal.toReal_rpow one_mul
lpNorm_one_eq_integral_norm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lpNorm ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Norm.norm NormedAddCommGroup.toNorm	—	lpNorm_eq_integral_norm_rpow_toReal one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.coe_ne_top Real.rpow_one inv_one
lpNorm_smul_measure_of_ne_top 📖	mathematical	—	lpNorm NNReal Measure Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real Real.semiring NNReal.instAlgebraOfReal Real.instCommSemiring NNReal.instPowReal Real.instInv ENNReal.toReal	—	IsScalarTower.right AEStronglyMeasurable.smul_measure eLpNorm_smul_measure_of_ne_top' ENNReal.toReal_mul eq_or_ne lpNorm_exponent_zero inv_zero NNReal.rpow_zero smul_zero NNReal.zero_rpow zero_smul lpNorm_measure_zero lpNorm_of_not_aestronglyMeasurable inv_smul_smul₀
lpNorm_smul_measure_of_ne_zero 📖	mathematical	—	lpNorm NNReal Measure Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Real Real.semiring NNReal.instAlgebraOfReal Real.instCommSemiring NNReal.instPowReal Real.instInv ENNReal.toReal	—	IsScalarTower.right AEStronglyMeasurable.smul_measure eLpNorm_smul_measure_of_ne_zero' ENNReal.toReal_mul lpNorm_of_not_aestronglyMeasurable inv_smul_smul₀ smul_zero
lpNorm_sub_comm 📖	mathematical	—	lpNorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	lpNorm_neg neg_sub
lpNorm_sub_le 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instAdd	—	sub_eq_add_neg lpNorm_neg lpNorm_add_le
lpNorm_sub_le_lpNorm_sub_add_lpNorm_sub 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instAdd	—	sub_add_sub_cancel lpNorm_add_le MemLp.sub
lpNorm_sum_le 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Real Real.instLE lpNorm Finset.sum Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instAddCommMonoid	—	Finset.sum_congr toReal_eLpNorm MemLp.aestronglyMeasurable ENNReal.toReal_sum LT.lt.ne Finset.aestronglyMeasurable_sum IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup le_imp_le_of_le_of_le ENNReal.toReal_mono eLpNorm_sum_le le_refl
lpNorm_zero 📖	mathematical	—	lpNorm Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instZero	—	eLpNorm_zero
ofReal_lpNorm 📖	mathematical	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	ENNReal.ofReal lpNorm eLpNorm	—	toReal_eLpNorm MemLp.aestronglyMeasurable ENNReal.ofReal_toReal MemLp.eLpNorm_ne_top
toReal_eLpNorm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	ENNReal.toReal eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm lpNorm	—	lpNorm.eq_1

---

← Back to Index