Tilted

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

Statistics

Metric	Count
Definitions	0
Theorems integral_tilted_mul_eq_cgf, integral_tilted_mul_eq_mgf, integral_tilted_mul_self, memLp_tilted_mul, setIntegral_tilted_mul_eq_cgf, setIntegral_tilted_mul_eq_cgf', setIntegral_tilted_mul_eq_mgf, setIntegral_tilted_mul_eq_mgf', tilted_mul_apply_cgf, tilted_mul_apply_cgf', tilted_mul_apply_eq_ofReal_integral_cgf, tilted_mul_apply_eq_ofReal_integral_cgf', tilted_mul_apply_eq_ofReal_integral_mgf, tilted_mul_apply_eq_ofReal_integral_mgf', tilted_mul_apply_mgf, tilted_mul_apply_mgf', variance_tilted_mul	17
Total	17

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_tilted_mul_eq_cgf 📖	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	MeasureTheory.integral MeasureTheory.Measure.tilted 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 Real.instSub cgf	—	eq_zero_or_neZero MeasureTheory.tilted_zero_measure MeasureTheory.integral_zero_measure cgf_zero_measure sub_zero integral_tilted_mul_eq_mgf Real.exp_sub exp_cgf
integral_tilted_mul_eq_mgf 📖	mathematical	—	MeasureTheory.integral MeasureTheory.Measure.tilted Real Real.instMul 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp mgf	—	MeasureTheory.integral_tilted mgf.eq_1
integral_tilted_mul_self 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.tilted Real.instMul deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing cgf	—	integral_tilted_mul_eq_mgf deriv_cgf Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_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
memLp_tilted_mul 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	MeasureTheory.MemLp ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm ENNReal.ofNNReal MeasureTheory.Measure.tilted Real.instMul	—	aemeasurable_of_mem_interior_integrableExpSet MeasureTheory.AEStronglyMeasurable.mono_ac MeasureTheory.tilted_absolutelyContinuous AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top ENNReal.ofReal_rpow_of_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add MeasureTheory.Integrable.lintegral_lt_top MeasureTheory.integrable_tilted_iff interior_subset mul_comm integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet
setIntegral_tilted_mul_eq_cgf 📖	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	MeasureTheory.integral MeasureTheory.Measure.restrict MeasureTheory.Measure.tilted 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 Real.instSub cgf	—	eq_zero_or_neZero MeasureTheory.tilted_zero_measure MeasureTheory.Measure.restrict_zero MeasureTheory.integral_zero_measure cgf_zero_measure sub_zero setIntegral_tilted_mul_eq_mgf Real.exp_sub exp_cgf
setIntegral_tilted_mul_eq_cgf' 📖	mathematical	MeasurableSet 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	MeasureTheory.integral MeasureTheory.Measure.restrict MeasureTheory.Measure.tilted 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 Real.instSub cgf	—	eq_zero_or_neZero MeasureTheory.tilted_zero_measure MeasureTheory.Measure.restrict_zero MeasureTheory.integral_zero_measure cgf_zero_measure sub_zero setIntegral_tilted_mul_eq_mgf' Real.exp_sub exp_cgf
setIntegral_tilted_mul_eq_mgf 📖	mathematical	—	MeasureTheory.integral MeasureTheory.Measure.restrict MeasureTheory.Measure.tilted Real Real.instMul 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp mgf	—	MeasureTheory.setIntegral_tilted mgf.eq_1
setIntegral_tilted_mul_eq_mgf' 📖	mathematical	MeasurableSet	MeasureTheory.integral MeasureTheory.Measure.restrict MeasureTheory.Measure.tilted Real Real.instMul 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp mgf	—	MeasureTheory.setIntegral_tilted' mgf.eq_1
tilted_mul_apply_cgf 📖	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	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted MeasureTheory.lintegral MeasureTheory.Measure.restrict ENNReal.ofReal Real.instSub cgf	—	eq_zero_or_neZero MeasureTheory.tilted_zero_measure MeasureTheory.Measure.restrict_zero cgf_zero_measure sub_zero MeasureTheory.lintegral_zero_measure tilted_mul_apply_mgf Real.exp_sub exp_cgf
tilted_mul_apply_cgf' 📖	mathematical	MeasurableSet 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	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted MeasureTheory.lintegral MeasureTheory.Measure.restrict ENNReal.ofReal Real.instSub cgf	—	eq_zero_or_neZero MeasureTheory.tilted_zero_measure MeasureTheory.Measure.restrict_zero cgf_zero_measure sub_zero MeasureTheory.lintegral_zero_measure tilted_mul_apply_mgf' Real.exp_sub exp_cgf
tilted_mul_apply_eq_ofReal_integral_cgf 📖	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	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict Real.instSub cgf	—	eq_zero_or_neZero MeasureTheory.tilted_zero_measure MeasureTheory.Measure.restrict_zero cgf_zero_measure sub_zero MeasureTheory.integral_zero_measure ENNReal.ofReal_zero tilted_mul_apply_eq_ofReal_integral_mgf Real.exp_sub exp_cgf
tilted_mul_apply_eq_ofReal_integral_cgf' 📖	mathematical	MeasurableSet 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	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict Real.instSub cgf	—	eq_zero_or_neZero MeasureTheory.tilted_zero_measure MeasureTheory.Measure.restrict_zero cgf_zero_measure sub_zero MeasureTheory.integral_zero_measure ENNReal.ofReal_zero tilted_mul_apply_eq_ofReal_integral_mgf' Real.exp_sub exp_cgf
tilted_mul_apply_eq_ofReal_integral_mgf 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted Real Real.instMul ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp mgf	—	MeasureTheory.tilted_apply_eq_ofReal_integral mgf.eq_1
tilted_mul_apply_eq_ofReal_integral_mgf' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted Real Real.instMul ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp mgf	—	MeasureTheory.tilted_apply_eq_ofReal_integral' mgf.eq_1
tilted_mul_apply_mgf 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted Real Real.instMul MeasureTheory.lintegral MeasureTheory.Measure.restrict ENNReal.ofReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp mgf	—	MeasureTheory.tilted_apply mgf.eq_1
tilted_mul_apply_mgf' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.tilted Real Real.instMul MeasureTheory.lintegral MeasureTheory.Measure.restrict ENNReal.ofReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp mgf	—	MeasureTheory.tilted_apply' mgf.eq_1
variance_tilted_mul 📖	mathematical	Real Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace integrableExpSet	variance MeasureTheory.Measure.tilted Real.instMul iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal cgf	—	variance_eq_integral MeasureTheory.AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace MeasureTheory.MemLp.aestronglyMeasurable memLp_tilted_mul integral_tilted_mul_self iteratedDeriv_two_cgf_eq_integral integral_tilted_mul_eq_mgf MeasureTheory.integral_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_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.pow_congr Mathlib.Tactic.Ring.sub_congr 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add 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 Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero

---

← Back to Index