Commit 2025-02-09 05:54 57e69ed8

View on Github →

chore(MeasureTheory/Integral/Bochner): split Bochner into BochnerL1 and Bochner (#21580) Split the too long file Bochner into BochnerL1 which defines the Bochner integral for L1 functions only, and Bochner which defines the Bochner integral for functions and provides the API.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

deleted theorem MeasureTheory.L1.SimpleFunc.coe_negPart

deleted theorem MeasureTheory.L1.SimpleFunc.coe_posPart

deleted def MeasureTheory.L1.SimpleFunc.integral

deleted def MeasureTheory.L1.SimpleFunc.integralCLM'

deleted def MeasureTheory.L1.SimpleFunc.integralCLM

deleted theorem MeasureTheory.L1.SimpleFunc.integral_L1_eq_integral

deleted theorem MeasureTheory.L1.SimpleFunc.integral_add

deleted theorem MeasureTheory.L1.SimpleFunc.integral_eq_integral

deleted theorem MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub

deleted theorem MeasureTheory.L1.SimpleFunc.integral_eq_setToL1S

deleted theorem MeasureTheory.L1.SimpleFunc.integral_smul

deleted def MeasureTheory.L1.SimpleFunc.negPart

deleted theorem MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc

deleted theorem MeasureTheory.L1.SimpleFunc.norm_Integral_le_one

deleted theorem MeasureTheory.L1.SimpleFunc.norm_eq_integral

deleted theorem MeasureTheory.L1.SimpleFunc.norm_integral_le_norm

deleted theorem MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc

deleted theorem MeasureTheory.L1.continuous_integral

deleted def MeasureTheory.L1.integralCLM

deleted theorem MeasureTheory.L1.integral_add

deleted theorem MeasureTheory.L1.integral_eq

deleted theorem MeasureTheory.L1.integral_eq_norm_posPart_sub

deleted theorem MeasureTheory.L1.integral_eq_setToL1

deleted theorem MeasureTheory.L1.integral_neg

deleted theorem MeasureTheory.L1.integral_smul

deleted theorem MeasureTheory.L1.integral_sub

deleted theorem MeasureTheory.L1.integral_zero

deleted theorem MeasureTheory.L1.nnnorm_Integral_le_one

deleted theorem MeasureTheory.L1.nnnorm_integral_le

deleted theorem MeasureTheory.L1.norm_Integral_le_one

deleted theorem MeasureTheory.L1.norm_integral_le

deleted def MeasureTheory.SimpleFunc.integral

deleted theorem MeasureTheory.SimpleFunc.integral_add

deleted theorem MeasureTheory.SimpleFunc.integral_add_measure

deleted theorem MeasureTheory.SimpleFunc.integral_congr

deleted theorem MeasureTheory.SimpleFunc.integral_const

deleted theorem MeasureTheory.SimpleFunc.integral_def

deleted theorem MeasureTheory.SimpleFunc.integral_eq

deleted theorem MeasureTheory.SimpleFunc.integral_eq_lintegral'

deleted theorem MeasureTheory.SimpleFunc.integral_eq_lintegral

deleted theorem MeasureTheory.SimpleFunc.integral_eq_sum_filter

deleted theorem MeasureTheory.SimpleFunc.integral_eq_sum_of_subset

deleted theorem MeasureTheory.SimpleFunc.integral_neg

deleted theorem MeasureTheory.SimpleFunc.integral_piecewise_zero

deleted theorem MeasureTheory.SimpleFunc.integral_smul

deleted theorem MeasureTheory.SimpleFunc.integral_sub

deleted theorem MeasureTheory.SimpleFunc.map_integral

deleted def MeasureTheory.SimpleFunc.negPart

deleted theorem MeasureTheory.SimpleFunc.negPart_map_norm

deleted theorem MeasureTheory.SimpleFunc.norm_integral_le_integral_norm

deleted theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm

deleted def MeasureTheory.SimpleFunc.posPart

deleted theorem MeasureTheory.SimpleFunc.posPart_map_norm

deleted theorem MeasureTheory.SimpleFunc.posPart_sub_negPart

deleted theorem MeasureTheory.dominatedFinMeasAdditive_weightedSMul

deleted theorem MeasureTheory.norm_weightedSMul_le

deleted def MeasureTheory.weightedSMul

deleted theorem MeasureTheory.weightedSMul_add_measure

deleted theorem MeasureTheory.weightedSMul_apply

deleted theorem MeasureTheory.weightedSMul_congr

deleted theorem MeasureTheory.weightedSMul_empty

deleted theorem MeasureTheory.weightedSMul_nonneg

deleted theorem MeasureTheory.weightedSMul_null

deleted theorem MeasureTheory.weightedSMul_smul

deleted theorem MeasureTheory.weightedSMul_smul_measure

deleted theorem MeasureTheory.weightedSMul_union'

deleted theorem MeasureTheory.weightedSMul_union

deleted theorem MeasureTheory.weightedSMul_zero_measure

Created Mathlib/MeasureTheory/Integral/BochnerL1.lean

added theorem MeasureTheory.L1.SimpleFunc.coe_negPart

added theorem MeasureTheory.L1.SimpleFunc.coe_posPart

added def MeasureTheory.L1.SimpleFunc.integral

added def MeasureTheory.L1.SimpleFunc.integralCLM'

added def MeasureTheory.L1.SimpleFunc.integralCLM

added theorem MeasureTheory.L1.SimpleFunc.integral_L1_eq_integral

added theorem MeasureTheory.L1.SimpleFunc.integral_add

added theorem MeasureTheory.L1.SimpleFunc.integral_eq_integral

added theorem MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub

added theorem MeasureTheory.L1.SimpleFunc.integral_eq_setToL1S

added theorem MeasureTheory.L1.SimpleFunc.integral_smul

added def MeasureTheory.L1.SimpleFunc.negPart

added theorem MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc

added theorem MeasureTheory.L1.SimpleFunc.norm_Integral_le_one

added theorem MeasureTheory.L1.SimpleFunc.norm_eq_integral

added theorem MeasureTheory.L1.SimpleFunc.norm_integral_le_norm

added theorem MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc

added theorem MeasureTheory.L1.continuous_integral

added def MeasureTheory.L1.integralCLM

added theorem MeasureTheory.L1.integral_add

added theorem MeasureTheory.L1.integral_eq

added theorem MeasureTheory.L1.integral_eq_norm_posPart_sub

added theorem MeasureTheory.L1.integral_eq_setToL1

added theorem MeasureTheory.L1.integral_neg

added theorem MeasureTheory.L1.integral_smul

added theorem MeasureTheory.L1.integral_sub

added theorem MeasureTheory.L1.integral_zero

added theorem MeasureTheory.L1.nnnorm_Integral_le_one

added theorem MeasureTheory.L1.nnnorm_integral_le

added theorem MeasureTheory.L1.norm_Integral_le_one

added theorem MeasureTheory.L1.norm_integral_le

added def MeasureTheory.SimpleFunc.integral

added theorem MeasureTheory.SimpleFunc.integral_add

added theorem MeasureTheory.SimpleFunc.integral_add_measure

added theorem MeasureTheory.SimpleFunc.integral_congr

added theorem MeasureTheory.SimpleFunc.integral_const

added theorem MeasureTheory.SimpleFunc.integral_def

added theorem MeasureTheory.SimpleFunc.integral_eq

added theorem MeasureTheory.SimpleFunc.integral_eq_lintegral'

added theorem MeasureTheory.SimpleFunc.integral_eq_lintegral

added theorem MeasureTheory.SimpleFunc.integral_eq_sum_filter

added theorem MeasureTheory.SimpleFunc.integral_eq_sum_of_subset

added theorem MeasureTheory.SimpleFunc.integral_neg

added theorem MeasureTheory.SimpleFunc.integral_piecewise_zero

added theorem MeasureTheory.SimpleFunc.integral_smul

added theorem MeasureTheory.SimpleFunc.integral_sub

added theorem MeasureTheory.SimpleFunc.map_integral

added def MeasureTheory.SimpleFunc.negPart

added theorem MeasureTheory.SimpleFunc.negPart_map_norm

added theorem MeasureTheory.SimpleFunc.norm_integral_le_integral_norm

added theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm

added def MeasureTheory.SimpleFunc.posPart

added theorem MeasureTheory.SimpleFunc.posPart_map_norm

added theorem MeasureTheory.SimpleFunc.posPart_sub_negPart

added theorem MeasureTheory.dominatedFinMeasAdditive_weightedSMul

added theorem MeasureTheory.norm_weightedSMul_le

added def MeasureTheory.weightedSMul

added theorem MeasureTheory.weightedSMul_add_measure

added theorem MeasureTheory.weightedSMul_apply

added theorem MeasureTheory.weightedSMul_congr

added theorem MeasureTheory.weightedSMul_empty

added theorem MeasureTheory.weightedSMul_nonneg

added theorem MeasureTheory.weightedSMul_null

added theorem MeasureTheory.weightedSMul_smul

added theorem MeasureTheory.weightedSMul_smul_measure

added theorem MeasureTheory.weightedSMul_union'

added theorem MeasureTheory.weightedSMul_union

added theorem MeasureTheory.weightedSMul_zero_measure