Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-21 21:29 aa6cc06f

View on Github →

feat(measure_theory/set_integral): integrals over subsets (#1875)

  • feat(measure_theory/set_integral): integral on a set
  • mismached variables
  • move if_preimage
  • Update src/measure_theory/l1_space.lean Co-Authored-By: Yury G. Kudryashov urkud@ya.ru
  • Small fixes
  • Put indicator_function into data folder
  • Use antimono as names
  • Change name to antimono
  • Fix everything
  • Use binder notation for integrals
  • delete an extra space
  • Update set_integral.lean
  • adjust implicit and explicit variables
  • measurable_on_singleton
  • prove integral_on_Union
  • Update indicator_function.lean
  • Update set_integral.lean
  • lint
  • Update bochner_integration.lean
  • reviewer's comment
  • use Yury's proof

Estimated changes

added theorem finset.bUnion_insert
added theorem finset.bUnion_union
added theorem finset.supr_union
added def set.indicator
added theorem set.indicator_add
added theorem set.indicator_compl
added theorem set.indicator_congr
added theorem set.indicator_empty
added theorem set.indicator_neg
added theorem set.indicator_of_mem
added theorem set.indicator_preimage
added theorem set.indicator_smul
added theorem set.indicator_sub
added theorem set.indicator_univ
added theorem set.indicator_zero
added theorem set.if_preimage
modified theorem measure_theory.integral_neg
added theorem is_measurable_Icc
added theorem is_measurable_Ici
modified theorem is_measurable_Ico
added theorem is_measurable_Iic
added theorem is_measurable_Ioc
added theorem is_measurable_Ioi
added theorem indicator_congr_ae
added theorem indicator_congr_of_set
added theorem indicator_union_ae
added theorem integrable_on.add
added theorem integrable_on.divide
added theorem integrable_on.mul_left
added theorem integrable_on.neg
added theorem integrable_on.smul
added theorem integrable_on.sub
added theorem integrable_on.subset
added theorem integrable_on.union
added def integrable_on
added theorem integrable_on_congr
added theorem integrable_on_congr_ae
added theorem integrable_on_empty
added theorem integrable_on_norm_iff
added theorem integral_on_Union
added theorem integral_on_add
added theorem integral_on_congr
added theorem integral_on_div
added theorem integral_on_mul_left
added theorem integral_on_mul_right
added theorem integral_on_neg
added theorem integral_on_smul
added theorem integral_on_sub
added theorem integral_on_union
added theorem integral_on_union_ae
added theorem integral_on_zero
added theorem measurable_on.subset
added theorem measurable_on.union
added def measurable_on
added theorem measurable_on_empty
added theorem measurable_on_univ