Commit 2024-06-29 15:21 85d5f96e

View on Github →

chore: rename set_lintegral to setLIntegral throughout mathlib (#14260) The old naming is a remnant of Lean 3. The change has already been made for the Bochner integral, from set_integral to setIntegral.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Modified Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

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

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.Measure.setLIntegral_rnDeriv'

added theorem MeasureTheory.Measure.setLIntegral_rnDeriv

added theorem MeasureTheory.Measure.setLIntegral_rnDeriv_le

deleted theorem MeasureTheory.Measure.set_lintegral_rnDeriv'

deleted theorem MeasureTheory.Measure.set_lintegral_rnDeriv

deleted theorem MeasureTheory.Measure.set_lintegral_rnDeriv_le

added theorem MeasureTheory.setLIntegral_rnDeriv_mul

deleted theorem MeasureTheory.set_lintegral_rnDeriv_mul

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

added theorem MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq

deleted theorem MeasureTheory.AEMeasurable.ae_eq_of_forall_set_lintegral_eq

added theorem MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite

added theorem MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀

deleted theorem MeasureTheory.ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite

deleted theorem MeasureTheory.ae_eq_of_forall_set_lintegral_eq_of_sigmaFinite₀

added theorem MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite

added theorem MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀

deleted theorem MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite

deleted theorem MeasureTheory.ae_le_of_forall_set_lintegral_le_of_sigmaFinite₀

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

added theorem MeasureTheory.setLIntegral_nnnorm_condexpIndSMul_le

added theorem MeasureTheory.setLIntegral_nnnorm_condexpL2_indicator_le

deleted theorem MeasureTheory.set_lintegral_nnnorm_condexpIndSMul_le

deleted theorem MeasureTheory.set_lintegral_nnnorm_condexpL2_indicator_le

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

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

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

added theorem MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum'

added theorem MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum

deleted theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum'

deleted theorem MeasureTheory.IsFundamentalDomain.set_lintegral_eq_tsum

Modified Mathlib/MeasureTheory/Group/Prod.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

added theorem MeasureTheory.IntegrableOn.setLIntegral_lt_top

deleted theorem MeasureTheory.IntegrableOn.set_lintegral_lt_top

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_emb

added theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage

added theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb

deleted theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_emb

deleted theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage

deleted theorem MeasureTheory.MeasurePreserving.set_lintegral_comp_preimage_emb

added theorem MeasureTheory.exists_pos_setLIntegral_lt_of_measure_lt

deleted theorem MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt

added theorem MeasureTheory.setLIntegral_congr

added theorem MeasureTheory.setLIntegral_congr_fun

added theorem MeasureTheory.setLIntegral_const

added theorem MeasureTheory.setLIntegral_const_lt_top

added theorem MeasureTheory.setLIntegral_dirac'

added theorem MeasureTheory.setLIntegral_dirac

added theorem MeasureTheory.setLIntegral_empty

added theorem MeasureTheory.setLIntegral_eq_const

added theorem MeasureTheory.setLIntegral_le_lintegral

added theorem MeasureTheory.setLIntegral_lt_top_of_bddAbove

added theorem MeasureTheory.setLIntegral_lt_top_of_isCompact

added theorem MeasureTheory.setLIntegral_map

added theorem MeasureTheory.setLIntegral_max

added theorem MeasureTheory.setLIntegral_measure_zero

added theorem MeasureTheory.setLIntegral_mono'

added theorem MeasureTheory.setLIntegral_mono

added theorem MeasureTheory.setLIntegral_mono_ae'

added theorem MeasureTheory.setLIntegral_mono_ae

added theorem MeasureTheory.setLIntegral_one

added theorem MeasureTheory.setLIntegral_smul_measure

added theorem MeasureTheory.setLIntegral_strict_mono

added theorem MeasureTheory.setLIntegral_subtype

added theorem MeasureTheory.setLIntegral_univ

deleted theorem MeasureTheory.set_lintegral_congr

deleted theorem MeasureTheory.set_lintegral_congr_fun

deleted theorem MeasureTheory.set_lintegral_const

deleted theorem MeasureTheory.set_lintegral_const_lt_top

deleted theorem MeasureTheory.set_lintegral_dirac'

deleted theorem MeasureTheory.set_lintegral_dirac

deleted theorem MeasureTheory.set_lintegral_empty

deleted theorem MeasureTheory.set_lintegral_eq_const

deleted theorem MeasureTheory.set_lintegral_le_lintegral

deleted theorem MeasureTheory.set_lintegral_lt_top_of_bddAbove

deleted theorem MeasureTheory.set_lintegral_lt_top_of_isCompact

deleted theorem MeasureTheory.set_lintegral_map

deleted theorem MeasureTheory.set_lintegral_max

deleted theorem MeasureTheory.set_lintegral_measure_zero

deleted theorem MeasureTheory.set_lintegral_mono'

deleted theorem MeasureTheory.set_lintegral_mono

deleted theorem MeasureTheory.set_lintegral_mono_ae'

deleted theorem MeasureTheory.set_lintegral_mono_ae

deleted theorem MeasureTheory.set_lintegral_one

deleted theorem MeasureTheory.set_lintegral_smul_measure

deleted theorem MeasureTheory.set_lintegral_strict_mono

deleted theorem MeasureTheory.set_lintegral_subtype

deleted theorem MeasureTheory.set_lintegral_univ

added theorem MeasureTheory.tendsto_setLIntegral_zero

deleted theorem MeasureTheory.tendsto_set_lintegral_zero

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

added theorem MeasureTheory.setLIntegral_tilted'

added theorem MeasureTheory.setLIntegral_tilted

deleted theorem MeasureTheory.set_lintegral_tilted'

deleted theorem MeasureTheory.set_lintegral_tilted

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

added theorem MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀'

added theorem MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀

added theorem MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul

added theorem MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable

added theorem MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀'

added theorem MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_lintegral_mul₀'

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_lintegral_mul₀

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀'

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀

Modified Mathlib/MeasureTheory/Measure/WithDensityFinite.lean

Modified Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean

Modified Mathlib/Probability/Density.lean

added theorem MeasureTheory.map_eq_setLIntegral_pdf

deleted theorem MeasureTheory.map_eq_set_lintegral_pdf

added theorem MeasureTheory.setLIntegral_pdf_le_map

deleted theorem MeasureTheory.set_lintegral_pdf_le_map

Modified Mathlib/Probability/Distributions/Exponential.lean

Modified Mathlib/Probability/Distributions/Gamma.lean

Modified Mathlib/Probability/Distributions/Uniform.lean

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.kernel.setLIntegral_const

added theorem ProbabilityTheory.kernel.setLIntegral_deterministic'

added theorem ProbabilityTheory.kernel.setLIntegral_deterministic

added theorem ProbabilityTheory.kernel.setLIntegral_piecewise

added theorem ProbabilityTheory.kernel.setLIntegral_restrict

deleted theorem ProbabilityTheory.kernel.set_lintegral_const

deleted theorem ProbabilityTheory.kernel.set_lintegral_deterministic'

deleted theorem ProbabilityTheory.kernel.set_lintegral_deterministic

deleted theorem ProbabilityTheory.kernel.set_lintegral_piecewise

deleted theorem ProbabilityTheory.kernel.set_lintegral_restrict

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.kernel.setLIntegral_compProd

added theorem ProbabilityTheory.kernel.setLIntegral_compProd_univ_left

added theorem ProbabilityTheory.kernel.setLIntegral_compProd_univ_right

deleted theorem ProbabilityTheory.kernel.set_lintegral_compProd

deleted theorem ProbabilityTheory.kernel.set_lintegral_compProd_univ_left

deleted theorem ProbabilityTheory.kernel.set_lintegral_compProd_univ_right

Modified Mathlib/Probability/Kernel/CondDistrib.lean

added theorem ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet

added theorem ProbabilityTheory.setLIntegral_preimage_condDistrib

deleted theorem ProbabilityTheory.set_lintegral_condDistrib_of_measurableSet

deleted theorem ProbabilityTheory.set_lintegral_preimage_condDistrib

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

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

added theorem ProbabilityTheory.IsCondKernelCDF.setLIntegral

deleted theorem ProbabilityTheory.IsCondKernelCDF.set_lintegral

added theorem ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat

added theorem ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat

added theorem ProbabilityTheory.setLIntegral_toKernel_Iic

added theorem ProbabilityTheory.setLIntegral_toKernel_prod

added theorem ProbabilityTheory.setLIntegral_toKernel_univ

deleted theorem ProbabilityTheory.set_lintegral_stieltjesOfMeasurableRat

deleted theorem ProbabilityTheory.set_lintegral_stieltjesOfMeasurableRat_rat

deleted theorem ProbabilityTheory.set_lintegral_toKernel_Iic

deleted theorem ProbabilityTheory.set_lintegral_toKernel_prod

deleted theorem ProbabilityTheory.set_lintegral_toKernel_univ

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

added theorem ProbabilityTheory.setLIntegral_condCDF

added theorem ProbabilityTheory.setLIntegral_preCDF_fst

deleted theorem ProbabilityTheory.set_lintegral_condCDF

deleted theorem ProbabilityTheory.set_lintegral_preCDF_fst

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

added theorem ProbabilityTheory.kernel.setLIntegral_density

deleted theorem ProbabilityTheory.kernel.set_lintegral_density

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

added theorem MeasureTheory.Measure.setLIntegral_condKernel

added theorem MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod

added theorem MeasureTheory.Measure.setLIntegral_condKernel_univ_left

added theorem MeasureTheory.Measure.setLIntegral_condKernel_univ_right

deleted theorem MeasureTheory.Measure.set_lintegral_condKernel

deleted theorem MeasureTheory.Measure.set_lintegral_condKernel_eq_measure_prod

deleted theorem MeasureTheory.Measure.set_lintegral_condKernel_univ_left

deleted theorem MeasureTheory.Measure.set_lintegral_condKernel_univ_right

added theorem ProbabilityTheory.setLIntegral_condKernel

added theorem ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod

added theorem ProbabilityTheory.setLIntegral_condKernel_univ_left

added theorem ProbabilityTheory.setLIntegral_condKernel_univ_right

deleted theorem ProbabilityTheory.set_lintegral_condKernel

deleted theorem ProbabilityTheory.set_lintegral_condKernel_eq_measure_prod

deleted theorem ProbabilityTheory.set_lintegral_condKernel_univ_left

deleted theorem ProbabilityTheory.set_lintegral_condKernel_univ_right

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

Modified Mathlib/Probability/Kernel/MeasurableIntegral.lean

added theorem Measurable.setLIntegral_kernel

added theorem Measurable.setLIntegral_kernel_prod_left

added theorem Measurable.setLIntegral_kernel_prod_right

deleted theorem Measurable.set_lintegral_kernel

deleted theorem Measurable.set_lintegral_kernel_prod_left

deleted theorem Measurable.set_lintegral_kernel_prod_right

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

added theorem MeasureTheory.Measure.setLIntegral_compProd

deleted theorem MeasureTheory.Measure.set_lintegral_compProd

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

added theorem ProbabilityTheory.kernel.setLIntegral_rnDerivAux

deleted theorem ProbabilityTheory.kernel.set_lintegral_rnDerivAux

Modified Mathlib/Probability/Kernel/WithDensity.lean