Commit 2024-04-18 02:39 f4b4298b

View on Github →

chore: replace set_integral with setIntegral (#12215) Done with a global search and replace, and then (to fix the #align lines), replace (#align \S*)setIntegral with $1set_integral.

Estimated changes

Modified Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

Modified Mathlib/Analysis/Convex/Integral.lean

added theorem ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const

deleted theorem ae_eq_const_or_norm_set_integral_lt_of_norm_le_const

Modified Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/MellinTransform.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Modified Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean

Modified Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

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

added theorem MeasureTheory.setIntegral_prod

added theorem MeasureTheory.setIntegral_prod_mul

deleted theorem MeasureTheory.set_integral_prod

deleted theorem MeasureTheory.set_integral_prod_mul

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

added theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv'

added theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv

added theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity'

added theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_eq_withDensity

added theorem MeasureTheory.Measure.setIntegral_toReal_rnDeriv_le

deleted theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv'

deleted theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv

deleted theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_eq_withDensity'

deleted theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_eq_withDensity

deleted theorem MeasureTheory.Measure.set_integral_toReal_rnDeriv_le

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq

deleted theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_set_integral_eq

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero

deleted theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_set_integral_eq_zero

added theorem MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_setIntegral_nonneg

deleted theorem MeasureTheory.AEFinStronglyMeasurable.ae_nonneg_of_forall_set_integral_nonneg

added theorem MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq

deleted theorem MeasureTheory.Integrable.ae_eq_of_forall_set_integral_eq

added theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero

deleted theorem MeasureTheory.Integrable.ae_eq_zero_of_forall_set_integral_eq_zero

added theorem MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq

deleted theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq

added theorem MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero

deleted theorem MeasureTheory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero

added theorem MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite

deleted theorem MeasureTheory.ae_eq_of_forall_set_integral_eq_of_sigmaFinite

added theorem MeasureTheory.ae_eq_restrict_of_forall_setIntegral_eq

deleted theorem MeasureTheory.ae_eq_restrict_of_forall_set_integral_eq

added theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_finStronglyMeasurable_trim

added theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite

added theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero

added theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero'

added theorem MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero

deleted theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_eq_of_finStronglyMeasurable_trim

deleted theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_eq_of_sigmaFinite

deleted theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_isClosed_eq_zero

deleted theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_isCompact_eq_zero'

deleted theorem MeasureTheory.ae_eq_zero_of_forall_set_integral_isCompact_eq_zero

added theorem MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero

added theorem MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real

deleted theorem MeasureTheory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero

deleted theorem MeasureTheory.ae_eq_zero_restrict_of_forall_set_integral_eq_zero_real

added theorem MeasureTheory.ae_le_of_forall_setIntegral_le

deleted theorem MeasureTheory.ae_le_of_forall_set_integral_le

added theorem MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg

added theorem MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite

added theorem MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_stronglyMeasurable

deleted theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg

deleted theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_sigmaFinite

deleted theorem MeasureTheory.ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable

added theorem MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg

added theorem MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter

deleted theorem MeasureTheory.ae_nonneg_restrict_of_forall_set_integral_nonneg

deleted theorem MeasureTheory.ae_nonneg_restrict_of_forall_set_integral_nonneg_inter

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

added theorem MeasureTheory.ae_eq_condexp_of_forall_setIntegral_eq

deleted theorem MeasureTheory.ae_eq_condexp_of_forall_set_integral_eq

added theorem MeasureTheory.setIntegral_condexp

deleted theorem MeasureTheory.set_integral_condexp

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

added theorem MeasureTheory.setIntegral_condexpInd

added theorem MeasureTheory.setIntegral_condexpL1

added theorem MeasureTheory.setIntegral_condexpL1CLM

added theorem MeasureTheory.setIntegral_condexpL1CLM_of_measure_ne_top

deleted theorem MeasureTheory.set_integral_condexpInd

deleted theorem MeasureTheory.set_integral_condexpL1

deleted theorem MeasureTheory.set_integral_condexpL1CLM

deleted theorem MeasureTheory.set_integral_condexpL1CLM_of_measure_ne_top

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

added theorem MeasureTheory.setIntegral_condexpIndSMul

added theorem MeasureTheory.setIntegral_condexpL2_indicator

deleted theorem MeasureTheory.set_integral_condexpIndSMul

deleted theorem MeasureTheory.set_integral_condexpL2_indicator

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

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

added theorem MeasureTheory.setIntegral_abs_condexp_le

deleted theorem MeasureTheory.set_integral_abs_condexp_le

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

added theorem MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq'

deleted theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq'

added theorem MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero'

deleted theorem MeasureTheory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero'

added theorem MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'

deleted theorem MeasureTheory.ae_eq_of_forall_set_integral_eq_of_sigmaFinite'

added theorem MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero

deleted theorem MeasureTheory.lpMeas.ae_eq_zero_of_forall_set_integral_eq_zero

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/L2Space.lean

added theorem MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral

deleted theorem MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral

added theorem MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner

deleted theorem MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

added theorem MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum'

added theorem MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum

deleted theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum'

deleted theorem MeasureTheory.IsFundamentalDomain.set_integral_eq_tsum

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero

deleted theorem MeasureTheory.HasFiniteIntegral.tendsto_set_integral_nhds_zero

added theorem MeasureTheory.Integrable.tendsto_setIntegral_nhds_zero

deleted theorem MeasureTheory.Integrable.tendsto_set_integral_nhds_zero

added theorem MeasureTheory.setIntegral_dirac'

added theorem MeasureTheory.setIntegral_dirac

deleted theorem MeasureTheory.set_integral_dirac'

deleted theorem MeasureTheory.set_integral_dirac

added theorem MeasureTheory.tendsto_setIntegral_of_L1'

added theorem MeasureTheory.tendsto_setIntegral_of_L1

deleted theorem MeasureTheory.tendsto_set_integral_of_L1'

deleted theorem MeasureTheory.tendsto_set_integral_of_L1

Modified Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

added theorem Antitone.tendsto_setIntegral

deleted theorem Antitone.tendsto_set_integral

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/Gamma.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/PeakFunction.lean

added theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto

added theorem tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux

added theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn

added theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn

added theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos

deleted theorem tendsto_set_integral_peak_smul_of_integrableOn_of_tendsto

deleted theorem tendsto_set_integral_peak_smul_of_integrableOn_of_tendsto_aux

deleted theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn

deleted theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn

deleted theorem tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem ClosedEmbedding.setIntegral_map

deleted theorem ClosedEmbedding.set_integral_map

added theorem ContinuousLinearMap.setIntegral_compLp

deleted theorem ContinuousLinearMap.set_integral_compLp

added theorem MeasurableEmbedding.setIntegral_map

deleted theorem MeasurableEmbedding.set_integral_map

added theorem MeasureTheory.MeasurePreserving.setIntegral_image_emb

added theorem MeasureTheory.MeasurePreserving.setIntegral_preimage_emb

deleted theorem MeasureTheory.MeasurePreserving.set_integral_image_emb

deleted theorem MeasureTheory.MeasurePreserving.set_integral_preimage_emb

added theorem MeasureTheory.continuous_setIntegral

deleted theorem MeasureTheory.continuous_set_integral

added theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const'

added theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const

added theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae''

added theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'

added theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae

deleted theorem MeasureTheory.norm_set_integral_le_of_norm_le_const'

deleted theorem MeasureTheory.norm_set_integral_le_of_norm_le_const

deleted theorem MeasureTheory.norm_set_integral_le_of_norm_le_const_ae''

deleted theorem MeasureTheory.norm_set_integral_le_of_norm_le_const_ae'

deleted theorem MeasureTheory.norm_set_integral_le_of_norm_le_const_ae

added theorem MeasureTheory.ofReal_setIntegral_one

added theorem MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top

deleted theorem MeasureTheory.ofReal_set_integral_one

deleted theorem MeasureTheory.ofReal_set_integral_one_of_measure_ne_top

added theorem MeasureTheory.setIntegral_congr

added theorem MeasureTheory.setIntegral_congr_ae

added theorem MeasureTheory.setIntegral_congr_ae₀

added theorem MeasureTheory.setIntegral_congr_set_ae

added theorem MeasureTheory.setIntegral_congr₀

added theorem MeasureTheory.setIntegral_const

added theorem MeasureTheory.setIntegral_eq_integral_of_ae_compl_eq_zero

added theorem MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero

added theorem MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero

added theorem MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux

added theorem MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero

added theorem MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae

added theorem MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero

added theorem MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero

added theorem MeasureTheory.setIntegral_ge_of_const_le

added theorem MeasureTheory.setIntegral_gt_gt

added theorem MeasureTheory.setIntegral_indicator

added theorem MeasureTheory.setIntegral_indicatorConstLp

added theorem MeasureTheory.setIntegral_le_integral

added theorem MeasureTheory.setIntegral_le_nonneg

added theorem MeasureTheory.setIntegral_map

added theorem MeasureTheory.setIntegral_map_equiv

added theorem MeasureTheory.setIntegral_mono

added theorem MeasureTheory.setIntegral_mono_ae

added theorem MeasureTheory.setIntegral_mono_ae_restrict

added theorem MeasureTheory.setIntegral_mono_on

added theorem MeasureTheory.setIntegral_mono_on_ae

added theorem MeasureTheory.setIntegral_mono_set

added theorem MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos

added theorem MeasureTheory.setIntegral_nonneg

added theorem MeasureTheory.setIntegral_nonneg_ae

added theorem MeasureTheory.setIntegral_nonneg_of_ae

added theorem MeasureTheory.setIntegral_nonneg_of_ae_restrict

added theorem MeasureTheory.setIntegral_nonpos

added theorem MeasureTheory.setIntegral_nonpos_ae

added theorem MeasureTheory.setIntegral_nonpos_le

added theorem MeasureTheory.setIntegral_nonpos_of_ae

added theorem MeasureTheory.setIntegral_nonpos_of_ae_restrict

added theorem MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae

added theorem MeasureTheory.setIntegral_trim

deleted theorem MeasureTheory.set_integral_congr

deleted theorem MeasureTheory.set_integral_congr_ae

deleted theorem MeasureTheory.set_integral_congr_ae₀

deleted theorem MeasureTheory.set_integral_congr_set_ae

deleted theorem MeasureTheory.set_integral_congr₀

deleted theorem MeasureTheory.set_integral_const

deleted theorem MeasureTheory.set_integral_eq_integral_of_ae_compl_eq_zero

deleted theorem MeasureTheory.set_integral_eq_integral_of_forall_compl_eq_zero

deleted theorem MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero

deleted theorem MeasureTheory.set_integral_eq_of_subset_of_ae_diff_eq_zero_aux

deleted theorem MeasureTheory.set_integral_eq_of_subset_of_forall_diff_eq_zero

deleted theorem MeasureTheory.set_integral_eq_zero_iff_of_nonneg_ae

deleted theorem MeasureTheory.set_integral_eq_zero_of_ae_eq_zero

deleted theorem MeasureTheory.set_integral_eq_zero_of_forall_eq_zero

deleted theorem MeasureTheory.set_integral_ge_of_const_le

deleted theorem MeasureTheory.set_integral_gt_gt

deleted theorem MeasureTheory.set_integral_indicator

deleted theorem MeasureTheory.set_integral_indicatorConstLp

deleted theorem MeasureTheory.set_integral_le_integral

deleted theorem MeasureTheory.set_integral_le_nonneg

deleted theorem MeasureTheory.set_integral_map

deleted theorem MeasureTheory.set_integral_map_equiv

deleted theorem MeasureTheory.set_integral_mono

deleted theorem MeasureTheory.set_integral_mono_ae

deleted theorem MeasureTheory.set_integral_mono_ae_restrict

deleted theorem MeasureTheory.set_integral_mono_on

deleted theorem MeasureTheory.set_integral_mono_on_ae

deleted theorem MeasureTheory.set_integral_mono_set

deleted theorem MeasureTheory.set_integral_neg_eq_set_integral_nonpos

deleted theorem MeasureTheory.set_integral_nonneg

deleted theorem MeasureTheory.set_integral_nonneg_ae

deleted theorem MeasureTheory.set_integral_nonneg_of_ae

deleted theorem MeasureTheory.set_integral_nonneg_of_ae_restrict

deleted theorem MeasureTheory.set_integral_nonpos

deleted theorem MeasureTheory.set_integral_nonpos_ae

deleted theorem MeasureTheory.set_integral_nonpos_le

deleted theorem MeasureTheory.set_integral_nonpos_of_ae

deleted theorem MeasureTheory.set_integral_nonpos_of_ae_restrict

deleted theorem MeasureTheory.set_integral_pos_iff_support_of_nonneg_ae

deleted theorem MeasureTheory.set_integral_trim

added theorem MeasureTheory.tendsto_setIntegral_of_antitone

added theorem MeasureTheory.tendsto_setIntegral_of_monotone

deleted theorem MeasureTheory.tendsto_set_integral_of_antitone

deleted theorem MeasureTheory.tendsto_set_integral_of_monotone

added theorem setIntegral_re_add_im

added theorem setIntegral_withDensity_eq_setIntegral_smul

added theorem setIntegral_withDensity_eq_setIntegral_smul₀'

added theorem setIntegral_withDensity_eq_setIntegral_smul₀

deleted theorem set_integral_re_add_im

deleted theorem set_integral_withDensity_eq_set_integral_smul

deleted theorem set_integral_withDensity_eq_set_integral_smul₀'

deleted theorem set_integral_withDensity_eq_set_integral_smul₀

Modified Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Modified Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean

added theorem MeasureTheory.Measure.setIntegral_comp_smul

added theorem MeasureTheory.Measure.setIntegral_comp_smul_of_pos

deleted theorem MeasureTheory.Measure.set_integral_comp_smul

deleted theorem MeasureTheory.Measure.set_integral_comp_smul_of_pos

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

added theorem MeasureTheory.setIntegral_tilted'

added theorem MeasureTheory.setIntegral_tilted

deleted theorem MeasureTheory.set_integral_tilted'

deleted theorem MeasureTheory.set_integral_tilted

Modified Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean

Modified Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

Modified Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean

Modified Mathlib/NumberTheory/ZetaFunction.lean

Modified Mathlib/Probability/ConditionalExpectation.lean

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.kernel.setIntegral_const

added theorem ProbabilityTheory.kernel.setIntegral_deterministic'

added theorem ProbabilityTheory.kernel.setIntegral_deterministic

added theorem ProbabilityTheory.kernel.setIntegral_piecewise

added theorem ProbabilityTheory.kernel.setIntegral_restrict

deleted theorem ProbabilityTheory.kernel.set_integral_const

deleted theorem ProbabilityTheory.kernel.set_integral_deterministic'

deleted theorem ProbabilityTheory.kernel.set_integral_deterministic

deleted theorem ProbabilityTheory.kernel.set_integral_piecewise

deleted theorem ProbabilityTheory.kernel.set_integral_restrict

Modified Mathlib/Probability/Kernel/CondDistrib.lean

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

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

added theorem ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt

deleted theorem ProbabilityTheory.IsRatCondKernelCDFAux.set_integral_iInf_rat_gt

added theorem ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat

added theorem ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat

deleted theorem ProbabilityTheory.set_integral_stieltjesOfMeasurableRat

deleted theorem ProbabilityTheory.set_integral_stieltjesOfMeasurableRat_rat

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

added theorem ProbabilityTheory.setIntegral_condCDF

added theorem ProbabilityTheory.setIntegral_preCDF_fst

deleted theorem ProbabilityTheory.set_integral_condCDF

deleted theorem ProbabilityTheory.set_integral_preCDF_fst

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

added theorem ProbabilityTheory.kernel.setIntegral_density

added theorem ProbabilityTheory.kernel.setIntegral_densityProcess

added theorem ProbabilityTheory.kernel.setIntegral_densityProcess_of_le

added theorem ProbabilityTheory.kernel.setIntegral_densityProcess_of_mem

added theorem ProbabilityTheory.kernel.setIntegral_density_of_measurableSet

deleted theorem ProbabilityTheory.kernel.set_integral_density

deleted theorem ProbabilityTheory.kernel.set_integral_densityProcess

deleted theorem ProbabilityTheory.kernel.set_integral_densityProcess_of_le

deleted theorem ProbabilityTheory.kernel.set_integral_densityProcess_of_mem

deleted theorem ProbabilityTheory.kernel.set_integral_density_of_measurableSet

added theorem ProbabilityTheory.kernel.tendsto_setIntegral_densityProcess

deleted theorem ProbabilityTheory.kernel.tendsto_set_integral_densityProcess

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

added theorem MeasureTheory.Measure.setIntegral_condKernel

added theorem MeasureTheory.Measure.setIntegral_condKernel_univ_left

added theorem MeasureTheory.Measure.setIntegral_condKernel_univ_right

deleted theorem MeasureTheory.Measure.set_integral_condKernel

deleted theorem MeasureTheory.Measure.set_integral_condKernel_univ_left

deleted theorem MeasureTheory.Measure.set_integral_condKernel_univ_right

added theorem ProbabilityTheory.setIntegral_condKernel

added theorem ProbabilityTheory.setIntegral_condKernel_univ_left

added theorem ProbabilityTheory.setIntegral_condKernel_univ_right

deleted theorem ProbabilityTheory.set_integral_condKernel

deleted theorem ProbabilityTheory.set_integral_condKernel_univ_left

deleted theorem ProbabilityTheory.set_integral_condKernel_univ_right

Modified Mathlib/Probability/Kernel/IntegralCompProd.lean

added theorem ProbabilityTheory.setIntegral_compProd

added theorem ProbabilityTheory.setIntegral_compProd_univ_left

added theorem ProbabilityTheory.setIntegral_compProd_univ_right

deleted theorem ProbabilityTheory.set_integral_compProd

deleted theorem ProbabilityTheory.set_integral_compProd_univ_left

deleted theorem ProbabilityTheory.set_integral_compProd_univ_right

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

added theorem MeasureTheory.Measure.setIntegral_compProd

deleted theorem MeasureTheory.Measure.set_integral_compProd

Modified Mathlib/Probability/Martingale/Basic.lean

added theorem MeasureTheory.Martingale.setIntegral_eq

deleted theorem MeasureTheory.Martingale.set_integral_eq

added theorem MeasureTheory.Submartingale.setIntegral_le

deleted theorem MeasureTheory.Submartingale.set_integral_le

added theorem MeasureTheory.Supermartingale.setIntegral_le

deleted theorem MeasureTheory.Supermartingale.set_integral_le

added theorem MeasureTheory.martingale_of_setIntegral_eq_succ

deleted theorem MeasureTheory.martingale_of_set_integral_eq_succ

added theorem MeasureTheory.submartingale_of_setIntegral_le

added theorem MeasureTheory.submartingale_of_setIntegral_le_succ

deleted theorem MeasureTheory.submartingale_of_set_integral_le

deleted theorem MeasureTheory.submartingale_of_set_integral_le_succ

added theorem MeasureTheory.supermartingale_of_setIntegral_succ_le

deleted theorem MeasureTheory.supermartingale_of_set_integral_succ_le

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Probability/Martingale/OptionalStopping.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/Probability/Moments.lean

Modified Mathlib/Probability/StrongLaw.lean

Modified scripts/style-exceptions.txt