ComplexMGF

📁 Source: Mathlib/Probability/Moments/ComplexMGF.lean

Statistics

Metric	Count
Definitions complexMGF	1
Theorems ext_of_complexMGF_eq, ext_of_complexMGF_id_eq, analyticAt_complexMGF, analyticOnNhd_complexMGF, analyticOn_complexMGF, complexMGF_congr_identDistrib, complexMGF_id_map, complexMGF_id_mul_I, complexMGF_mul_I, complexMGF_ofReal, complexMGF_undef, differentiableOn_complexMGF, eqOn_complexMGF_of_mgf, eqOn_complexMGF_of_mgf', hasDerivAt_complexMGF, hasDerivAt_integral_pow_mul_exp, hasDerivAt_iteratedDeriv_complexMGF, integrableExpSet_eq_of_mgf, integrableExpSet_eq_of_mgf', iteratedDeriv_complexMGF, norm_complexMGF_le_mgf, re_complexMGF_ofReal, re_complexMGF_ofReal'	23
Total	24

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_of_complexMGF_eq 📖	mathematical	AEMeasurable Real Real.measurableSpace ProbabilityTheory.complexMGF	map	—	Algebra.to_smulCommClass DFunLike.ne_iff inner_self_ne_zero MeasureTheory.ext_of_integral_char_eq Real.borelSpace Real.instCompleteSpace instSecondCountableTopologyReal Real.continuous_probChar Real.probChar_ne_one continuous_inner isFiniteMeasure_map conj_trivial instTrivialStarReal Complex.ofReal_mul MeasureTheory.integral_map Continuous.comp_aestronglyMeasurable Continuous.cexp continuous_id' MeasureTheory.AEStronglyMeasurable.mul_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing MeasureTheory.AEStronglyMeasurable.const_mul Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right secondCountable_of_proper Complex.instProperSpace Complex.continuous_ofReal mul_comm mul_assoc
ext_of_complexMGF_id_eq 📖	—	ProbabilityTheory.complexMGF Real Real.measurableSpace	—	—	map_id ext_of_complexMGF_eq aemeasurable_id

ProbabilityTheory

Definitions

Name	Category	Theorems
complexMGF 📖	CompOp	20 math math: eqOn_complexMGF_of_mgf', complexMGF_mul_I, eqOn_complexMGF_of_mgf, iteratedDeriv_complexMGF, analyticAt_complexMGF, complexMGF_id_mul_I, complexMGF_gaussianReal, hasDerivAt_complexMGF, norm_complexMGF_le_mgf, complexMGF_congr_identDistrib, differentiableOn_complexMGF, complexMGF_id_map, complexMGF_id_gaussianReal, hasDerivAt_iteratedDeriv_complexMGF, analyticOn_complexMGF, complexMGF_ofReal, complexMGF_undef, re_complexMGF_ofReal', analyticOnNhd_complexMGF, re_complexMGF_ofReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_complexMGF 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace complexMGF	—	analyticOnNhd_complexMGF
analyticOnNhd_complexMGF 📖	mathematical	—	AnalyticOnNhd Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace complexMGF setOf Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn_complexMGF IsOpen.preimage Complex.continuous_re isOpen_interior
analyticOn_complexMGF 📖	mathematical	—	AnalyticOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace complexMGF setOf Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	—	AnalyticOnNhd.analyticOn analyticOnNhd_complexMGF
complexMGF_congr_identDistrib 📖	mathematical	IdentDistrib Real Real.measurableSpace	complexMGF	—	complexMGF_id_map IdentDistrib.aemeasurable_fst IdentDistrib.aemeasurable_snd IdentDistrib.map_eq
complexMGF_id_map 📖	mathematical	AEMeasurable Real Real.measurableSpace	complexMGF MeasureTheory.Measure.map	—	complexMGF.eq_1 MeasureTheory.integral_map Continuous.comp_aestronglyMeasurable Continuous.cexp continuous_id' MeasureTheory.AEStronglyMeasurable.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.continuous_ofReal aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal
complexMGF_id_mul_I 📖	mathematical	—	complexMGF Real Real.measurableSpace Complex Complex.instMul Complex.ofReal Complex.I MeasureTheory.charFun InnerProductSpace.toInner Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal	—	conj_trivial instTrivialStarReal Complex.ofReal_mul 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_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero
complexMGF_mul_I 📖	mathematical	AEMeasurable Real Real.measurableSpace	complexMGF Complex Complex.instMul Complex.ofReal Complex.I MeasureTheory.charFun InnerProductSpace.toInner Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal MeasureTheory.Measure.map	—	complexMGF_id_map complexMGF_id_mul_I
complexMGF_ofReal 📖	mathematical	—	complexMGF Complex.ofReal mgf	—	complexMGF.eq_1 mgf.eq_1 integral_complex_ofReal
complexMGF_undef 📖	mathematical	AEMeasurable Real Real.measurableSpace MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp Real.instMul Complex.re	complexMGF Complex Complex.instZero	—	complexMGF.eq_1 MeasureTheory.integral_undef MeasureTheory.integrable_norm_iff Continuous.comp_aestronglyMeasurable Continuous.cexp continuous_id' MeasureTheory.AEStronglyMeasurable.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.continuous_ofReal AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal Complex.norm_exp MulZeroClass.mul_zero sub_zero
differentiableOn_complexMGF 📖	mathematical	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField complexMGF setOf Real Set Set.instMembership interior Real.pseudoMetricSpace integrableExpSet Complex.re	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasDerivAt_complexMGF HasFDerivWithinAt.differentiableWithinAt HasFDerivAt.hasFDerivWithinAt hasDerivAt_iff_hasFDerivAt
eqOn_complexMGF_of_mgf 📖	mathematical	mgf	Set.EqOn Complex complexMGF setOf Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	—	eqOn_complexMGF_of_mgf' LT.lt.ne' mgf_pos MulZeroClass.zero_mul Real.exp_zero MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure enorm_one NormedDivisionRing.to_normOneClass mgf_zero'
eqOn_complexMGF_of_mgf' 📖	mathematical	mgf MeasureTheory.Measure MeasureTheory.Measure.instZero	Set.EqOn Complex complexMGF setOf Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	—	Set.nonempty_iff_ne_empty analyticOnNhd_complexMGF integrableExpSet_eq_of_mgf' AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq Convex.isPreconnected IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Convex.linear_preimage Convex.interior instIsTopologicalAddGroupReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul instIsTopologicalRingReal Real.instZeroLEOneClass convex_integrableExpSet Filter.Frequently.of_forall PerfectSpace.not_isolated instPerfectSpace complexMGF_ofReal Filter.frequently_iff_seq_forall TopologicalSpace.isCountablyGenerated_nhdsWithin FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace tendsto_nhdsWithin_iff Filter.tendsto_ofReal_iff instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
hasDerivAt_complexMGF 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField Complex.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Complex.instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing complexMGF MeasureTheory.integral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing pow_zero one_mul zero_add pow_one hasDerivAt_integral_pow_mul_exp
hasDerivAt_integral_pow_mul_exp 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField Complex.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Complex.instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing MeasureTheory.integral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	—	aemeasurable_of_mem_interior_integrableExpSet IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing mem_nhds_iff_exists_Ioo_subset instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMinOrderOfNontrivial mem_interior_iff_mem_nhds Nat.instAtLeastTwoHAddOfNat IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivAt_integral_of_dominated_loc_of_deriv_le Metric.ball_mem_nhds Filter.Eventually.of_forall Continuous.comp_aestronglyMeasurable continuous_mul IsTopologicalSemiring.toContinuousMul MeasureTheory.AEStronglyMeasurable.prodMk Continuous.pow continuous_id' Complex.continuous_ofReal AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal Continuous.cexp MeasureTheory.AEStronglyMeasurable.const_mul integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass norm_mul NormedDivisionRing.toNormMulClass norm_pow NormedDivisionRing.to_normOneClass Complex.norm_real Complex.norm_exp MulZeroClass.mul_zero sub_zero mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.exp_monotone add_sub_cancel Complex.add_re add_mul Distrib.rightDistribClass add_le_add_right LE.le.trans le_abs_self abs_mul mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Complex.abs_re_le_norm LT.lt.le dist_eq_norm abs_nonneg pow_nonneg IsOrderedRing.toZeroLEOneClass integrable_pow_abs_mul_exp_add_of_integrable_exp_mul add_half_inf_sub_mem_Ioo sub_half_inf_sub_mem_Ioo le_of_lt div_pos Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_of_lt_of_le HasDerivAt.congr_simp pow_succ mul_assoc HasDerivAt.const_mul Complex.exp_eq_exp_ℂ NonUnitalSeminormedRing.toIsTopologicalRing smul_eq_mul mul_comm hasDerivAt_exp_smul_const Complex.instCompleteSpace
hasDerivAt_iteratedDeriv_complexMGF 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField Complex.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Complex.instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing iteratedDeriv Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace complexMGF MeasureTheory.integral Real.instRCLike instInnerProductSpaceRealComplex	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasDerivAt.congr_simp iteratedDeriv_zero zero_add pow_one hasDerivAt_complexMGF iteratedDeriv_succ IsOpen.eventually_mem IsOpen.preimage Complex.continuous_re isOpen_interior Filter.mp_mem Filter.univ_mem' HasDerivAt.deriv IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.EventuallyEq.hasDerivAt_iff hasDerivAt_integral_pow_mul_exp
integrableExpSet_eq_of_mgf 📖	mathematical	mgf	integrableExpSet	—	integrableExpSet_eq_of_mgf' LT.lt.ne' mgf_pos MulZeroClass.zero_mul Real.exp_zero MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure enorm_one NormedDivisionRing.to_normOneClass mgf_zero'
integrableExpSet_eq_of_mgf' 📖	mathematical	mgf MeasureTheory.Measure MeasureTheory.Measure.instZero	integrableExpSet	—	Set.ext not_iff_not mgf_pos_iff
iteratedDeriv_complexMGF 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Complex.re	iteratedDeriv Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace complexMGF MeasureTheory.integral Real.instRCLike instInnerProductSpaceRealComplex	—	iteratedDeriv_zero pow_zero one_mul iteratedDeriv_succ HasDerivAt.deriv hasDerivAt_iteratedDeriv_complexMGF
norm_complexMGF_le_mgf 📖	mathematical	—	Real Real.instLE Norm.norm Complex Complex.instNorm complexMGF mgf Complex.re	—	complexMGF.eq_1 Complex.re_add_im add_mul Distrib.rightDistribClass Complex.exp_add MeasureTheory.norm_integral_le_integral_norm Complex.norm_mul Complex.norm_exp MulZeroClass.mul_zero sub_zero mul_one sub_self MulZeroClass.zero_mul add_zero Real.exp_zero
re_complexMGF_ofReal 📖	mathematical	—	Complex.re complexMGF Complex.ofReal mgf	—	complexMGF_ofReal
re_complexMGF_ofReal' 📖	mathematical	—	Complex.re complexMGF Complex.ofReal mgf	—	re_complexMGF_ofReal

---

← Back to Index