Commit 2023-06-05 08:37 6af7bec9

View on Github →

feat: port MeasureTheory.Integral.Bochner (#4590)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem ClosedEmbedding.integral_map

added theorem MeasurableEmbedding.integral_map

added theorem MeasureTheory.HasFiniteIntegral.tendsto_set_integral_nhds_zero

added theorem MeasureTheory.Integrable.tendsto_set_integral_nhds_zero

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_integral

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_of_fun_eq_integral

added theorem MeasureTheory.L1.integral_smul

added theorem MeasureTheory.L1.integral_sub

added theorem MeasureTheory.L1.integral_zero

added theorem MeasureTheory.L1.norm_Integral_le_one

added theorem MeasureTheory.L1.norm_eq_integral_norm

added theorem MeasureTheory.L1.norm_integral_le

added theorem MeasureTheory.L1.norm_of_fun_eq_integral_norm

added theorem MeasureTheory.MeasurePreserving.integral_comp

added theorem MeasureTheory.Memℒp.snorm_eq_integral_rpow_norm

added theorem MeasureTheory.SimpleFunc.coe_toLargerSpace_eq

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_integral

added theorem MeasureTheory.SimpleFunc.integral_eq_lintegral'

added theorem MeasureTheory.SimpleFunc.integral_eq_lintegral

added theorem MeasureTheory.SimpleFunc.integral_eq_sum

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 def MeasureTheory.SimpleFunc.toLargerSpace

added theorem MeasureTheory.ae_eq_trim_iff

added theorem MeasureTheory.ae_eq_trim_of_stronglyMeasurable

added theorem MeasureTheory.ae_le_trim_iff

added theorem MeasureTheory.ae_le_trim_of_stronglyMeasurable

added theorem MeasureTheory.continuousAt_of_dominated

added theorem MeasureTheory.continuousOn_of_dominated

added theorem MeasureTheory.continuousWithinAt_of_dominated

added theorem MeasureTheory.continuous_integral

added theorem MeasureTheory.continuous_of_dominated

added theorem MeasureTheory.dominatedFinMeasAdditive_weightedSMul

added theorem MeasureTheory.ennnorm_integral_le_lintegral_ennnorm

added theorem MeasureTheory.hasSum_integral_measure

added theorem MeasureTheory.hasSum_integral_of_dominated_convergence

added theorem MeasureTheory.integrable_of_integral_eq_one

added theorem MeasureTheory.integral_add'

added theorem MeasureTheory.integral_add

added theorem MeasureTheory.integral_add_measure

added theorem MeasureTheory.integral_coe_le_of_lintegral_coe_le

added theorem MeasureTheory.integral_congr_ae

added theorem MeasureTheory.integral_const

added theorem MeasureTheory.integral_dirac'

added theorem MeasureTheory.integral_dirac

added theorem MeasureTheory.integral_div

added theorem MeasureTheory.integral_eq

added theorem MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part

added theorem MeasureTheory.integral_eq_lintegral_of_nonneg_ae

added theorem MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part

added theorem MeasureTheory.integral_eq_setToFun

added theorem MeasureTheory.integral_eq_zero_iff_of_nonneg

added theorem MeasureTheory.integral_eq_zero_iff_of_nonneg_ae

added theorem MeasureTheory.integral_eq_zero_of_ae

added theorem MeasureTheory.integral_finset_sum

added theorem MeasureTheory.integral_finset_sum_measure

added theorem MeasureTheory.integral_map

added theorem MeasureTheory.integral_map_equiv

added theorem MeasureTheory.integral_map_of_stronglyMeasurable

added theorem MeasureTheory.integral_mono

added theorem MeasureTheory.integral_mono_ae

added theorem MeasureTheory.integral_mono_measure

added theorem MeasureTheory.integral_mono_of_nonneg

added theorem MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg

added theorem MeasureTheory.integral_mul_left

added theorem MeasureTheory.integral_mul_norm_le_Lp_mul_Lq

added theorem MeasureTheory.integral_mul_right

added theorem MeasureTheory.integral_neg'

added theorem MeasureTheory.integral_neg

added theorem MeasureTheory.integral_non_aestronglyMeasurable

added theorem MeasureTheory.integral_nonneg

added theorem MeasureTheory.integral_nonneg_of_ae

added theorem MeasureTheory.integral_nonpos

added theorem MeasureTheory.integral_nonpos_of_ae

added theorem MeasureTheory.integral_norm_eq_lintegral_nnnorm

added theorem MeasureTheory.integral_pos_iff_support_of_nonneg

added theorem MeasureTheory.integral_pos_iff_support_of_nonneg_ae

added theorem MeasureTheory.integral_simpleFunc_larger_space

added theorem MeasureTheory.integral_smul

added theorem MeasureTheory.integral_smul_measure

added theorem MeasureTheory.integral_sub'

added theorem MeasureTheory.integral_sub

added theorem MeasureTheory.integral_sum_measure

added theorem MeasureTheory.integral_toReal

added theorem MeasureTheory.integral_trim

added theorem MeasureTheory.integral_trim_ae

added theorem MeasureTheory.integral_trim_simpleFunc

added theorem MeasureTheory.integral_tsum

added theorem MeasureTheory.integral_undef

added theorem MeasureTheory.integral_zero'

added theorem MeasureTheory.integral_zero

added theorem MeasureTheory.integral_zero_measure

added theorem MeasureTheory.lintegral_coe_eq_integral

added theorem MeasureTheory.lintegral_coe_le_coe_iff_integral_le

added theorem MeasureTheory.mul_meas_ge_le_integral_of_nonneg

added theorem MeasureTheory.nndist_integral_add_measure_le_lintegral

added theorem MeasureTheory.norm_integral_le_integral_norm

added theorem MeasureTheory.norm_integral_le_lintegral_norm

added theorem MeasureTheory.norm_integral_le_of_norm_le

added theorem MeasureTheory.norm_integral_le_of_norm_le_const

added theorem MeasureTheory.norm_weightedSMul_le

added theorem MeasureTheory.ofReal_integral_eq_lintegral_ofReal

added theorem MeasureTheory.ofReal_integral_norm_eq_lintegral_nnnorm

added theorem MeasureTheory.set_integral_dirac'

added theorem MeasureTheory.set_integral_dirac

added theorem MeasureTheory.set_integral_eq_subtype

added theorem MeasureTheory.snorm_one_le_of_le'

added theorem MeasureTheory.snorm_one_le_of_le

added theorem MeasureTheory.tendsto_integral_approxOn_of_measurable

added theorem MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset

added theorem MeasureTheory.tendsto_integral_filter_of_dominated_convergence

added theorem MeasureTheory.tendsto_integral_of_L1

added theorem MeasureTheory.tendsto_integral_of_dominated_convergence

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

Created Mathlib/MeasureTheory/Integral/IntegralSimps.lean