Commit 2024-12-23 14:32 9c1fb883

View on Github →

feat: generalize measure-theoretic definitions using ENorm (#20122)

Lemmas are not generalized yet (some lemmas can be generalized by just weakening the typeclasses, but others require rules how enorm interacts with algebraic operations).
All proofs that broke unfolded the definition. Now they rewrite with a lemma giving the definition in terms of nnnorm.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/ENormedSpace.lean

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

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

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

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

Modified Mathlib/MeasureTheory/Function/L1Space.lean

modified def MeasureTheory.HasFiniteIntegral

modified def MeasureTheory.Integrable

modified theorem MeasureTheory.hasFiniteIntegral_def

added theorem MeasureTheory.hasFiniteIntegral_iff_nnnorm

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

modified def MeasureTheory.Memℒp

modified def MeasureTheory.eLpNorm'

added theorem MeasureTheory.eLpNorm'_eq_lintegral_nnnorm

modified theorem MeasureTheory.eLpNorm'_zero

modified def MeasureTheory.eLpNormEssSup

added theorem MeasureTheory.eLpNormEssSup_eq_essSup_nnnorm

Modified Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

modified def MeasureTheory.IntegrableAtFilter

modified def MeasureTheory.IntegrableOn

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/Prod.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/Probability/Density.lean

Modified Mathlib/Probability/Distributions/Exponential.lean

Modified Mathlib/Probability/Integration.lean

Modified Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean

Modified Mathlib/Probability/Kernel/CondDistrib.lean