Commit 2025-01-23 12:20 5eb97b6c

View on Github →

chore(CondExp): golf (#20981)

  • Remove useless @
  • Remove useless haveI/letI
  • Make m explicit in condExp_add, condExp_sub, etc... for use inside filter_upwards. Currently, using one of those lemmas in filter_upwards results in metavariables.
  • Reorder the file according to typeclass assumptions
  • Rename the base σ-algebra to m₀ and the normed space to E From my PhD (LeanCamCombi)

Estimated changes

modified theorem MeasureTheory.condExp_add
modified theorem MeasureTheory.condExp_bot'
modified theorem MeasureTheory.condExp_bot
modified theorem MeasureTheory.condExp_const
modified theorem MeasureTheory.condExp_mono
modified theorem MeasureTheory.condExp_neg
modified theorem MeasureTheory.condExp_smul
modified theorem MeasureTheory.condExp_sub
modified theorem MeasureTheory.condExp_zero