Commit 2023-07-17 03:51 307d5488

View on Github →

feat(MeasureTheory.Integral.Bochner): drop completeness requirement from the definition (#5910) The notion of Bochner integral of a function taking values in a normed space E requires that E is complete. This means that whenever we write down an integral, the term contains the assertion that E is complete. In this PR, we remove the completeness requirement from the definition, using the junk value 0 when the space is not complete. Mathematically this does not make any difference, as all reasonable applications will be with a complete E. But it means that terms involving integrals become a little bit simpler and that completeness will not have to be checked by the system when applying a bunch of basic lemmas on integrals.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

modified theorem convolution_mul

modified theorem convolution_mul_swap

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

modified theorem Real.fourierIntegral_eq_integral_exp_smul

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

modified theorem MeasureTheory.HasFiniteIntegral.tendsto_set_integral_nhds_zero

modified theorem MeasureTheory.Integrable.tendsto_set_integral_nhds_zero

modified theorem MeasureTheory.L1.integral_of_fun_eq_integral

modified theorem MeasureTheory.continuousAt_of_dominated

modified theorem MeasureTheory.continuousOn_of_dominated

modified theorem MeasureTheory.continuousWithinAt_of_dominated

modified theorem MeasureTheory.continuous_integral

modified theorem MeasureTheory.continuous_of_dominated

modified theorem MeasureTheory.ennnorm_integral_le_lintegral_ennnorm

modified theorem MeasureTheory.hasSum_integral_measure

modified theorem MeasureTheory.hasSum_integral_of_dominated_convergence

modified theorem MeasureTheory.integral_add'

modified theorem MeasureTheory.integral_add

modified theorem MeasureTheory.integral_add_measure

modified theorem MeasureTheory.integral_congr_ae

modified theorem MeasureTheory.integral_eq

modified theorem MeasureTheory.integral_eq_zero_of_ae

modified theorem MeasureTheory.integral_finset_sum

modified theorem MeasureTheory.integral_finset_sum_measure

modified theorem MeasureTheory.integral_map

modified theorem MeasureTheory.integral_map_equiv

modified theorem MeasureTheory.integral_neg'

modified theorem MeasureTheory.integral_neg

modified theorem MeasureTheory.integral_non_aestronglyMeasurable

modified theorem MeasureTheory.integral_norm_eq_lintegral_nnnorm

modified theorem MeasureTheory.integral_smul

modified theorem MeasureTheory.integral_smul_measure

modified theorem MeasureTheory.integral_sub'

modified theorem MeasureTheory.integral_sub

modified theorem MeasureTheory.integral_sum_measure

modified theorem MeasureTheory.integral_trim

modified theorem MeasureTheory.integral_trim_ae

modified theorem MeasureTheory.integral_tsum

modified theorem MeasureTheory.integral_undef

modified theorem MeasureTheory.integral_zero'

modified theorem MeasureTheory.integral_zero

modified theorem MeasureTheory.integral_zero_measure

modified theorem MeasureTheory.nndist_integral_add_measure_le_lintegral

modified theorem MeasureTheory.norm_integral_le_integral_norm

modified theorem MeasureTheory.norm_integral_le_lintegral_norm

modified theorem MeasureTheory.norm_integral_le_of_norm_le

modified theorem MeasureTheory.norm_integral_le_of_norm_le_const

modified theorem MeasureTheory.ofReal_integral_norm_eq_lintegral_nnnorm

modified theorem MeasureTheory.tendsto_integral_of_L1

modified theorem MeasureTheory.tendsto_integral_of_dominated_convergence

Modified Mathlib/MeasureTheory/Integral/CircleTransform.lean

modified theorem Complex.integral_circleTransform

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

modified theorem MeasureTheory.continuous_set_integral

modified theorem MeasureTheory.integral_indicatorConstLp

modified theorem MeasureTheory.integral_indicator_const

modified theorem MeasureTheory.set_integral_const

modified theorem MeasureTheory.set_integral_indicatorConstLp

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

Modified Mathlib/Probability/IdentDistrib.lean

modified theorem ProbabilityTheory.IdentDistrib.integral_eq

Modified Mathlib/Probability/Kernel/Basic.lean

modified theorem ProbabilityTheory.kernel.integral_const

modified theorem ProbabilityTheory.kernel.integral_piecewise

modified theorem ProbabilityTheory.kernel.set_integral_const

Modified Mathlib/Probability/Martingale/Convergence.lean