Commit 2023-10-15 21:38 5ac9cb38

View on Github →

feat: drop more CompleteSpace assumptions (#7691) Also add completeSpace_prod, integrable_prod.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

modified theorem MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul

modified theorem MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.Integrable.fst

added theorem MeasureTheory.Integrable.snd

added theorem MeasureTheory.integrable_prod

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

modified theorem ContinuousLinearEquiv.integral_comp_comm

modified theorem fst_integral

modified theorem integral_pair

modified theorem integral_smul_const

modified theorem snd_integral

added theorem swap_integral

Modified Mathlib/Probability/Kernel/WithDensity.lean

modified theorem ProbabilityTheory.kernel.integral_withDensity

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added def ContinuousLinearEquiv.prodComm

added theorem ContinuousLinearEquiv.prodComm_symm

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

added theorem CompleteSpace.fst_of_prod

added theorem CompleteSpace.snd_of_prod

added theorem completeSpace_prod_of_nonempty