Commit 2024-07-11 13:27 fc5e76e4

View on Github →

feat(ENNReal): ENNReal.rpow_inv_lt_iff (#14570) Self-contained PR filling an API gap for ENNReal. To be used in PR #9163.

Estimated changes

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/MeanInequalitiesPow.lean

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

Modified Mathlib/Analysis/NormedSpace/ProdLp.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

added theorem ENNReal.le_rpow_inv_iff

added theorem ENNReal.lt_rpow_inv_iff

added theorem ENNReal.rpow_inv_le_iff

added theorem ENNReal.rpow_inv_lt_iff

added theorem NNReal.eq_rpow_inv_iff

added theorem NNReal.le_rpow_inv_iff

added theorem NNReal.lt_rpow_inv_iff

added theorem NNReal.rpow_inv_eq_iff

added theorem NNReal.rpow_inv_le_iff

added theorem NNReal.rpow_inv_lt_iff

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

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean