Commit 2023-06-16 15:28 7f3d0dc7

View on Github →

feat: port Probability.Kernel.CondCdf (#5143)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/CondCdf.lean

added theorem Directed.sequence_anti

added theorem Directed.sequence_le

added theorem ENNReal.ofReal_cinfi

added theorem MeasureTheory.Measure.IicSnd_ac_fst

added theorem MeasureTheory.Measure.IicSnd_apply

added theorem MeasureTheory.Measure.IicSnd_le_fst

added theorem MeasureTheory.Measure.IicSnd_mono

added theorem MeasureTheory.Measure.IicSnd_univ

added theorem MeasureTheory.Measure.IsFiniteMeasure.IicSnd

added theorem MeasureTheory.Measure.iInf_IicSnd_gt

added theorem MeasureTheory.Measure.tendsto_IicSnd_atBot

added theorem MeasureTheory.Measure.tendsto_IicSnd_atTop

added structure ProbabilityTheory.HasCondCdf

added theorem ProbabilityTheory.bddBelow_range_condCdfRat_gt

added theorem ProbabilityTheory.condCdf'_def'

added theorem ProbabilityTheory.condCdf'_eq_condCdfRat

added theorem ProbabilityTheory.condCdf'_nonneg

added theorem ProbabilityTheory.condCdfRat_ae_eq

added theorem ProbabilityTheory.condCdfRat_le_one

added theorem ProbabilityTheory.condCdfRat_nonneg

added theorem ProbabilityTheory.condCdfRat_of_mem

added theorem ProbabilityTheory.condCdfRat_of_not_mem

added def ProbabilityTheory.condCdfSet

added theorem ProbabilityTheory.condCdf_ae_eq

added theorem ProbabilityTheory.condCdf_eq_condCdfRat

added theorem ProbabilityTheory.condCdf_le_one

added theorem ProbabilityTheory.condCdf_nonneg

added theorem ProbabilityTheory.continuousWithinAt_condCdf'_Ici

added theorem ProbabilityTheory.hasCondCdf_ae

added theorem ProbabilityTheory.hasCondCdf_of_mem_condCdfSet

added theorem ProbabilityTheory.inf_gt_condCdfRat

added theorem ProbabilityTheory.inf_gt_preCdf

added theorem ProbabilityTheory.integrable_condCdf

added theorem ProbabilityTheory.integral_condCdf

added theorem ProbabilityTheory.lintegral_condCdf

added theorem ProbabilityTheory.measurableSet_condCdfSet

added theorem ProbabilityTheory.measurable_condCdf

added theorem ProbabilityTheory.measurable_condCdfRat

added theorem ProbabilityTheory.measurable_measure_condCdf

added theorem ProbabilityTheory.measurable_preCdf

added theorem ProbabilityTheory.measure_condCdf_Iic

added theorem ProbabilityTheory.measure_condCdf_univ

added theorem ProbabilityTheory.mem_condCdfSet_ae

added theorem ProbabilityTheory.monotone_condCdf'

added theorem ProbabilityTheory.monotone_condCdfRat

added theorem ProbabilityTheory.monotone_preCdf

added theorem ProbabilityTheory.ofReal_condCdfRat_ae_eq

added theorem ProbabilityTheory.ofReal_condCdf_ae_eq

added theorem ProbabilityTheory.preCdf_le_one

added theorem ProbabilityTheory.set_integral_condCdf

added theorem ProbabilityTheory.set_lintegral_condCdf

added theorem ProbabilityTheory.set_lintegral_condCdf_rat

added theorem ProbabilityTheory.set_lintegral_iInf_gt_preCdf

added theorem ProbabilityTheory.set_lintegral_preCdf_fst

added theorem ProbabilityTheory.stronglyMeasurable_condCdf

added theorem ProbabilityTheory.tendsto_condCdfRat_atBot

added theorem ProbabilityTheory.tendsto_condCdfRat_atTop

added theorem ProbabilityTheory.tendsto_condCdf_atBot

added theorem ProbabilityTheory.tendsto_condCdf_atTop

added theorem ProbabilityTheory.tendsto_lintegral_preCdf_atBot

added theorem ProbabilityTheory.tendsto_lintegral_preCdf_atTop

added theorem ProbabilityTheory.tendsto_preCdf_atBot_zero

added theorem ProbabilityTheory.tendsto_preCdf_atTop_one

added theorem ProbabilityTheory.withDensity_preCdf

added theorem Real.iInter_Iic_rat

added theorem Real.iUnion_Iic_rat

added theorem atBot_le_nhds_bot

added theorem atTop_le_nhds_top

added theorem isPiSystem_Ici

added theorem isPiSystem_Iic

added theorem lintegral_iInf_directed_of_measurable

added theorem prod_iInter

added theorem tendsto_of_antitone