Commit 2025-08-08 00:06 08ab79b4

View on Github →

feat: integrability in a product space (#27674) Prove that f : (i : ι) → X → E i is in Lᵖ if and only if for all i, f i is in Lᵖ. Do the same for f : X → (E × F). Also provide WithLp versions. from BrownianMotion

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

added theorem ContinuousLinearMap.norm_single

added theorem ContinuousLinearMap.norm_single_le_one

Modified Mathlib/MeasureTheory/Integral/Pi.lean

added theorem MeasureTheory.integrable_comp_eval

added theorem MeasureTheory.integral_comp_eval

modified theorem MeasureTheory.integral_fintype_prod_eq_pow

modified theorem MeasureTheory.integral_fintype_prod_eq_prod

modified theorem MeasureTheory.integral_fintype_prod_volume_eq_pow

modified theorem MeasureTheory.integral_fintype_prod_volume_eq_prod

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

Created Mathlib/MeasureTheory/SpecificCodomains/Pi.lean

added theorem MeasureTheory.MemLp.fst

added theorem MeasureTheory.MemLp.snd

added theorem MeasureTheory.eval_integral

added theorem MeasureTheory.integrable_pi_iff

added theorem MeasureTheory.memLp_pi_iff

added theorem MeasureTheory.memLp_prod_iff

Created Mathlib/MeasureTheory/SpecificCodomains/WithLp.lean

added theorem MeasureTheory.Integrable.prodLp_fst

added theorem MeasureTheory.Integrable.prodLp_snd

added theorem MeasureTheory.MemLp.prodLp_fst

added theorem MeasureTheory.MemLp.prodLp_snd

added theorem MeasureTheory.eval_integral_piLp

added theorem MeasureTheory.fst_integral_withLp

added theorem MeasureTheory.integrable_piLp_iff

added theorem MeasureTheory.integrable_prodLp_iff

added theorem MeasureTheory.memLp_piLp_iff

added theorem MeasureTheory.memLp_prodLp_iff

added theorem MeasureTheory.snd_integral_withLp

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean