Commit 2025-04-09 02:33 e584e66c

View on Github →

chore: standardise on AES or aes in AEStronglyMeasurable (#23852) In other words, AES is treated as one letter in declaration names. The oddly-cased instances were found using the regex (AEs|AeS|Aes|aES|aEs|aeS)trongly.

Estimated changes

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

deleted theorem MeasureTheory.ae_eq_trim_iff_of_aeStronglyMeasurable'

added theorem MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable

deleted theorem MeasureTheory.isClosed_aeStronglyMeasurable'

added theorem MeasureTheory.isClosed_aestronglyMeasurable

deleted theorem MeasureTheory.isComplete_aeStronglyMeasurable'

added theorem MeasureTheory.isComplete_aestronglyMeasurable

deleted theorem MeasureTheory.lpMeas.aeStronglyMeasurable

added theorem MeasureTheory.lpMeas.aestronglyMeasurable

deleted theorem MeasureTheory.mem_lpMeasSubgroup_iff_aeStronglyMeasurable

added theorem MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable

deleted theorem MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable

added theorem MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable

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

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

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

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

deleted theorem MeasureTheory.setToFun_non_aEStronglyMeasurable

added theorem MeasureTheory.setToFun_non_aestronglyMeasurable