Commit 2025-03-08 05:09 bf2462cf

View on Github →

chore(MeasureTheory,Probability): rename many lemmas (#22619) Mostly prod_mk -> prodMk. Cherry picked from #22195

Estimated changes

Modified Mathlib/Analysis/Calculus/LineDeriv/Measurable.lean

Modified Mathlib/Analysis/Convex/Integral.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/Constructions/Cylinders.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

added theorem MeasureTheory.Integrable.prodMk

deleted theorem MeasureTheory.Integrable.prod_mk

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Inner.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/Group/Prod.lean

Modified Mathlib/MeasureTheory/Integral/Prod.lean

added theorem MeasureTheory.AEStronglyMeasurable.prodMk_left

deleted theorem MeasureTheory.AEStronglyMeasurable.prod_mk_left

added theorem MeasureTheory.Measure.integrable_measure_prodMk_left

deleted theorem MeasureTheory.Measure.integrable_measure_prod_mk_left

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem Measurable.prodMap

added theorem Measurable.prodMk

deleted theorem Measurable.prod_map

deleted theorem Measurable.prod_mk

added theorem measurable_prodMk_left

added theorem measurable_prodMk_right

deleted theorem measurable_prod_mk_left

deleted theorem measurable_prod_mk_right

Modified Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

added theorem MeasurableEmbedding.prodMk_left

added theorem MeasurableEmbedding.prodMk_right

deleted theorem MeasurableEmbedding.prod_mk_left

deleted theorem MeasurableEmbedding.prod_mk_right

added theorem measurableEmbedding_prodMk_left

deleted theorem measurableEmbedding_prod_mk_left

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem AEMeasurable.prodMk

deleted theorem AEMeasurable.prod_mk

Modified Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean

Modified Mathlib/MeasureTheory/Measure/Prod.lean

added theorem Measurable.map_prodMk_left

added theorem Measurable.map_prodMk_right

deleted theorem Measurable.map_prod_mk_left

deleted theorem Measurable.map_prod_mk_right

modified theorem MeasureTheory.Measure.fst_add

added theorem MeasureTheory.Measure.fst_map_prodMk

added theorem MeasureTheory.Measure.fst_map_prodMk₀

deleted theorem MeasureTheory.Measure.fst_map_prod_mk

deleted theorem MeasureTheory.Measure.fst_map_prod_mk₀

modified theorem MeasureTheory.Measure.fst_sum

modified theorem MeasureTheory.Measure.snd_add

added theorem MeasureTheory.Measure.snd_map_prodMk

added theorem MeasureTheory.Measure.snd_map_prodMk₀

deleted theorem MeasureTheory.Measure.snd_map_prod_mk

deleted theorem MeasureTheory.Measure.snd_map_prod_mk₀

modified theorem MeasureTheory.Measure.snd_sum

added theorem measurable_measure_prodMk_left

added theorem measurable_measure_prodMk_left_finite

added theorem measurable_measure_prodMk_right

deleted theorem measurable_measure_prod_mk_left

deleted theorem measurable_measure_prod_mk_left_finite

deleted theorem measurable_measure_prod_mk_right

Modified Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

Modified Mathlib/MeasureTheory/Order/Lattice.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.iIndepFun.indepFun_prodMk

added theorem ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk

deleted theorem ProbabilityTheory.iIndepFun.indepFun_prod_mk

deleted theorem ProbabilityTheory.iIndepFun.indepFun_prod_mk_prod_mk

Modified Mathlib/Probability/Independence/Conditional.lean

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prodMk_prodMk

deleted theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_mk

deleted theorem ProbabilityTheory.iCondIndepFun.condIndepFun_prod_mk_prod_mk

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk

deleted theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk

deleted theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk_prod_mk

Modified Mathlib/Probability/Kernel/CompProdEqIff.lean

Modified Mathlib/Probability/Kernel/Composition/CompProd.lean

Modified Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean

added theorem ProbabilityTheory.hasFiniteIntegral_prodMk_left

deleted theorem ProbabilityTheory.hasFiniteIntegral_prod_mk_left

added theorem ProbabilityTheory.integrable_kernel_prodMk_left

deleted theorem ProbabilityTheory.integrable_kernel_prod_mk_left

Modified Mathlib/Probability/Kernel/Composition/Lemmas.lean

Modified Mathlib/Probability/Kernel/Composition/MapComap.lean

Modified Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

Modified Mathlib/Probability/Kernel/Composition/ParallelComp.lean

Modified Mathlib/Probability/Kernel/Composition/Prod.lean

Modified Mathlib/Probability/Kernel/CondDistrib.lean

added theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk

deleted theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_mk

added theorem MeasureTheory.Integrable.comp_snd_map_prodMk

deleted theorem MeasureTheory.Integrable.comp_snd_map_prod_mk

added theorem ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff

deleted theorem ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prod_mk_iff

added theorem ProbabilityTheory.integrable_comp_snd_map_prodMk_iff

deleted theorem ProbabilityTheory.integrable_comp_snd_map_prod_mk_iff

Modified Mathlib/Probability/Kernel/Condexp.lean

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean

Modified Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

Modified Mathlib/Probability/Kernel/Disintegration/Unique.lean

Modified Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean

Modified Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean

Modified Mathlib/Probability/Kernel/MeasurableIntegral.lean

Modified Mathlib/Probability/Kernel/MeasurableLIntegral.lean

added theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'

added theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_left

added theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite

added theorem ProbabilityTheory.Kernel.measurable_kernel_prodMk_right

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left'

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left_of_finite

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_right

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

Modified Mathlib/Probability/Process/Adapted.lean

Modified Mathlib/Probability/Process/Stopping.lean