Tilted

📁 Source: Mathlib/MeasureTheory/Measure/Tilted.lean

Statistics

Metric	Count
Definitions tilted	1
Theorems absolutelyContinuous_tilted, integrable_tilted_iff, integral_exp_tilted, integral_tilted, isProbabilityMeasure_tilted, isZeroOrProbabilityMeasure_tilted, lintegral_tilted, log_rnDeriv_tilted_left_self, rnDeriv_tilted_left, rnDeriv_tilted_left_self, rnDeriv_tilted_right, setIntegral_tilted, setIntegral_tilted', setLIntegral_tilted, setLIntegral_tilted', tilted_absolutelyContinuous, tilted_apply, tilted_apply', tilted_apply_eq_ofReal_integral, tilted_apply_eq_ofReal_integral', tilted_comm, tilted_congr, tilted_const, tilted_const', tilted_eq_withDensity_nnreal, tilted_neg_same, tilted_neg_same', tilted_of_not_aemeasurable, tilted_of_not_integrable, tilted_tilted, tilted_zero, tilted_zero', tilted_zero_measure, toReal_rnDeriv_tilted_left, toReal_rnDeriv_tilted_right	35
Total	36

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_tilted 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Measure.AbsolutelyContinuous Measure.tilted	—	eq_zero_or_neZero tilted_zero_measure withDensity_absolutelyContinuous' AEMeasurable.ennreal_ofReal AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Filter.univ_mem' Measure.instOuterMeasureClass div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_exp_pos
integrable_tilted_iff 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Measure.tilted SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	tilted_zero_measure Real.aemeasurable_of_aemeasurable_exp AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace Measure.tilted.eq_1 integrable_withDensity_iff_integrable_smul₀' AEMeasurable.ennreal_ofReal AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal AEMeasurable.exp Measure.instOuterMeasureClass ENNReal.toReal_ofReal Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal le_of_lt smul_smul div_eq_inv_mul integrable_fun_smul_iff NormedSpace.toIsBoundedSMul LT.lt.ne' integral_exp_pos
integral_exp_tilted 📖	mathematical	—	integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.tilted Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Pi.instAdd Real.instAdd	—	eq_zero_or_neZero tilted_zero_measure integral_zero_measure div_zero integral_tilted Pi.add_apply Real.exp_add 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 div_eq_mul_inv integral_mul_const
integral_tilted 📖	mathematical	—	integral Measure.tilted Real 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 Real.normedAddCommGroup NormedField.toNormedSpace	—	setIntegral_univ setIntegral_tilted' MeasurableSet.univ
isProbabilityMeasure_tilted 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	IsProbabilityMeasure Measure.tilted	—	tilted_apply' MeasurableSet.univ setLIntegral_univ ENNReal.ofReal_div_of_pos integral_exp_pos div_eq_mul_inv lintegral_mul_const'' AEMeasurable.ennreal_ofReal AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace ofReal_integral_eq_lintegral_ofReal ae_of_all Measure.instOuterMeasureClass LT.lt.le Real.exp_pos ENNReal.mul_inv_cancel
isZeroOrProbabilityMeasure_tilted 📖	mathematical	—	IsZeroOrProbabilityMeasure Measure.tilted	—	eq_zero_or_neZero tilted_zero_measure instIsZeroOrProbabilityMeasureOfNatMeasure isProbabilityMeasure_tilted instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure tilted_of_not_integrable
lintegral_tilted 📖	mathematical	—	lintegral Measure.tilted ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	setLIntegral_univ setLIntegral_tilted' MeasurableSet.univ
log_rnDeriv_tilted_left_self 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real.log ENNReal.toReal Measure.rnDeriv Measure.tilted Real.instSub integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	eq_zero_or_neZero Measure.instOuterMeasureClass ae.congr_simp ae_zero Filter.eventually_bot Real.aemeasurable_of_aemeasurable_exp AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace Filter.mp_mem rnDeriv_tilted_left_self Filter.univ_mem' ENNReal.toReal_ofReal Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal le_of_lt Real.log_div LT.lt.ne' integral_exp_pos Real.log_exp
rnDeriv_tilted_left 📖	mathematical	AEMeasurable Real Real.measurableSpace	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.rnDeriv Measure.tilted Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.rnDeriv_withDensity_left AEMeasurable.ennreal_ofReal AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.comp_aemeasurable Real.measurable_exp ae_of_all Measure.instOuterMeasureClass
rnDeriv_tilted_left_self 📖	mathematical	AEMeasurable Real Real.measurableSpace	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.rnDeriv Measure.tilted ENNReal.ofReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Filter.EventuallyEq.trans Measure.instOuterMeasureClass rnDeriv_tilted_left Filter.mp_mem Measure.rnDeriv_self Filter.univ_mem' mul_one
rnDeriv_tilted_right 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.rnDeriv Measure.tilted Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real.instMul Real.instNeg integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	eq_zero_or_neZero Measure.instOuterMeasureClass ae.congr_simp ae_zero Filter.eventually_bot Filter.EventuallyEq.trans Measure.rnDeriv_withDensity_right AEMeasurable.ennreal_ofReal AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Filter.univ_mem' div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_exp_pos ae_of_all ENNReal.ofReal_inv_of_pos inv_div' Real.exp_neg div_eq_mul_inv inv_inv
setIntegral_tilted 📖	mathematical	—	integral Measure.restrict Measure.tilted Real 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 Real.normedAddCommGroup NormedField.toNormedSpace	—	tilted_eq_withDensity_nnreal setIntegral_withDensity_eq_setIntegral_smul₀' AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.comp_aemeasurable Real.measurable_exp aemeasurable_coe_nnreal_real_iff AEMeasurable.restrict Real.aemeasurable_of_aemeasurable_exp AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace tilted_of_not_aemeasurable Measure.restrict_zero integral_zero_measure integral_undef div_zero zero_smul integral_zero
setIntegral_tilted' 📖	mathematical	MeasurableSet	integral Measure.restrict Measure.tilted Real 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 Real.normedAddCommGroup NormedField.toNormedSpace	—	tilted_eq_withDensity_nnreal setIntegral_withDensity_eq_setIntegral_smul₀ AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.comp_aemeasurable Real.measurable_exp aemeasurable_coe_nnreal_real_iff AEMeasurable.restrict Real.aemeasurable_of_aemeasurable_exp AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace tilted_of_not_aemeasurable Measure.restrict_zero integral_zero_measure integral_undef div_zero zero_smul integral_zero
setLIntegral_tilted 📖	mathematical	—	lintegral Measure.restrict Measure.tilted ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.tilted.eq_1 setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀' AEMeasurable.restrict AEMeasurable.ennreal_ofReal AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.comp_aemeasurable Real.measurable_exp Filter.univ_mem' Measure.instOuterMeasureClass Real.aemeasurable_of_aemeasurable_exp AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace tilted_of_not_aemeasurable Measure.restrict_zero lintegral_zero_measure integral_undef div_zero ENNReal.ofReal_zero MulZeroClass.zero_mul lintegral_const Measure.restrict_apply Set.univ_inter
setLIntegral_tilted' 📖	mathematical	MeasurableSet	lintegral Measure.restrict Measure.tilted ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofReal Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.tilted.eq_1 setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ AEMeasurable.restrict AEMeasurable.ennreal_ofReal AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.comp_aemeasurable Real.measurable_exp Filter.univ_mem' Measure.instOuterMeasureClass Real.aemeasurable_of_aemeasurable_exp AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace tilted_of_not_aemeasurable Measure.restrict_zero lintegral_zero_measure integral_undef div_zero ENNReal.ofReal_zero MulZeroClass.zero_mul lintegral_const Measure.restrict_apply Set.univ_inter
tilted_absolutelyContinuous 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.tilted	—	withDensity_absolutelyContinuous
tilted_apply 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.tilted lintegral Measure.restrict ENNReal.ofReal Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.tilted.eq_1 withDensity_apply'
tilted_apply' 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.tilted lintegral Measure.restrict ENNReal.ofReal Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.tilted.eq_1 withDensity_apply
tilted_apply_eq_ofReal_integral 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.tilted ENNReal.ofReal integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp	—	tilted_apply ofReal_integral_eq_lintegral_ofReal Integrable.div_const Integrable.integrableOn ae_of_all Measure.instOuterMeasureClass Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal le_of_lt tilted_of_not_integrable integral_undef div_zero integral_zero ENNReal.ofReal_zero
tilted_apply_eq_ofReal_integral' 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.tilted ENNReal.ofReal integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp	—	tilted_apply' ofReal_integral_eq_lintegral_ofReal Integrable.div_const Integrable.integrableOn ae_of_all Measure.instOuterMeasureClass Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal le_of_lt tilted_of_not_integrable integral_undef div_zero integral_zero ENNReal.ofReal_zero
tilted_comm 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Measure.tilted	—	tilted_tilted add_comm
tilted_congr 📖	mathematical	Filter.EventuallyEq Real ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Measure.tilted	—	Measure.instOuterMeasureClass integral_congr_ae Filter.mp_mem Filter.univ_mem' withDensity_congr_ae
tilted_const 📖	mathematical	—	Measure.tilted	—	IsScalarTower.right tilted_const' IsProbabilityMeasure.measure_univ inv_one one_smul
tilted_const' 📖	mathematical	—	Measure.tilted ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.instInv DFunLike.coe Set Measure.instFunLike Set.univ	—	eq_zero_or_neZero IsScalarTower.right tilted_zero_measure ENNReal.inv_zero smul_zero integral_const Real.instCompleteSpace withDensity_const MulZeroClass.zero_mul div_zero ENNReal.ofReal_zero zero_smul ENNReal.inv_top div_eq_mul_inv mul_inv mul_comm mul_assoc inv_mul_cancel₀ LT.lt.ne' Real.exp_pos mul_one measureReal_def ENNReal.toReal_inv ENNReal.ofReal_toReal
tilted_eq_withDensity_nnreal 📖	mathematical	—	Measure.tilted Measure.withDensity ENNReal.ofNNReal Real Real.instLE Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.tilted.eq_1 ENNReal.ofReal_eq_coe_nnreal
tilted_neg_same 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Measure.tilted Pi.instNeg Real.instNeg	—	IsScalarTower.right tilted_neg_same' IsProbabilityMeasure.measure_univ inv_one one_smul
tilted_neg_same' 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Measure.tilted Pi.instNeg Real.instNeg ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.instInv DFunLike.coe Set Measure.instFunLike Set.univ	—	IsScalarTower.right tilted_tilted add_neg_cancel tilted_zero'
tilted_of_not_aemeasurable 📖	mathematical	AEMeasurable Real Real.measurableSpace	Measure.tilted Measure Measure.instZero	—	tilted_of_not_integrable Real.aemeasurable_of_aemeasurable_exp AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace
tilted_of_not_integrable 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Measure.tilted Measure Measure.instZero	—	Measure.tilted.eq_1 integral_undef IsScalarTower.right div_zero ENNReal.ofReal_zero withDensity_const zero_smul
tilted_tilted 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Measure.tilted Pi.instAdd Real.instAdd	—	eq_zero_or_neZero tilted_zero_measure Measure.ext tilted_apply' setLIntegral_tilted' ENNReal.ofReal_mul Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal le_of_lt integral_exp_tilted Pi.add_apply Real.exp_add LT.lt.ne' integral_exp_pos Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt one_ne_zero NeZero.one GroupWithZero.toNontrivial one_div
tilted_zero 📖	mathematical	—	Measure.tilted Pi.instZero Real Real.instZero	—	IsScalarTower.right tilted_zero' IsProbabilityMeasure.measure_univ inv_one one_smul
tilted_zero' 📖	mathematical	—	Measure.tilted Pi.instZero Real Real.instZero ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.instInv DFunLike.coe Set Measure.instFunLike Set.univ	—	IsScalarTower.right tilted_const'
tilted_zero_measure 📖	mathematical	—	Measure.tilted Measure Measure.instZero	—	IsScalarTower.right integral_zero_measure div_zero ENNReal.ofReal_zero withDensity_const smul_zero
toReal_rnDeriv_tilted_left 📖	mathematical	AEMeasurable Real Real.measurableSpace	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass ENNReal.toReal Measure.rnDeriv Measure.tilted Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Filter.mp_mem Measure.instOuterMeasureClass rnDeriv_tilted_left Filter.univ_mem' ENNReal.toReal_mul IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.exp_pos integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal le_of_lt
toReal_rnDeriv_tilted_right 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.exp	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass ENNReal.toReal Measure.rnDeriv Measure.tilted Real.instMul Real.instNeg integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Filter.mp_mem Measure.instOuterMeasureClass rnDeriv_tilted_right Filter.univ_mem' ENNReal.toReal_mul IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Real.exp_pos integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal

MeasureTheory.Measure

Definitions

Name	Category	Theorems
tilted 📖	CompOp	58 math math: MeasureTheory.setIntegral_tilted, MeasureTheory.isZeroOrProbabilityMeasure_tilted, MeasureTheory.tilted_congr, MeasureTheory.toReal_rnDeriv_tilted_left, MeasureTheory.tilted_neg_same', MeasureTheory.integral_tilted, ProbabilityTheory.tilted_mul_apply_cgf, MeasureTheory.tilted_zero, MeasureTheory.integral_exp_tilted, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf', MeasureTheory.llr_tilted_right, MeasureTheory.tilted_comm, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf, MeasureTheory.isProbabilityMeasure_tilted, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf', MeasureTheory.integral_llr_tilted_left, ProbabilityTheory.setIntegral_tilted_mul_eq_mgf', MeasureTheory.tilted_tilted, MeasureTheory.tilted_neg_same, ProbabilityTheory.tilted_mul_apply_mgf', MeasureTheory.tilted_apply_eq_ofReal_integral, MeasureTheory.tilted_const', MeasureTheory.tilted_apply, MeasureTheory.log_rnDeriv_tilted_left_self, ProbabilityTheory.setIntegral_tilted_mul_eq_cgf', MeasureTheory.integrable_tilted_iff, MeasureTheory.setLIntegral_tilted, ProbabilityTheory.integral_tilted_mul_eq_mgf, MeasureTheory.rnDeriv_tilted_left, MeasureTheory.tilted_zero_measure, ProbabilityTheory.tilted_mul_apply_mgf, MeasureTheory.setIntegral_tilted', ProbabilityTheory.memLp_tilted_mul, MeasureTheory.tilted_of_not_integrable, MeasureTheory.absolutelyContinuous_tilted, MeasureTheory.tilted_zero', MeasureTheory.integrable_llr_tilted_right, MeasureTheory.lintegral_tilted, MeasureTheory.llr_tilted_left, ProbabilityTheory.setIntegral_tilted_mul_eq_mgf, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf, ProbabilityTheory.setIntegral_tilted_mul_eq_cgf, MeasureTheory.tilted_absolutelyContinuous, MeasureTheory.setLIntegral_tilted', MeasureTheory.integrable_llr_tilted_left, MeasureTheory.tilted_eq_withDensity_nnreal, MeasureTheory.rnDeriv_tilted_right, MeasureTheory.tilted_of_not_aemeasurable, MeasureTheory.tilted_apply_eq_ofReal_integral', MeasureTheory.integral_llr_tilted_right, MeasureTheory.rnDeriv_tilted_left_self, ProbabilityTheory.variance_tilted_mul, MeasureTheory.tilted_const, ProbabilityTheory.integral_tilted_mul_self, MeasureTheory.toReal_rnDeriv_tilted_right, ProbabilityTheory.tilted_mul_apply_cgf', MeasureTheory.tilted_apply', ProbabilityTheory.integral_tilted_mul_eq_cgf

---

← Back to Index