PolarCoord

📁 Source: Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Statistics

Metric	Count
Definitions polarCoord, fderivPiPolarCoordSymm, fderivPolarCoordSymm, polarCoord	4
Theorems integral_comp_pi_polarCoord_symm, integral_comp_polarCoord_symm, lintegral_comp_pi_polarCoord_symm, lintegral_comp_polarCoord_symm, measurableEquivRealProd_symm_polarCoord_symm_apply, norm_polarCoord_symm, polarCoord_apply, polarCoord_source, polarCoord_symm_apply, polarCoord_target, abs_fst_of_mem_pi_polarCoord_target, continuous_polarCoord_symm, det_fderivPiPolarCoordSymm, det_fderivPolarCoordSymm, hasFDerivAt_pi_polarCoord_symm, hasFDerivAt_polarCoord_symm, injOn_pi_polarCoord_symm, instIsAddHaarMeasureProdRealVolume, integral_comp_pi_polarCoord_symm, integral_comp_polarCoord_symm, lintegral_comp_pi_polarCoord_symm, lintegral_comp_polarCoord_symm, measurableSet_pi_polarCoord_target, pi_polarCoord_symm_target_ae_eq_univ, polarCoord_apply, polarCoord_source, polarCoord_source_ae_eq_univ, polarCoord_symm_apply, polarCoord_target	29
Total	33

Complex

Definitions

Name	Category	Theorems
polarCoord 📖	CompOp	18 math math: norm_polarCoord_symm, integral_comp_pi_polarCoord_symm, NumberField.mixedEmbedding.polarSpaceCoord_target, integral_comp_polarCoord_symm, polarCoord_apply, NumberField.mixedEmbedding.polarCoord_symm_apply, lintegral_comp_polarCoord_symm, NumberField.mixedEmbedding.polarCoord_source, NumberField.mixedEmbedding.polarSpaceCoord_symm_apply, measurableEquivRealProd_symm_polarCoord_symm_apply, NumberField.mixedEmbedding.polarCoord_target, polarCoord_source, NumberField.mixedEmbedding.polarCoord_apply, NumberField.mixedEmbedding.polarSpaceCoord_apply, NumberField.mixedEmbedding.polarSpaceCoord_source, lintegral_comp_pi_polarCoord_symm, polarCoord_symm_apply, polarCoord_target

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_comp_pi_polarCoord_symm 📖	mathematical	—	MeasureTheory.integral MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.pi Set.univ PartialEquiv.target Complex OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instTopologicalSpaceProd Real.pseudoMetricSpace polarCoord SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Finset.prod Real.instCommMonoid Finset.univ OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm measureSpaceOfInnerProductSpace instNormedAddCommGroup instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real instRCLike measurableSpace borelSpace	—	FiniteDimensional.rclike_to_real borelSpace MeasureTheory.volume_preserving_pi MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper instProperSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper MeasureTheory.MeasurePreserving.symm volume_preserving_equiv_real_prod MeasureTheory.MeasurePreserving.integral_comp MeasurableEquiv.measurableEmbedding integral_comp_pi_polarCoord_symm
integral_comp_polarCoord_symm 📖	mathematical	—	MeasureTheory.integral Real MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField OpenPartialHomeomorph.toFun' Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField OpenPartialHomeomorph.symm polarCoord measureSpaceOfInnerProductSpace instNormedAddCommGroup instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real instRCLike measurableSpace borelSpace	—	FiniteDimensional.rclike_to_real borelSpace MeasureTheory.MeasurePreserving.integral_comp MeasureTheory.MeasurePreserving.symm volume_preserving_equiv_real_prod MeasurableEquiv.measurableEmbedding integral_comp_polarCoord_symm
lintegral_comp_pi_polarCoord_symm 📖	mathematical	—	MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.pi Set.univ PartialEquiv.target Complex OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instTopologicalSpaceProd Real.pseudoMetricSpace polarCoord ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Finset.prod CommSemiring.toCommMonoid Finset.univ ENNReal.ofReal OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm measureSpaceOfInnerProductSpace instNormedAddCommGroup instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real instRCLike measurableSpace borelSpace	—	FiniteDimensional.rclike_to_real borelSpace MeasureTheory.volume_preserving_pi MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper instProperSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper MeasureTheory.MeasurePreserving.symm volume_preserving_equiv_real_prod MeasureTheory.MeasurePreserving.lintegral_comp_emb MeasurableEquiv.measurableEmbedding lintegral_comp_pi_polarCoord_symm
lintegral_comp_polarCoord_symm 📖	mathematical	—	MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord ENNReal Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id ENNReal.ofReal OpenPartialHomeomorph.toFun' Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField OpenPartialHomeomorph.symm polarCoord measureSpaceOfInnerProductSpace instNormedAddCommGroup instInnerProductSpaceRealComplex FiniteDimensional.rclike_to_real instRCLike measurableSpace borelSpace	—	FiniteDimensional.rclike_to_real borelSpace MeasureTheory.MeasurePreserving.lintegral_comp_emb MeasureTheory.MeasurePreserving.symm volume_preserving_equiv_real_prod MeasurableEquiv.measurableEmbedding lintegral_comp_polarCoord_symm
measurableEquivRealProd_symm_polarCoord_symm_apply 📖	mathematical	—	DFunLike.coe MeasurableEquiv Real Complex Prod.instMeasurableSpace Real.measurableSpace measurableSpace EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm measurableEquivRealProd OpenPartialHomeomorph.toFun' instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm polarCoord SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField polarCoord	—	—
norm_polarCoord_symm 📖	mathematical	—	Norm.norm Complex instNorm OpenPartialHomeomorph.toFun' Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField OpenPartialHomeomorph.symm polarCoord abs Real.lattice Real.instAddGroup	—	polarCoord_symm_apply ofReal_cos ofReal_sin norm_mul norm_real norm_cos_add_sin_mul_I mul_one
polarCoord_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Complex Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instTopologicalSpaceProd Real.pseudoMetricSpace polarCoord Norm.norm instNorm arg	—	—
polarCoord_source 📖	mathematical	—	PartialEquiv.source Complex Real OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instTopologicalSpaceProd Real.pseudoMetricSpace polarCoord slitPlane	—	—
polarCoord_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real Complex instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField OpenPartialHomeomorph.symm polarCoord instMul ofReal instAdd Real.cos Real.sin I	—	RingHomInvPair.ids equivRealProdCLM_symm_apply ofReal_mul ofReal_cos ofReal_sin mul_assoc mul_add Distrib.leftDistribClass
polarCoord_target 📖	mathematical	—	PartialEquiv.target Complex Real OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instTopologicalSpaceProd Real.pseudoMetricSpace polarCoord SProd.sprod Set Set.instSProd Set.Ioi Real.instPreorder Real.instZero Set.Ioo Real.instNeg Real.pi	—	—

(root)

Definitions

Name	Category	Theorems
fderivPiPolarCoordSymm 📖	CompOp	2 math math: det_fderivPiPolarCoordSymm, hasFDerivAt_pi_polarCoord_symm
fderivPolarCoordSymm 📖	CompOp	2 math math: det_fderivPolarCoordSymm, hasFDerivAt_polarCoord_symm
polarCoord 📖	CompOp	20 math math: NumberField.mixedEmbedding.polarCoordReal_apply, Complex.integral_comp_polarCoord_symm, lintegral_comp_pi_polarCoord_symm, polarCoord_target, continuous_polarCoord_symm, NumberField.mixedEmbedding.polarCoordReal_source, measurableSet_pi_polarCoord_target, integral_comp_polarCoord_symm, polarCoord_symm_apply, Complex.lintegral_comp_polarCoord_symm, Complex.measurableEquivRealProd_symm_polarCoord_symm_apply, hasFDerivAt_polarCoord_symm, injOn_pi_polarCoord_symm, hasFDerivAt_pi_polarCoord_symm, lintegral_comp_polarCoord_symm, polarCoord_apply, polarCoord_source_ae_eq_univ, pi_polarCoord_symm_target_ae_eq_univ, integral_comp_pi_polarCoord_symm, polarCoord_source

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_fst_of_mem_pi_polarCoord_target 📖	mathematical	Set Set.instMembership Set.pi Real Set.univ PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord	abs Real.lattice Real.instAddGroup	—	abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.mem_univ_pi
continuous_polarCoord_symm 📖	mathematical	—	Continuous Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm polarCoord	—	Continuous.prodMk Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fst continuous_id' Real.continuous_cos Continuous.snd Real.continuous_sin
det_fderivPiPolarCoordSymm 📖	mathematical	—	ContinuousLinearMap.det Real Real.commRing Pi.topologicalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.addCommGroup Prod.instAddCommGroup Real.instAddCommGroup Pi.Function.module Real.semiring Prod.instAddCommMonoid Real.instAddCommMonoid Prod.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal fderivPiPolarCoordSymm Finset.prod Real.instCommMonoid Finset.univ	—	ContinuousLinearMap.det_pi Module.Free.prod Module.Free.self Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.rclike_to_real Module.Projective.of_free Finset.prod_congr det_fderivPolarCoordSymm
det_fderivPolarCoordSymm 📖	mathematical	—	ContinuousLinearMap.det Real Real.commRing instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Prod.instAddCommGroup Real.instAddCommGroup Prod.instModule Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal fderivPolarCoordSymm	—	one_mul Real.cos_sq_add_sin_sq Real.instCompleteSpace neg_mul RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.det_toLin Matrix.det_fin_two_of sub_neg_eq_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero
hasFDerivAt_pi_polarCoord_symm 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Pi.addCommGroup Prod.instAddCommGroup Real.instAddCommGroup Pi.Function.module Real.semiring Prod.instAddCommMonoid Real.instAddCommMonoid Prod.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Pi.topologicalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm polarCoord fderivPiPolarCoordSymm	—	fderivPiPolarCoordSymm.eq_1 hasFDerivAt_pi HasFDerivAt.comp hasFDerivAt_polarCoord_symm hasFDerivAt_apply
hasFDerivAt_polarCoord_symm 📖	mathematical	—	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.instAddCommGroup Real.instAddCommGroup Prod.instModule Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm polarCoord fderivPolarCoordSymm	—	Real.instCompleteSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd Prod.instIsTopologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self ContinuousSMul.continuousConstSMul Prod.continuousSMul IsModuleTopology.toContinuousSMul isModuleTopologyOfFiniteDimensional IsTopologicalSemiring.toIsModuleTopology TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace FiniteDimensional.finiteDimensional_self Prod.t2Space Module.IsNoetherian.finite isNoetherian_prod IsSimpleModule.instIsNoetherian instIsSimpleModule Finite.of_fintype Matrix.toLin_finTwoProd_toContinuousLinearMap NonUnitalSeminormedRing.toIsTopologicalRing instIsTopologicalAddGroupReal instIsUniformAddGroupReal instIsTopologicalRingReal RingHomIsometric.ids neg_mul neg_smul smul_neg smul_smul add_comm HasFDerivAt.prodMk HasFDerivAt.mul hasFDerivAt_fst HasDerivAt.comp_hasFDerivAt Real.hasDerivAt_cos hasFDerivAt_snd Real.hasDerivAt_sin
injOn_pi_polarCoord_symm 📖	mathematical	—	Set.InjOn OpenPartialHomeomorph.toFun' Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm polarCoord Set.pi Set.univ PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	OpenPartialHomeomorph.injOn
instIsAddHaarMeasureProdRealVolume 📖	mathematical	—	MeasureTheory.Measure.IsAddHaarMeasure Real Prod.instAddGroup Real.instAddGroup instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.prod.instIsAddHaarMeasure instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal ContinuousAdd.measurableAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
integral_comp_pi_polarCoord_symm 📖	mathematical	—	MeasureTheory.integral MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.pi Set.univ PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Finset.prod Real.instCommMonoid Finset.univ OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	MeasureTheory.setIntegral_univ MeasureTheory.setIntegral_congr_set pi_polarCoord_symm_target_ae_eq_univ MeasureTheory.setIntegral_congr_fun measurableSet_pi_polarCoord_target Finite.of_fintype det_fderivPiPolarCoordSymm Finset.abs_prod Real.instIsStrictOrderedRing Finset.prod_congr abs_fst_of_mem_pi_polarCoord_target MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul FiniteDimensional.finiteDimensional_pi' Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.rclike_to_real Module.Projective.of_free Module.Free.self Pi.borelSpace Finite.to_countable TopologicalSpace.instSecondCountableTopologyProd instSecondCountableTopologyReal Prod.borelSpace Real.borelSpace secondCountableTopologyEither_of_right MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd Prod.continuousAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.instSigmaFiniteProdVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal instIsAddHaarMeasureProdRealVolume HasFDerivAt.hasFDerivWithinAt hasFDerivAt_pi_polarCoord_symm injOn_pi_polarCoord_symm
integral_comp_polarCoord_symm 📖	mathematical	—	MeasureTheory.integral Real MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	MeasureTheory.setIntegral_univ MeasureTheory.setIntegral_congr_set Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass polarCoord_source_ae_eq_univ OpenPartialHomeomorph.symm_target MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.rclike_to_real Module.Projective.of_free Module.Free.self Prod.borelSpace Real.borelSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal instIsAddHaarMeasureProdRealVolume hasFDerivAt_polarCoord_symm OpenPartialHomeomorph.symm_source det_fderivPolarCoordSymm MeasureTheory.setIntegral_congr_fun IsOpen.measurableSet Prod.opensMeasurableSpace BorelSpace.opensMeasurable OpenPartialHomeomorph.open_target abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
lintegral_comp_pi_polarCoord_symm 📖	mathematical	—	MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.pi Set.univ PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Finset.prod CommSemiring.toCommMonoid Finset.univ ENNReal.ofReal OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	MeasureTheory.setLIntegral_univ MeasureTheory.setLIntegral_congr pi_polarCoord_symm_target_ae_eq_univ MeasureTheory.setLIntegral_congr_fun measurableSet_pi_polarCoord_target Finite.of_fintype det_fderivPiPolarCoordSymm Finset.abs_prod Real.instIsStrictOrderedRing ENNReal.ofReal_prod_of_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.prod_congr abs_fst_of_mem_pi_polarCoord_target MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul FiniteDimensional.finiteDimensional_pi' Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.rclike_to_real Module.Projective.of_free Module.Free.self Pi.borelSpace Finite.to_countable TopologicalSpace.instSecondCountableTopologyProd instSecondCountableTopologyReal Prod.borelSpace Real.borelSpace secondCountableTopologyEither_of_right MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite ContinuousAdd.measurableAdd Prod.continuousAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Measure.instSigmaFiniteProdVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal instIsAddHaarMeasureProdRealVolume HasFDerivAt.hasFDerivWithinAt hasFDerivAt_pi_polarCoord_symm injOn_pi_polarCoord_symm
lintegral_comp_polarCoord_symm 📖	mathematical	—	MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord ENNReal Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id ENNReal.ofReal OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	MeasureTheory.setLIntegral_univ MeasureTheory.setLIntegral_congr Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass polarCoord_source_ae_eq_univ OpenPartialHomeomorph.symm_image_target_eq_source MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.rclike_to_real Module.Projective.of_free Module.Free.self Prod.borelSpace Real.borelSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal instIsAddHaarMeasureProdRealVolume MeasurableSet.prod measurableSet_Ioi BorelSpace.opensMeasurable instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid measurableSet_Ioo HasFDerivAt.hasFDerivWithinAt hasFDerivAt_polarCoord_symm OpenPartialHomeomorph.injOn det_fderivPolarCoordSymm MeasureTheory.setLIntegral_congr_fun IsOpen.measurableSet Prod.opensMeasurableSpace OpenPartialHomeomorph.open_target abs_of_pos IsOrderedAddMonoid.toAddLeftMono
measurableSet_pi_polarCoord_target 📖	mathematical	—	MeasurableSet MeasurableSpace.pi Real Prod.instMeasurableSpace Real.measurableSpace Set.pi Set.univ PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord	—	MeasurableSet.univ_pi Finite.to_countable IsOpen.measurableSet Prod.opensMeasurableSpace BorelSpace.opensMeasurable Real.borelSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal OpenPartialHomeomorph.open_target
pi_polarCoord_symm_target_ae_eq_univ 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.pi Real MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume Set.image Pi.map OpenPartialHomeomorph.toFun' instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm polarCoord Set.pi Set.univ PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	MeasureTheory.Measure.instOuterMeasureClass Set.piMap_image_univ_pi OpenPartialHomeomorph.symm_image_target_eq_source MeasureTheory.volume_pi Set.pi_univ MeasureTheory.Measure.ae_eq_set_pi MeasureTheory.Measure.instSigmaFiniteProdVolume MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal polarCoord_source_ae_eq_univ
polarCoord_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord Real.sqrt Real.instAdd Monoid.toNatPow Real.instMonoid Complex.arg DFunLike.coe Equiv Complex EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Complex.equivRealProd	—	—
polarCoord_source 📖	mathematical	—	PartialEquiv.source Real OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord Set Set.instUnion setOf Real.instLT Real.instZero	—	—
polarCoord_source_ae_eq_univ 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.prod.measureSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord Set.univ	—	Set.compl_union MeasureTheory.Measure.addHaar_submodule Prod.borelSpace Real.borelSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.rclike_to_real Module.Projective.of_free Module.Free.self instIsAddHaarMeasureProdRealVolume LinearMap.ker_eq_top NeZero.charZero_one RCLike.charZero_rclike MeasureTheory.Measure.instOuterMeasureClass le_antisymm LE.le.trans MeasureTheory.measure_mono le_of_eq bot_le
polarCoord_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace OpenPartialHomeomorph.symm polarCoord Real.instMul Real.cos Real.sin	—	—
polarCoord_target 📖	mathematical	—	PartialEquiv.target Real OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace polarCoord SProd.sprod Set Set.instSProd Set.Ioi Real.instPreorder Real.instZero Set.Ioo Real.instNeg Real.pi	—	—

---

← Back to Index