Revision #1298 → #2590 · back to history
modifiedEssential supremum convention15b59c303649
| Field | From #1298 | To #2590 |
|---|
| mathlib.decl | MeasureTheory.essSup | essSup |
| provenance | ai | ai-moderated |
modifiedCauchy–Schwarz inequality (L² case)3ab10fdc1be8
| Field | From #1298 | To #2590 |
|---|
| mathlib.decl | integral_mul_norm_le_Lp_mul_Lq | MeasureTheory.integral_mul_norm_le_Lp_mul_Lq |
| provenance | ai | ai-moderated |
modifiedHölder's inequality on a probability space577a867efeaf
| Field | From #1298 | To #2590 |
|---|
| mathlib.decl | MemLp.mono_exponent | MeasureTheory.MemLp.mono_exponent |
| provenance | ai | ai-moderated |
modifiedHölder's inequality for Lebesgue measure4193c538fcce
| Field | From #1298 | To #2590 |
|---|
| mathlib.decl | integral_mul_norm_le_Lp_mul_Lq | MeasureTheory.integral_mul_norm_le_Lp_mul_Lq |
| provenance | ai | ai-moderated |
modifiedHölder's inequality for random variables52efed8d356f
| Field | From #1298 | To #2590 |
|---|
| mathlib.decl | integral_mul_norm_le_Lp_mul_Lq | MeasureTheory.integral_mul_norm_le_Lp_mul_Lq |
| provenance | ai | ai-moderated |
modifiedAbsolute moment inequality9e07f75e9c25
| Field | From #1298 | To #2590 |
|---|
| mathlib.decl | MemLp.mono_exponent | MeasureTheory.MemLp.mono_exponent |
| provenance | ai | ai-moderated |
modifiedHölder's inequality for vector-valued functions206589396aac
| Field | From #1298 | To #2590 |
|---|
| mathlib.decl | eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm | MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm |
| provenance | ai | ai-moderated |