Commit 2025-01-19 09:13 a58a89a2

View on Github →

feat: describe the interval of reals t where exp (t * X) is integrable (#20418) The set of reals t where exp (t * X) is integrable is an interval containing 0. Also prove integrability of other function for a parameter in that interval. Rename Probability/Moments to Probability/Moments/Basic

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

added theorem Real.rpow_max

Modified Mathlib/Data/Complex/Exponential.lean

added theorem Real.le_inv_mul_exp

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.integrable_norm_rpow_iff

Modified Mathlib/Probability/Distributions/Gaussian.lean

Renamed Mathlib/Probability/Moments.lean to Mathlib/Probability/Moments/Basic.lean

added theorem ProbabilityTheory.mgf_anti_of_nonpos

added theorem ProbabilityTheory.mgf_mono_of_nonneg

Created Mathlib/Probability/Moments/IntegrableExpMul.lean

added theorem ProbabilityTheory.add_half_inf_sub_mem_Ioo

added theorem ProbabilityTheory.aemeasurable_of_integrable_exp_mul

added theorem ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.convex_integrableExpSet

added def ProbabilityTheory.integrableExpSet

added theorem ProbabilityTheory.integrable_exp_abs_mul_abs

added theorem ProbabilityTheory.integrable_exp_abs_mul_abs_add

added theorem ProbabilityTheory.integrable_exp_mul_abs

added theorem ProbabilityTheory.integrable_exp_mul_abs_add

added theorem ProbabilityTheory.integrable_exp_mul_of_abs_le

added theorem ProbabilityTheory.integrable_exp_mul_of_le_of_le

added theorem ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le

added theorem ProbabilityTheory.integrable_exp_mul_of_nonpos_of_ge

added theorem ProbabilityTheory.integrable_of_mem_integrableExpSet

added theorem ProbabilityTheory.integrable_pow_abs_mul_exp_add_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_pow_abs_mul_exp_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_pow_abs_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_pow_abs_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_pow_mul_exp_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_pow_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_pow_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_rpow_abs_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_rpow_abs_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_rpow_of_integrable_exp_mul

added theorem ProbabilityTheory.integrable_rpow_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.memℒp_of_mem_interior_integrableExpSet

added theorem ProbabilityTheory.rpow_abs_le_mul_exp_abs

added theorem ProbabilityTheory.rpow_abs_le_mul_max_exp

added theorem ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos

added theorem ProbabilityTheory.sub_half_inf_sub_mem_Ioo