L2Space

📁 Source: Mathlib/MeasureTheory/Function/L2Space.lean

Statistics

Metric	Count
Definitions innerProductSpace, instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal	2
Theorems inner_toLp, inner_toLp, const_inner, inner_const, eLpNorm_inner_lt_top, eLpNorm_rpow_two_norm_lt_top, inner_def, inner_indicatorConstLp_eq_inner_setIntegral, inner_indicatorConstLp_eq_setIntegral_inner, inner_indicatorConstLp_indicatorConstLp, inner_indicatorConstLp_one, inner_indicatorConstLp_one_indicatorConstLp_one, integrable_inner, integral_inner_eq_sq_eLpNorm, mem_L1_inner, real_inner_indicatorConstLp_one_indicatorConstLp_one, const_inner, inner_const, integrable_sq, memLp_two_iff_integrable_sq, memLp_two_iff_integrable_sq_norm, integral_eq_zero_of_forall_integral_inner_eq_zero, integral_inner	23
Total	25

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
memLp_two_iff_integrable_sq 📖	mathematical	AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Integrable Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat sq_abs memLp_two_iff_integrable_sq_norm
memLp_two_iff_integrable_sq_norm 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Integrable Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	Nat.instAtLeastTwoHAddOfNat memLp_one_iff_integrable ENNReal.toReal_ofNat Real.rpow_ofNat div_eq_mul_inv ENNReal.mul_inv_cancel two_ne_zero CharZero.NeZero.two ENNReal.instCharZero ENNReal.ofNat_ne_top memLp_norm_rpow_iff

MeasureTheory.BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_toLp 📖	mathematical	—	Inner.inner MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal RCLike.innerProductSpace DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing RingHom.id Semiring.toNonAssocSemiring BoundedContinuousFunction BoundedContinuousFunction.instPseudoMetricSpace BoundedContinuousFunction.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instBoundedAddOfLipschitzAdd AddCommMonoid.toAddMonoid SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal BoundedContinuousFunction.instModule SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace NormedSpace.toIsBoundedSMul MeasureTheory.Lp.instModule ContinuousLinearMap.funLike BoundedContinuousFunction.toLp secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable SeminormedCommRing.toSeminormedRing EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real Real Real.instRCLike RCLike.toInnerProductSpaceReal FiniteDimensional.rclike_to_real MeasureTheory.integral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing BoundedContinuousFunction.instFunLike RingHom CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd RCLike.toStarRing	—	MeasureTheory.integral_congr_ae instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal NormedSpace.toIsBoundedSMul secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real MeasureTheory.Measure.instOuterMeasureClass BoundedContinuousFunction.coeFn_toLp Filter.mp_mem Filter.univ_mem'

MeasureTheory.ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_toLp 📖	mathematical	—	Inner.inner MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal RCLike.innerProductSpace DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing RingHom.id Semiring.toNonAssocSemiring ContinuousMap ContinuousMap.compactOpen ContinuousMap.instAddCommMonoidOfContinuousAdd ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_two_ennreal ContinuousMap.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul MeasureTheory.Lp.instModule ContinuousLinearMap.funLike ContinuousMap.toLp secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable SeminormedCommRing.toSeminormedRing EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real Real Real.instRCLike RCLike.toInnerProductSpaceReal FiniteDimensional.rclike_to_real MeasureTheory.integral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousMap.instFunLike RingHom CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.instFunLike starRingEnd RCLike.toStarRing	—	MeasureTheory.integral_congr_ae IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real FiniteDimensional.rclike_to_real MeasureTheory.Measure.instOuterMeasureClass ContinuousMap.coeFn_toLp Filter.mp_mem Filter.univ_mem'

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_inner 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Inner.inner InnerProductSpace.toInner	—	MeasureTheory.memLp_one_iff_integrable MeasureTheory.MemLp.const_inner
inner_const 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Inner.inner InnerProductSpace.toInner	—	MeasureTheory.memLp_one_iff_integrable MeasureTheory.MemLp.inner_const

MeasureTheory.L2

Definitions

Name	Category	Theorems
innerProductSpace 📖	CompOp	6 math math: UnitAddTorus.coe_mFourierBasis, orthonormal_fourier, UnitAddTorus.orthonormal_mFourier, coe_fourierBasis, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr
instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal 📖	CompOp	15 math math: SchwartzMap.inner_fourier_toL2_eq, inner_indicatorConstLp_eq_inner_setIntegral, MeasureTheory.inner_condExpL2_left_eq_right, inner_def, SchwartzMap.inner_toL2_toL2_eq, inner_indicatorConstLp_one, inner_indicatorConstLp_indicatorConstLp, real_inner_indicatorConstLp_one_indicatorConstLp_one, inner_indicatorConstLp_eq_setIntegral_inner, SchwartzMap.inner_fourierTransformCLM_toL2_eq, inner_indicatorConstLp_one_indicatorConstLp_one, MeasureTheory.Lp.inner_fourier_eq, MeasureTheory.inner_condExpL2_eq_inner_fun, MeasureTheory.BoundedContinuousFunction.inner_toLp, MeasureTheory.ContinuousMap.inner_toLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eLpNorm_inner_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddGroup.toContinuousENorm Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat AddMonoidWithOne.toOne Top.top instTopENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat Nat.cast_two Real.rpow_natCast norm_inner_le_norm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_mul_of_one_le_left norm_nonneg one_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LE.le.trans two_mul_le_add_sq AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le le_abs_self LE.le.trans_lt MeasureTheory.eLpNorm_mono_ae MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.eLpNorm_add_le AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal AEMeasurable.pow_const Real.hasMeasurablePow MeasureTheory.AEStronglyMeasurable.aemeasurable MeasureTheory.AEStronglyMeasurable.norm MeasureTheory.Lp.aestronglyMeasurable le_rfl ENNReal.add_lt_top eLpNorm_rpow_two_norm_lt_top
eLpNorm_rpow_two_norm_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.instPow Norm.norm NormedAddCommGroup.toNorm MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Real.instNatCast AddMonoidWithOne.toOne Top.top instTopENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat ENNReal.ofReal_ofNat MeasureTheory.eLpNorm_norm_rpow zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid one_mul ENNReal.rpow_lt_top_of_nonneg zero_le_two MeasureTheory.Lp.eLpNorm_ne_top
inner_def 📖	mathematical	—	Inner.inner 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 ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike RCLike.toInnerProductSpaceReal InnerProductSpace.toInner MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat
inner_indicatorConstLp_eq_inner_setIntegral 📖	mathematical	MeasurableSet	Inner.inner 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 ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal MeasureTheory.indicatorConstLp InnerProductSpace.toInner MeasureTheory.integral MeasureTheory.Measure.restrict MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat integral_inner MeasureTheory.integrableOn_Lp_of_measure_ne_top Fact.elim fact_one_le_two_ennreal inner_indicatorConstLp_eq_setIntegral_inner
inner_indicatorConstLp_eq_setIntegral_inner 📖	mathematical	MeasurableSet	Inner.inner 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 ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal MeasureTheory.indicatorConstLp MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict InnerProductSpace.toInner MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat inner_def MeasureTheory.integral_add_compl integrable_inner MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.indicatorConstLp_coeFn_mem Filter.Eventually.mono MeasureTheory.setIntegral_congr_ae MeasureTheory.indicatorConstLp_coeFn_notMem inner_zero_left MeasurableSet.compl MeasureTheory.integral_zero add_zero
inner_indicatorConstLp_indicatorConstLp 📖	mathematical	MeasurableSet ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Top.top instTopENNReal	Inner.inner 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal MeasureTheory.indicatorConstLp Real Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra MeasureTheory.Measure.real Set.instInter InnerProductSpace.toInner	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat inner_indicatorConstLp_eq_inner_setIntegral MeasureTheory.setIntegral_indicatorConstLp inner_smul_right_eq_smul Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace RCLike.instStarModuleReal Set.inter_comm
inner_indicatorConstLp_one 📖	mathematical	MeasurableSet	Inner.inner MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal RCLike.innerProductSpace MeasureTheory.indicatorConstLp AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing MeasureTheory.integral InnerProductSpace.toNormedSpace Real Real.instRCLike RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict MeasureTheory.AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat inner_indicatorConstLp_eq_inner_setIntegral RCLike.toCompleteSpace map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one
inner_indicatorConstLp_one_indicatorConstLp_one 📖	mathematical	MeasurableSet ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Top.top instTopENNReal	Inner.inner MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal RCLike.innerProductSpace MeasureTheory.indicatorConstLp AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing RCLike.ofReal MeasureTheory.Measure.real Set.instInter	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat inner_indicatorConstLp_indicatorConstLp RCLike.toCompleteSpace inner_self_eq_norm_sq_to_K CStarRing.norm_of_mem_unitary RCLike.instCStarRing IsLocalRing.toNontrivial Field.instIsLocalRing SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass RCLike.ofReal_alg one_smul one_pow
integrable_inner 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun.cast SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat MeasureTheory.AEStronglyMeasurable.inner MeasureTheory.Lp.aestronglyMeasurable MeasureTheory.integrable_congr MeasureTheory.AEEqFun.integrable_iff_mem_L1 mem_L1_inner
integral_inner_eq_sq_eLpNorm 📖	mathematical	—	MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat RCLike.ofReal ENNReal.toReal MeasureTheory.lintegral ENNReal.instPowReal ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Real.instNatCast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat inner_self_eq_norm_sq_to_K integral_ofReal ENNReal.rpow_natCast Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing MeasureTheory.integral_eq_lintegral_of_nonneg_ae Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal AEMeasurable.pow_const Monoid.measurablePow ContinuousMul.measurableMul₂ IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.AEStronglyMeasurable.aemeasurable MeasureTheory.AEStronglyMeasurable.norm MeasureTheory.Lp.aestronglyMeasurable Real.rpow_natCast ENNReal.ofReal_rpow_of_nonneg norm_nonneg zero_le_two Real.instZeroLEOneClass ofReal_norm_eq_enorm
mem_L1_inner 📖	mathematical	—	MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSubgroup SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Inner.inner InnerProductSpace.toInner MeasureTheory.AEEqFun.cast instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.AEStronglyMeasurable.inner MeasureTheory.Lp.aestronglyMeasurable	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat MeasureTheory.AEStronglyMeasurable.inner MeasureTheory.Lp.aestronglyMeasurable MeasureTheory.eLpNorm_aeeqFun eLpNorm_inner_lt_top
real_inner_indicatorConstLp_one_indicatorConstLp_one 📖	mathematical	MeasurableSet ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Top.top instTopENNReal	Inner.inner Real MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal Real.instRCLike RCLike.toInnerProductSpaceReal MeasureTheory.indicatorConstLp Real.instOne MeasureTheory.Measure.real Set.instInter	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat inner_indicatorConstLp_indicatorConstLp Real.instCompleteSpace inner_self_eq_norm_sq_to_K CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass one_pow mul_one

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_inner 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner	—	of_le_mul MeasureTheory.AEStronglyMeasurable.inner MeasureTheory.aestronglyMeasurable_const Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass norm_inner_le_norm
inner_const 📖	mathematical	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner	—	of_le_mul MeasureTheory.AEStronglyMeasurable.inner MeasureTheory.aestronglyMeasurable_const Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass mul_comm norm_inner_le_norm
integrable_sq 📖	mathematical	MeasureTheory.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 ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	MeasureTheory.Integrable Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat ENNReal.toReal_ofNat Real.rpow_ofNat sq_abs norm_rpow two_ne_zero CharZero.NeZero.two ENNReal.instCharZero ENNReal.ofNat_ne_top

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_eq_zero_of_forall_integral_inner_eq_zero 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	inner_self_eq_zero integral_inner
integral_inner 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.integral NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	ContinuousLinearMap.integral_comp_comm RCLike.toCompleteSpace LinearMap.IsScalarTower.compatibleSMul Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsScalarTower.right SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul

---

← Back to Index