Commit 2022-08-09 17:00 a150b69f

View on Github →

chore(probability/*): change to probability notation in the probability folder (#15933) This PR makes two notational changes in the probability folder: α changed to Ω and x of type α to ω.

Estimated changes

Modified src/probability/cond_count.lean

modified def probability_theory.cond_count

modified theorem probability_theory.cond_count_add_compl_eq

modified theorem probability_theory.cond_count_compl

modified theorem probability_theory.cond_count_empty

modified theorem probability_theory.cond_count_empty_meas

modified theorem probability_theory.cond_count_is_probability_measure

modified theorem probability_theory.cond_count_singleton

modified theorem probability_theory.finite_of_cond_count_ne_zero

Modified src/probability/conditional_expectation.lean

Modified src/probability/conditional_probability.lean

modified def probability_theory.cond

modified theorem probability_theory.cond_apply

modified theorem probability_theory.cond_inter_self

Modified src/probability/density.lean

modified theorem measure_theory.has_pdf.measurable

modified theorem measure_theory.has_pdf_of_pdf_ne_zero

modified theorem measure_theory.map_eq_set_lintegral_pdf

modified theorem measure_theory.map_eq_with_density_pdf

modified theorem measure_theory.measurable_of_pdf_ne_zero

modified theorem measure_theory.measurable_pdf

modified theorem measure_theory.pdf.ae_lt_top

modified theorem measure_theory.pdf.has_pdf_iff

modified theorem measure_theory.pdf.has_pdf_iff_of_measurable

modified theorem measure_theory.pdf.have_lebesgue_decomposition_of_has_pdf

modified theorem measure_theory.pdf.integrable_iff_integrable_mul_pdf

modified theorem measure_theory.pdf.is_uniform.has_pdf

modified theorem measure_theory.pdf.is_uniform.is_probability_measure

modified theorem measure_theory.pdf.is_uniform.measure_preimage

modified theorem measure_theory.pdf.is_uniform.pdf_to_real_ae_eq

modified def measure_theory.pdf.is_uniform

modified theorem measure_theory.pdf.lintegral_eq_measure_univ

modified theorem measure_theory.pdf.map_absolutely_continuous

modified theorem measure_theory.pdf.of_real_to_real_ae_eq

modified theorem measure_theory.pdf.quasi_measure_preserving_has_pdf

modified theorem measure_theory.pdf.to_quasi_measure_preserving

modified def measure_theory.pdf

modified theorem measure_theory.pdf_eq_zero_of_not_measurable

modified theorem measure_theory.pdf_undef

Modified src/probability/hitting_time.lean

modified theorem measure_theory.hitting_bot_le_iff

modified theorem measure_theory.hitting_eq_Inf

modified theorem measure_theory.hitting_le

modified theorem measure_theory.hitting_le_of_mem

modified theorem measure_theory.hitting_mem_Icc

modified theorem measure_theory.hitting_mem_set

modified theorem measure_theory.hitting_of_lt

modified theorem measure_theory.le_hitting

modified theorem measure_theory.le_hitting_of_exists

Modified src/probability/independence.lean

modified theorem probability_theory.Indep.Indep_sets

modified theorem probability_theory.Indep.indep

modified def probability_theory.Indep

modified theorem probability_theory.Indep_fun.indep_fun

modified def probability_theory.Indep_fun

modified def probability_theory.Indep_set

modified theorem probability_theory.Indep_sets.Indep

modified theorem probability_theory.Indep_sets.Indep_aux

modified theorem probability_theory.Indep_sets.indep_sets

modified theorem probability_theory.Indep_sets.pi_Union_Inter_singleton

modified def probability_theory.Indep_sets

modified theorem probability_theory.indep.indep_sets

modified theorem probability_theory.indep.symm

modified def probability_theory.indep

modified theorem probability_theory.indep_fun.ae_eq

modified def probability_theory.indep_fun

modified theorem probability_theory.indep_of_indep_of_le_left

modified theorem probability_theory.indep_of_indep_of_le_right

modified def probability_theory.indep_set

modified theorem probability_theory.indep_sets.Inter

modified theorem probability_theory.indep_sets.Union

modified theorem probability_theory.indep_sets.indep

modified theorem probability_theory.indep_sets.inter

modified theorem probability_theory.indep_sets.symm

modified theorem probability_theory.indep_sets.union

modified theorem probability_theory.indep_sets.union_iff

modified def probability_theory.indep_sets

modified theorem probability_theory.indep_sets_of_indep_sets_of_le_left

modified theorem probability_theory.indep_sets_of_indep_sets_of_le_right

modified theorem probability_theory.indep_sets_singleton_iff

Modified src/probability/integration.lean

modified theorem probability_theory.indep_fun.integrable_mul

modified theorem probability_theory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator

Modified src/probability/martingale.lean

modified def measure_theory.martingale

modified theorem measure_theory.martingale_condexp

modified theorem measure_theory.martingale_const

modified theorem measure_theory.martingale_zero

modified theorem measure_theory.submartingale.integrable_stopped_value

modified theorem measure_theory.submartingale.set_integral_le

modified theorem measure_theory.submartingale.smul_nonneg

modified theorem measure_theory.submartingale.smul_nonpos

modified theorem measure_theory.submartingale.sum_mul_sub'

modified theorem measure_theory.submartingale.sum_mul_sub

modified def measure_theory.submartingale

modified theorem measure_theory.submartingale_iff_condexp_sub_nonneg

modified theorem measure_theory.supermartingale.set_integral_le

modified theorem measure_theory.supermartingale.smul_nonneg

modified theorem measure_theory.supermartingale.smul_nonpos

modified def measure_theory.supermartingale

Modified src/probability/stopping.lean

modified def measure_theory.adapted

modified theorem measure_theory.adapted_zero

modified theorem measure_theory.filtration.adapted_natural

modified def measure_theory.filtration.const

modified theorem measure_theory.filtration.const_apply

modified def measure_theory.filtration.natural

modified structure measure_theory.filtration

modified theorem measure_theory.is_stopping_time.le_measurable_space_of_const_le

modified theorem measure_theory.is_stopping_time.measurable_set_inter_eq_iff

modified theorem measure_theory.is_stopping_time.measurable_set_min_const_iff

modified theorem measure_theory.is_stopping_time.measurable_set_min_iff

modified theorem measure_theory.is_stopping_time.measurable_space_le

modified theorem measure_theory.is_stopping_time.measurable_space_le_of_le_const

modified def measure_theory.is_stopping_time

modified theorem measure_theory.measurable_set_of_filtration

modified def measure_theory.prog_measurable

modified def measure_theory.stopped_process

modified theorem measure_theory.stopped_process_eq_of_ge

modified theorem measure_theory.stopped_process_eq_of_le

modified def measure_theory.stopped_value

modified theorem measure_theory.stopped_value_const

modified theorem measure_theory.stopped_value_eq

modified theorem measure_theory.stopped_value_piecewise_const'

modified theorem measure_theory.stopped_value_piecewise_const

modified theorem measure_theory.stopped_value_sub_eq_sum'

Modified src/probability/variance.lean