Commit 2025-06-17 11:28 2b6e3d70

View on Github →

chore: add a pointwise version of setLIntegral_congr_fun, append ae to the current version (#25962) In this way, we match the API for the Bochner integral. And we simplify most calls to the previous version, which were using ae_of_all 90% of the times.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

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

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

Modified Mathlib/MeasureTheory/Integral/Average.lean

modified theorem MeasureTheory.setLAverage_congr_fun

added theorem MeasureTheory.setLAverage_congr_fun_ae

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

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

added theorem MeasureTheory.setLIntegral_congr_fun_ae

added theorem MeasureTheory.setLIntegral_eq_zero

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

Modified Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean

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

Modified Mathlib/Probability/Distributions/Exponential.lean

Modified Mathlib/Probability/Distributions/Gamma.lean

Modified Mathlib/Probability/Distributions/Pareto.lean

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

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

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

Modified Mathlib/Probability/Kernel/Posterior.lean

Modified Mathlib/Probability/Kernel/RadonNikodym.lean