Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-03 00:58 fd5617c1

View on Github →

feat(measure_theory): Define Bochner integration (#1149)

  • Create .DS_Store
  • Revert "Create .DS_Store" This reverts commit 5612886d493aef59205eddc5a34a75e6e5ba22c1.
  • Define bochner integral
  • Define bochner integral
  • Headings
  • Change used names
  • Fix styles; Get rid of redundant lemmas
  • Delete dash lines
  • changes
  • Fix everything Things remaining:
  • extend comments in headings
  • integrable predicate should include measurability
  • better proofs for simple_func_dense.lean
  • Fix everything Things remaining:
  • extend comments in headings
  • integrable predicate should include measurability
  • better proofs for simple_func_dense.lean
  • Remove redundant lemma
  • Fix styles

Estimated changes

modified theorem finset.prod_map
added theorem nat.inv_pos_of_nat
added theorem nat.one_div_pos_of_nat
modified theorem real.mul_rpow
modified theorem real.rpow_le_rpow
modified theorem real.norm_eq_abs
modified theorem fin.cast_succ_cast_lt
modified theorem finset.Ico.image_sub
modified theorem finsupp.support_add_eq
modified theorem holor.mul_assoc
modified theorem holor.slice_add
modified theorem list.Ico.map_sub
modified theorem nat.mul_left_eq_self_iff
modified theorem nat.mul_right_eq_self_iff
added theorem nat.cast_add_one_pos
modified theorem nonempty_quotient_iff
modified theorem quotient.lift_beta
modified theorem quotient.lift_on_beta
added theorem ennreal.coe_nnreal_eq
added theorem ennreal.of_real_mul
modified theorem ennreal.sub_left_inj
added theorem ennreal.sub_self
modified theorem hyperreal.epsilon_lt_pos
modified theorem hyperreal.infinite_omega
modified theorem hyperreal.infinitesimal_add
modified theorem hyperreal.infinitesimal_def
modified theorem hyperreal.infinitesimal_mul
modified theorem hyperreal.infinitesimal_neg
modified theorem hyperreal.is_st_Sup
modified theorem hyperreal.is_st_add
modified theorem hyperreal.is_st_inj_real
modified theorem hyperreal.is_st_inv
modified theorem hyperreal.is_st_mul
modified theorem hyperreal.is_st_neg
modified theorem hyperreal.is_st_real_iff_eq
modified theorem hyperreal.is_st_refl_real
modified theorem hyperreal.is_st_st'
modified theorem hyperreal.is_st_st
modified theorem hyperreal.is_st_st_of_is_st
modified theorem hyperreal.is_st_symm_real
modified theorem hyperreal.is_st_trans_real
modified theorem hyperreal.lt_of_st_lt
modified theorem hyperreal.not_infinite_add
modified theorem hyperreal.not_infinite_mul
modified theorem hyperreal.not_infinite_neg
modified theorem hyperreal.st_add
modified theorem hyperreal.st_infinite
modified theorem hyperreal.st_inv
modified theorem hyperreal.st_le_of_le
modified theorem hyperreal.st_mul
modified theorem hyperreal.st_neg
modified theorem hyperreal.st_of_is_st
added theorem nnreal.of_real_mul
modified theorem rel.core_id
modified def rel
modified theorem set.range_coe_subtype
added theorem set.range_ite_subset'
added theorem set.range_ite_subset
added theorem set.disjointed_subset
added theorem set.finite_range_const
added theorem set.finite_range_ite
modified theorem set.Union_subset_iff
modified theorem dim_map_le
modified theorem function.restrict_eq
added theorem measurable_from_nat
added theorem measurable_to_nat
modified theorem bdd_below_bot
modified theorem filter.mem_infi
modified theorem filter.mem_infi_finite
modified theorem filter.univ_mem_sets'
modified theorem polynomial.degree_le_mono
modified theorem liminf_eq_of_tendsto
modified theorem limsup_eq_of_tendsto
modified theorem mem_of_is_glb_of_is_closed
modified theorem mem_of_is_lub_of_is_closed
modified theorem tendsto_of_liminf_eq_limsup
added theorem dense_of_subset_dense
added theorem ennreal.Icc_mem_nhds
added theorem ennreal.nhds_of_ne_top
added theorem ennreal.nhds_top
added theorem ennreal.nhds_zero
modified theorem nnreal.tendsto_of_real
added theorem continuous_nndist
modified theorem emetric.ball_subset
modified theorem uniformity_lift_le_comp
modified def tidy.test.tidy_test_1