MGFAnalytic

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

Statistics

Metric	Count
Definitions	0
Theorems analyticAt_cgf, analyticAt_iteratedDeriv_mgf, analyticAt_mgf, analyticOnNhd_cgf, analyticOnNhd_iteratedDeriv_mgf, analyticOnNhd_mgf, analyticOn_cgf, analyticOn_iteratedDeriv_mgf, analyticOn_mgf, continuousOn_mgf, continuous_mgf, deriv_cgf, deriv_cgf_zero, deriv_mgf, deriv_mgf_zero, differentiableAt_iteratedDeriv_mgf, differentiableAt_mgf, differentiableOn_mgf, exists_cgf_eq_iteratedDeriv_two_cgf_mul, hasDerivAt_integral_pow_mul_exp_real, hasDerivAt_iteratedDeriv_mgf, hasDerivAt_mgf, hasFPowerSeriesAt_mgf, iteratedDeriv_mgf, iteratedDeriv_mgf_zero, iteratedDeriv_two_cgf, iteratedDeriv_two_cgf_eq_integral	27
Total	27

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_cgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	AnalyticAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal cgf	—	cgf_zero_measure analyticAt_const AnalyticAt.log analyticAt_mgf mgf_pos' interior_subset
analyticAt_iteratedDeriv_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	AnalyticAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal iteratedDeriv mgf	—	analyticOnNhd_iteratedDeriv_mgf
analyticAt_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	AnalyticAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal mgf	—	re_complexMGF_ofReal' AnalyticAt.re_ofReal analyticAt_complexMGF
analyticOnNhd_cgf 📖	mathematical	—	AnalyticOnNhd Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal cgf interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	—	analyticAt_cgf
analyticOnNhd_iteratedDeriv_mgf 📖	mathematical	—	AnalyticOnNhd Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal iteratedDeriv mgf interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	—	iteratedDeriv_eq_iterate AnalyticOnNhd.iterated_deriv Real.instCompleteSpace analyticOnNhd_mgf
analyticOnNhd_mgf 📖	mathematical	—	AnalyticOnNhd Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal mgf interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	—	analyticAt_mgf
analyticOn_cgf 📖	mathematical	—	AnalyticOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal cgf interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	—	AnalyticOnNhd.analyticOn analyticOnNhd_cgf
analyticOn_iteratedDeriv_mgf 📖	mathematical	—	AnalyticOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal iteratedDeriv mgf interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	—	AnalyticOnNhd.analyticOn analyticOnNhd_iteratedDeriv_mgf
analyticOn_mgf 📖	mathematical	—	AnalyticOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal mgf interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	—	AnalyticOnNhd.analyticOn analyticOnNhd_mgf
continuousOn_mgf 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace mgf interior integrableExpSet	—	DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology differentiableOn_mgf
continuous_mgf 📖	mathematical	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp Real.instMul	Continuous mgf	—	continuousOn_univ interior_eq_univ Set.ext continuousOn_mgf
deriv_cgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal cgf DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.integral Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup mgf	—	cgf_zero_measure MeasureTheory.integral_zero_measure mgf_zero_measure div_zero deriv_const interior_subset deriv.log differentiableAt_mgf LT.lt.ne' mgf_pos' deriv_mgf
deriv_cgf_zero 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Real.instZero	deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal cgf DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.integral Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.Measure.real Set.univ	—	deriv_cgf MulZeroClass.zero_mul Real.exp_zero mul_one mgf_zero'
deriv_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal mgf MeasureTheory.integral Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup	—	HasDerivAt.deriv hasDerivAt_mgf
deriv_mgf_zero 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Real.instZero	deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal mgf MeasureTheory.integral Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup	—	deriv_mgf MulZeroClass.zero_mul Real.exp_zero mul_one
differentiableAt_iteratedDeriv_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal iteratedDeriv Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup mgf	—	AnalyticAt.differentiableAt analyticAt_iteratedDeriv_mgf
differentiableAt_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal mgf	—	AnalyticAt.differentiableAt analyticAt_mgf
differentiableOn_mgf 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace mgf interior integrableExpSet	—	DifferentiableAt.differentiableWithinAt differentiableAt_mgf
exists_cgf_eq_iteratedDeriv_two_cgf_mul 📖	mathematical	Real Real.instLT Real.instZero MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set Set.instHasSubset Set.Icc Real.instPreorder interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	Set.instMembership Set.Ioo cgf DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	uniqueDiffOn_Icc Nat.instAtLeastTwoHAddOfNat sub_zero zero_div deriv_cgf_zero le_refl le_of_lt DifferentiableAt.derivWithin AnalyticAt.differentiableAt analyticAt_cgf taylorWithinEval_succ taylor_within_zero_eval cgf_zero CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_add Nat.cast_one mul_one inv_one pow_one one_mul iteratedDerivWithin_one MulZeroClass.mul_zero add_zero taylor_mean_remainder_lagrange_iteratedDeriv AnalyticOn.contDiffOn AnalyticOn.mono analyticOn_cgf
hasDerivAt_integral_pow_mul_exp_real 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.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 Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal MeasureTheory.integral Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup	—	RCLike.re_eq_complex_re integral_re integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet Filter.mp_mem IsOpen.eventually_mem isOpen_interior Filter.univ_mem' IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.EventuallyEq.hasDerivAt_iff HasDerivAt.real_of_complex hasDerivAt_integral_pow_mul_exp
hasDerivAt_iteratedDeriv_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.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 Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal iteratedDeriv Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup mgf MeasureTheory.integral	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.congr_simp iteratedDeriv_zero zero_add pow_one hasDerivAt_mgf iteratedDeriv_succ IsOpen.eventually_mem isOpen_interior Filter.mp_mem Filter.univ_mem' HasDerivAt.deriv IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.EventuallyEq.hasDerivAt_iff hasDerivAt_integral_pow_mul_exp_real
hasDerivAt_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.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 Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal mgf MeasureTheory.integral Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal pow_zero one_mul zero_add pow_one hasDerivAt_integral_pow_mul_exp_real
hasFPowerSeriesAt_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	HasFPowerSeriesAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal mgf FormalMultilinearSeries.ofScalars Real.instField Real.instRing Algebra.id Semifield.toCommSemiring Field.toSemifield instIsTopologicalRingReal DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.integral Real.instNatCast Nat.factorial	—	instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul iteratedDeriv_mgf AnalyticAt.hasFPowerSeriesAt Real.instCompleteSpace RCLike.charZero_rclike analyticAt_mgf
iteratedDeriv_mgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal mgf MeasureTheory.integral	—	iteratedDeriv_zero pow_zero one_mul iteratedDeriv_succ HasDerivAt.deriv hasDerivAt_iteratedDeriv_mgf
iteratedDeriv_mgf_zero 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet Real.instZero	iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal mgf MeasureTheory.integral Pi.instPow Monoid.toNatPow Real.instMonoid	—	iteratedDeriv_mgf MulZeroClass.zero_mul Real.exp_zero mul_one
iteratedDeriv_two_cgf 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal cgf Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.integral mgf Monoid.toNatPow Real.instMonoid deriv Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	—	iteratedDeriv_succ iteratedDeriv_one cgf_zero_measure deriv_zero MeasureTheory.integral_zero_measure mgf_zero_measure div_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat sub_self IsOpen.eventually_mem isOpen_interior Filter.mp_mem Filter.univ_mem' deriv_cgf deriv_mgf Filter.EventuallyEq.deriv_eq deriv_fun_div Filter.EventuallyEq.differentiableAt_iff Filter.EventuallyEq.symm differentiableAt_iteratedDeriv_mgf differentiableAt_mgf LT.lt.ne' mgf_pos' interior_subset sub_div pow_two div_mul_eq_div_div mul_div_assoc div_self mul_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_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_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw 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.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 Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right pow_one HasDerivAt.deriv hasDerivAt_integral_pow_mul_exp_real
iteratedDeriv_two_cgf_eq_integral 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal cgf DivInvMonoid.toDiv Real.instDivInvMonoid MeasureTheory.integral mgf	—	cgf_zero_measure iteratedDeriv_const_zero deriv_zero sub_zero MeasureTheory.integral_zero_measure mgf_zero_measure div_zero iteratedDeriv_two_cgf Nat.instAtLeastTwoHAddOfNat add_div sub_div sub_add mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass LT.lt.ne' mgf_pos' interior_subset deriv_cgf Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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 Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add add_mul Distrib.rightDistribClass sub_mul mul_assoc mul_comm MeasureTheory.Integrable.const_mul MeasureTheory.Integrable.mul_const pow_one integrable_pow_mul_exp_of_mem_interior_integrableExpSet MeasureTheory.integral_add MeasureTheory.Integrable.sub MeasureTheory.integral_sub MeasureTheory.integral_const_mul MeasureTheory.integral_mul_const mgf.eq_1 Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one

---

← Back to Index