Commit 2024-03-23 07:28 8b3fbc92

View on Github →

feat: Positivity extension for Bochner integral (#10661) Inspired by #10538 add a positivity extension for Bochner integrals.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added def Mathlib.Meta.Positivity.evalIntegral

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/Probability/Moments.lean

Modified Mathlib/Probability/Variance.lean

Modified scripts/style-exceptions.txt

Modified test/positivity.lean