Complex

📁 Source: Mathlib/MeasureTheory/Constructions/BorelSpace/Complex.lean

Statistics

Metric	Count
Definitions measurableSpace, measurableSpace	2
Theorems borelSpace, borelSpace	2
Total	4

Complex

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	67 math math: NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, Measurable.complex_ofReal, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, integral_comp_pi_polarCoord_symm, measurable_arg, borelSpace, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume, NumberField.mixedEmbedding.convexBodyLT_volume, integral_rpow_mul_exp_neg_rpow, volume_sum_rpow_le, measurableEquivPi_apply, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, integral_comp_polarCoord_symm, NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero, measurableEquivRealProd_apply, measurable_circleMap, integral_exp_neg_rpow, measurable_re, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, NumberField.mixedEmbedding.covolume_idealLattice, NumberField.mixedEmbedding.volume_preserving_negAt, measurable_cos, NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm, integral_exp_neg_mul_rpow, volume_sum_rpow_lt, lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, measurable_im, NumberField.mixedEmbedding.measurableSet_fundamentalCone, measurable_exp, measurableEquivRealProd_symm_polarCoord_symm_apply, volume_preserving_equiv_real_prod, NumberField.mixedEmbedding.covolume_integerLattice, volume_closedBall, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.convexBodyLT'_volume, measurableEquivPi_symm_apply, measurable_sinh, volume_preserving_equiv_pi, AEMeasurable.complex_ofReal, NumberField.mixedEmbedding.volume_eq_zero, NumberField.mixedEmbedding.measurable_polarCoord_symm, measurable_sin, measurable_log, integral_rpow_mul_exp_neg_mul_rpow, measurable_cosh, volume_ball, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, lintegral_comp_pi_polarCoord_symm, volume_sum_rpow_lt_one, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne, measurable_ofReal, hasMeasurablePow, NumberField.mixedEmbedding.convexBodySum_volume, measurableEquivRealProd_symm_apply, MeasureTheory.measurable_charFun, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne, NumberField.mixedEmbedding.measurable_polarSpaceCoord_symm, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField measurableSpace	—	—

RCLike

Definitions

Name	Category	Theorems
measurableSpace 📖	CompOp	12 math math: measurable_ofReal, aemeasurable_of_re_im, Measurable.inner, borelSpace, AEMeasurable.const_inner, measurable_re, AEMeasurable.inner, Measurable.const_inner, AEMeasurable.inner_const, measurable_of_re_im, measurable_im, Measurable.inner_const

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borelSpace 📖	mathematical	—	BorelSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField measurableSpace	—	—

---

← Back to Index