Commit 2024-08-12 04:09 267c64be
View on Github →feat (MeasureTheory-Probabilty): Congruence lemma for double integrals. (#15460)
- Add
ProbabilityTheory.Kernel.integral_congr_ae₂
andMeasureTheory.integral_congr_ae₂
.
feat (MeasureTheory-Probabilty): Congruence lemma for double integrals. (#15460)
ProbabilityTheory.Kernel.integral_congr_ae₂
and MeasureTheory.integral_congr_ae₂
.