Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-25 09:29 242159f8

View on Github →

feat(measure_theory/bochner_integration): bochner integral of simple functions (#1676)

Bochner integral of simple functions
Update bochner_integration.lean
Change notation for simple functions in L1 space; Fill in blanks in calc proofs
Better definitions of operations on integrable simple functions
Update src/measure_theory/bochner_integration.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Update src/measure_theory/bochner_integration.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Update src/measure_theory/bochner_integration.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Update src/measure_theory/bochner_integration.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Update src/measure_theory/bochner_integration.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Update src/measure_theory/bochner_integration.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Several fixes - listed below
K -> \bbk
remove indentation after calc
use local instances
one tactic per line
add elim_cast attributes
remove definitions from nolints.txt
use linear_map.with_bound to get continuity
Update documentation and comments
Fix things
norm_triangle_sum -> norm_sum_le
fix documentations and comments (The Bochner integral)
Fix typos and grammatical errors
Update src/measure_theory/ae_eq_fun.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr

Estimated changes

Modified scripts/nolints.txt

Modified src/linear_algebra/basic.lean

added theorem finset.smul_sum'

Modified src/measure_theory/ae_eq_fun.lean

modified theorem measure_theory.ae_eq_fun.edist_smul

modified theorem measure_theory.ae_eq_fun.smul_mk

modified theorem measure_theory.ae_eq_fun.smul_to_fun

Modified src/measure_theory/bochner_integration.lean

deleted def measure_theory.integral

deleted def measure_theory.l1.integral

added theorem measure_theory.l1.simple_func.add_to_simple_func

added theorem measure_theory.l1.simple_func.coe_add

added theorem measure_theory.l1.simple_func.coe_neg

added theorem measure_theory.l1.simple_func.coe_smul

added theorem measure_theory.l1.simple_func.coe_sub

added def measure_theory.l1.simple_func.coe_to_l1

added theorem measure_theory.l1.simple_func.coe_zero

deleted theorem measure_theory.l1.simple_func.dense_embedding_of_simple_func

added theorem measure_theory.l1.simple_func.dist_eq

added theorem measure_theory.l1.simple_func.dist_to_simple_func

added theorem measure_theory.l1.simple_func.edist_eq

modified theorem measure_theory.l1.simple_func.exists_simple_func_near

modified def measure_theory.l1.simple_func.integral

added theorem measure_theory.l1.simple_func.integral_add

added def measure_theory.l1.simple_func.integral_clm

added theorem measure_theory.l1.simple_func.integral_congr

added theorem measure_theory.l1.simple_func.integral_eq_lintegral

added theorem measure_theory.l1.simple_func.integral_smul

added theorem measure_theory.l1.simple_func.lintegral_edist_to_simple_func_lt_top

deleted def measure_theory.l1.simple_func.mk

added theorem measure_theory.l1.simple_func.neg_to_simple_func

added theorem measure_theory.l1.simple_func.norm_Integral_le_one

added theorem measure_theory.l1.simple_func.norm_eq'

added theorem measure_theory.l1.simple_func.norm_eq

added theorem measure_theory.l1.simple_func.norm_eq_bintegral

added theorem measure_theory.l1.simple_func.norm_integral_le_norm

added theorem measure_theory.l1.simple_func.norm_of_simple_func

added theorem measure_theory.l1.simple_func.norm_to_simple_func

added def measure_theory.l1.simple_func.of_simple_func

added theorem measure_theory.l1.simple_func.of_simple_func_add

added theorem measure_theory.l1.simple_func.of_simple_func_eq_mk

added theorem measure_theory.l1.simple_func.of_simple_func_eq_of_fun

added theorem measure_theory.l1.simple_func.of_simple_func_neg

added theorem measure_theory.l1.simple_func.of_simple_func_smul

added theorem measure_theory.l1.simple_func.of_simple_func_sub

added theorem measure_theory.l1.simple_func.of_simple_func_to_simple_func

added theorem measure_theory.l1.simple_func.of_simple_func_zero

added theorem measure_theory.l1.simple_func.smul_to_simple_func

added theorem measure_theory.l1.simple_func.sub_to_simple_func

modified def measure_theory.l1.simple_func.to_simple_func

added theorem measure_theory.l1.simple_func.to_simple_func_eq_to_fun

added theorem measure_theory.l1.simple_func.to_simple_func_of_simple_func

deleted theorem measure_theory.l1.simple_func.uniform_continuous_of_simple_func

deleted theorem measure_theory.l1.simple_func.uniform_embedding_of_simple_func

added theorem measure_theory.l1.simple_func.zero_to_simple_func

added def measure_theory.simple_func.bintegral

added theorem measure_theory.simple_func.bintegral_add

added theorem measure_theory.simple_func.bintegral_congr

added theorem measure_theory.simple_func.bintegral_eq_integral'

added theorem measure_theory.simple_func.bintegral_eq_integral

added theorem measure_theory.simple_func.bintegral_eq_lintegral'

added theorem measure_theory.simple_func.bintegral_eq_lintegral

added theorem measure_theory.simple_func.bintegral_smul

added theorem measure_theory.simple_func.fin_vol_supp_of_integrable

added theorem measure_theory.simple_func.integrable_iff_fin_vol_supp

added theorem measure_theory.simple_func.integrable_iff_integral_lt_top

added theorem measure_theory.simple_func.integrable_of_fin_vol_supp

added theorem measure_theory.simple_func.integrable_pair

added theorem measure_theory.simple_func.map_bintegral

added theorem measure_theory.simple_func.norm_bintegral_le_bintegral_norm

Modified src/measure_theory/l1_space.lean

modified theorem measure_theory.ae_eq_fun.integrable_smul

modified theorem measure_theory.integrable_smul

deleted theorem measure_theory.l1.add_def

deleted theorem measure_theory.l1.all_ae_mk_to_fun

added theorem measure_theory.l1.coe_add

added theorem measure_theory.l1.coe_neg

added theorem measure_theory.l1.coe_smul

added theorem measure_theory.l1.coe_sub

added theorem measure_theory.l1.coe_zero

deleted theorem measure_theory.l1.dist_def

added theorem measure_theory.l1.dist_eq

added theorem measure_theory.l1.edist_eq

deleted theorem measure_theory.l1.ext_iff

deleted def measure_theory.l1.mk

deleted theorem measure_theory.l1.mk_add

deleted theorem measure_theory.l1.mk_eq_mk

added theorem measure_theory.l1.mk_to_fun

deleted theorem measure_theory.l1.mk_zero

deleted theorem measure_theory.l1.neg_mk

modified theorem measure_theory.l1.neg_to_fun

deleted theorem measure_theory.l1.norm_def

added theorem measure_theory.l1.norm_eq

deleted theorem measure_theory.l1.norm_mk

added theorem measure_theory.l1.norm_of_fun

added def measure_theory.l1.of_fun

added theorem measure_theory.l1.of_fun_add

added theorem measure_theory.l1.of_fun_eq_mk

added theorem measure_theory.l1.of_fun_eq_of_fun

added theorem measure_theory.l1.of_fun_neg

added theorem measure_theory.l1.of_fun_smul

added theorem measure_theory.l1.of_fun_to_fun

added theorem measure_theory.l1.of_fun_zero

deleted theorem measure_theory.l1.self_eq_mk

deleted theorem measure_theory.l1.smul_def

deleted theorem measure_theory.l1.smul_mk

modified theorem measure_theory.l1.smul_to_fun

added theorem measure_theory.l1.to_fun_of_fun

deleted theorem measure_theory.l1.zero_def