Commit 2023-06-21 10:46 d1395178

View on Github →

feat: port Probability.StrongLaw (#5336) This PR completes the port of the entire Probability folder to mathlib4 – for real this time.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/StrongLaw.lean

added theorem MeasureTheory.AEStronglyMeasurable.integrable_truncation

added theorem MeasureTheory.AEStronglyMeasurable.memℒp_truncation

added theorem MeasureTheory.AEStronglyMeasurable.truncation

added theorem ProbabilityTheory.IdentDistrib.truncation

added theorem ProbabilityTheory.abs_truncation_le_abs_self

added theorem ProbabilityTheory.abs_truncation_le_bound

added theorem ProbabilityTheory.integral_truncation_eq_intervalIntegral

added theorem ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg

added theorem ProbabilityTheory.integral_truncation_le_integral_of_nonneg

added theorem ProbabilityTheory.moment_truncation_eq_intervalIntegral

added theorem ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg

added theorem ProbabilityTheory.strong_law_Lp

added theorem ProbabilityTheory.strong_law_ae

added theorem ProbabilityTheory.strong_law_aux1

added theorem ProbabilityTheory.strong_law_aux2

added theorem ProbabilityTheory.strong_law_aux3

added theorem ProbabilityTheory.strong_law_aux4

added theorem ProbabilityTheory.strong_law_aux5

added theorem ProbabilityTheory.strong_law_aux6

added theorem ProbabilityTheory.strong_law_aux7

added theorem ProbabilityTheory.sum_prob_mem_Ioc_le

added theorem ProbabilityTheory.sum_variance_truncation_le

added theorem ProbabilityTheory.tendsto_integral_truncation

added def ProbabilityTheory.truncation

added theorem ProbabilityTheory.truncation_eq_of_nonneg

added theorem ProbabilityTheory.truncation_eq_self

added theorem ProbabilityTheory.truncation_nonneg

added theorem ProbabilityTheory.truncation_zero

added theorem ProbabilityTheory.tsum_prob_mem_Ioi_lt_top