TorusIntegral

📁 Source: Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Statistics

Metric	Count
Definitions TorusIntegrable, torusIntegral, torusMap, «term∯_InT(_,_),_»,_»)	4
Theorems add, function_integrable, neg, sub, torusIntegrable_const, torusIntegrable_zero_radius, norm_torusIntegral_le_of_norm_le_const, torusIntegral_add, torusIntegral_const_mul, torusIntegral_dim0, torusIntegral_dim1, torusIntegral_neg, torusIntegral_radius_zero, torusIntegral_smul, torusIntegral_sub, torusIntegral_succ, torusIntegral_succAbove, torusMap_eq_center_iff, torusMap_sub_center, torusMap_zero_radius	20
Total	24

TorusIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	TorusIntegrable	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	MeasureTheory.Integrable.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
function_integrable 📖	mathematical	TorusIntegrable	MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Fin.fintype Real Real.measureSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Finset.prod CommRing.toCommMonoid Complex.commRing Finset.univ Complex.instMul Complex.ofReal Complex.exp Complex.I torusMap Set.Icc Pi.preorder Real.instPreorder Pi.instZero Real.instZero Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Integrable.mono' MeasureTheory.Integrable.const_mul MeasureTheory.Integrable.norm MeasureTheory.AEStronglyMeasurable.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.aestronglyMeasurable Pi.opensMeasurableSpace instCountableFin instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right secondCountable_of_proper Complex.instProperSpace continuous_finset_prod IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.comp' Continuous.fun_mul continuous_id' continuous_const Continuous.cexp Complex.continuous_ofReal continuous_apply MeasureTheory.Measure.instOuterMeasureClass norm_smul NormedSpace.toNormSMulClass norm_prod NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Finset.prod_congr Complex.norm_mul Complex.norm_real Complex.norm_exp_ofReal_mul_I mul_one Complex.norm_I MeasureTheory.ae_restrict_eq Pi.orderClosedTopology' HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
neg 📖	mathematical	TorusIntegrable	Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	MeasureTheory.Integrable.neg
sub 📖	mathematical	TorusIntegrable	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	MeasureTheory.Integrable.sub
torusIntegrable_const 📖	mathematical	—	TorusIntegrable	—	Pi.compact_Icc_space' ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Real.locallyFinite_volume
torusIntegrable_zero_radius 📖	mathematical	—	TorusIntegrable Pi.instZero Real Real.instZero	—	eq_1 torusMap_zero_radius torusIntegrable_const

(root)

Definitions

Name	Category	Theorems
TorusIntegrable 📖	MathDef	2 math math: TorusIntegrable.torusIntegrable_zero_radius, TorusIntegrable.torusIntegrable_const
torusIntegral 📖	CompOp	11 math math: norm_torusIntegral_le_of_norm_le_const, torusIntegral_add, torusIntegral_succ, torusIntegral_neg, torusIntegral_const_mul, torusIntegral_dim1, torusIntegral_radius_zero, torusIntegral_smul, torusIntegral_dim0, torusIntegral_sub, torusIntegral_succAbove
torusMap 📖	CompOp	4 math math: torusMap_zero_radius, torusMap_eq_center_iff, TorusIntegrable.function_integrable, torusMap_sub_center
«term∯_InT(_,_),_» 📖,_» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_torusIntegral_le_of_norm_le_const 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm torusMap	torusIntegral Real.instMul Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Finset.prod Real.instCommMonoid Finset.univ Fin.fintype abs Real.lattice Real.instAddGroup	—	Nat.instAtLeastTwoHAddOfNat MeasureTheory.norm_setIntegral_le_of_norm_le_const measure_Icc_lt_top Pi.compact_Icc_space' ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Real.locallyFinite_volume norm_smul NormedSpace.toNormSMulClass norm_prod NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Finset.prod_congr Complex.norm_mul Complex.norm_real Complex.norm_exp_ofReal_mul_I mul_one Complex.norm_I mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing Finset.prod_nonneg Real.instZeroLEOneClass abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.volume_Icc_pi_toReal LT.lt.le Real.two_pi_pos sub_zero Fin.prod_const mul_assoc mul_comm
torusIntegral_add 📖	mathematical	TorusIntegrable	torusIntegral AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	smul_add MeasureTheory.integral_add Nat.instAtLeastTwoHAddOfNat TorusIntegrable.function_integrable
torusIntegral_const_mul 📖	mathematical	—	torusIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instMul	—	torusIntegral_smul Algebra.to_smulCommClass
torusIntegral_dim0 📖	mathematical	—	torusIntegral	—	IsScalarTower.right Fin.isEmpty' MeasureTheory.Measure.pi_of_empty Unique.instSubsingleton Nat.instAtLeastTwoHAddOfNat Set.Icc_self MeasureTheory.Measure.restrict_singleton MeasureTheory.Measure.dirac_apply_of_mem Set.mem_singleton one_smul MeasureTheory.integral_dirac Pi.instMeasurableSingletonClass instCountableFin instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
torusIntegral_dim1 📖	mathematical	—	torusIntegral circleIntegral	—	Nat.instAtLeastTwoHAddOfNat OrderIso.preimage_Icc torusIntegral.eq_1 circleIntegral.eq_1 intervalIntegral.integral_of_le LT.lt.le Real.two_pi_pos MeasureTheory.Measure.restrict_congr_set MeasureTheory.Ioc_ae_eq_Icc Real.noAtoms_volume MeasureTheory.MeasurePreserving.setIntegral_preimage_emb MeasureTheory.MeasurePreserving.symm MeasureTheory.volume_preserving_funUnique MeasurableEquiv.measurableEmbedding Finset.prod_congr Finset.univ_unique Finset.prod_singleton deriv_circleMap circleMap_zero
torusIntegral_neg 📖	mathematical	—	torusIntegral NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	smul_neg MeasureTheory.integral_neg
torusIntegral_radius_zero 📖	mathematical	—	torusIntegral Pi.instZero Real Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Finset.prod_congr MulZeroClass.zero_mul Fin.prod_const zero_pow zero_smul MeasureTheory.integral_zero
torusIntegral_smul 📖	mathematical	—	torusIntegral 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 DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	SMulCommClass.smul_comm MeasureTheory.integral_smul NormedSpace.toNormSMulClass IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
torusIntegral_sub 📖	mathematical	TorusIntegrable	torusIntegral SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub_eq_add_neg torusIntegral_add TorusIntegrable.neg
torusIntegral_succ 📖	mathematical	TorusIntegrable	torusIntegral circleIntegral Fin.cons Complex Real	—	Fin.insertNth_zero' torusIntegral_succAbove
torusIntegral_succAbove 📖	mathematical	TorusIntegrable	torusIntegral circleIntegral Fin.insertNth Complex Fin.succAbove Real	—	MeasureTheory.MeasurePreserving.symm MeasureTheory.volume_preserving_piFinSuccAbove MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Nat.instAtLeastTwoHAddOfNat OrderIso.preimage_Icc Set.Icc_prod_eq torusIntegral.eq_1 MeasureTheory.MeasurePreserving.map_eq MeasureTheory.setIntegral_map_equiv MeasureTheory.Measure.volume_eq_prod MeasureTheory.setIntegral_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.instSigmaFiniteForallVolume TorusIntegrable.function_integrable MeasureTheory.MeasurePreserving.integrableOn_comp_preimage MeasurableEquiv.measurableEmbedding circleIntegral_def_Icc MeasureTheory.setIntegral_congr_fun measurableSet_Icc BorelSpace.opensMeasurable HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Finset.prod_congr Fin.prod_univ_succAbove deriv_circleMap circleMap_zero NormedSpace.toNormSMulClass SMulCommClass.complexToReal smulCommClass_self smul_smul Pi.opensMeasurableSpace instCountableFin Pi.orderClosedTopology' Fin.insertNth_apply_same Fin.insertNth_apply_succAbove Fin.forall_iff_succAbove
torusMap_eq_center_iff 📖	mathematical	—	torusMap Pi.instZero Real Real.instZero	—	AddLeftCancelSemigroup.toIsLeftCancelAdd NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
torusMap_sub_center 📖	mathematical	—	Pi.instSub Complex Complex.instSub torusMap Pi.instZero Complex.instZero	—	add_sub_cancel_left zero_add
torusMap_zero_radius 📖	mathematical	—	torusMap Pi.instZero Real Real.instZero	—	torusMap_eq_center_iff

---

← Back to Index