Revision #3189 → #3706 · back to history
modifiedHölder's inequality7d47a79ef62f
| Field | From #3189 | To #3706 |
|---|
| note | Mathlib formalizes the central Hölder inequality `∫ f·g ≤ (∫ fᵖ)^(1/p)·(∫ gᵍ)^(1/q)` for conjugate exponents and ℝ≥0∞-valued measurable functions. | Verified: `ENNReal.lintegral_mul_le_Lp_mul_Lq` exists and states the ℝ≥0∞ Hölder integral inequality for conjugate exponents. |
modifiedConventions for Hölder conjugates7a93851b7a85
| Field | From #3189 | To #3706 |
|---|
| note | `ENNReal.HolderConjugate p q` is defined as `p⁻¹ + q⁻¹ = 1` in `ℝ≥0∞` where `(∞)⁻¹ = 0`, exactly matching the Wikipedia convention. | Verified: `ENNReal.HolderConjugate p q` encodes `p⁻¹ + q⁻¹ = 1` in ℝ≥0∞ where `∞⁻¹ = 0`. |
modifiedEssential supremum convention15b59c303649
| Field | From #3189 | To #3706 |
|---|
| note | `essSup f μ` is defined as `(ae μ).limsup f`, capturing the essential supremum of a measurable function. | Verified: `essSup` is defined in Mathlib as the essential supremum with respect to a measure. |
modifiedCauchy–Schwarz inequality (L² case)3ab10fdc1be8
| Field | From #3189 | To #3706 |
|---|
| note | The L² Cauchy–Schwarz inequality is the special case p=q=2 of Mathlib's Hölder inequality for Bochner integrals; the abstract Hilbert-space version is `norm_inner_le_norm`. | Verified: the L² Cauchy–Schwarz on integrable products is the p=q=2 case of `integral_mul_norm_le_Lp_mul_Lq`. |
modifiedHölder's inequality on a probability space577a867efeaf
| Field | From #3189 | To #3706 |
|---|
| note | Mathlib has the underlying pieces (Hölder + `MemLp.mono_exponent` for finite measures) but no single decl stating the relaxed `1/p + 1/q ≤ 1` Hölder on a probability space. | Verified: `MemLp.mono_exponent` plus Hölder gives the relaxed `1/p + 1/q ≤ 1` version on finite/probability measures, but no dedicated named lemma exists. |
modifiedHölder's inequality for counting measured2781e425452
| Field | From #3189 | To #3706 |
|---|
| note | Finite-sum Hölder inequalities for NNReal- and Real-valued sequences (`inner_le_Lp_mul_Lq` and variants) formalize the counting-measure case directly. | Verified: `NNReal.inner_le_Lp_mul_Lq` states the finite-sum Hölder inequality (counting measure). |
modifiedGeneralization to more than two sums809f2d08df24
| Field | From #3189 | To #3706 |
|---|
| note | The multi-function Hölder `lintegral_prod_norm_pow_le` covers the counting-measure (sums) case as a special instance. | Verified: `lintegral_prod_norm_pow_le` covers the multi-function Hölder inequality, specializing to counting measure gives the multi-sum version. |
modifiedHölder's inequality for sequence spaces5e0cf8eac2c3
| Field | From #3189 | To #3706 |
|---|
| note | `lp.tsum_mul_le_mul_norm` (and `NNReal.inner_le_Lp_mul_Lq_tsum`) state Hölder for the sequence spaces `ℓᵖ` and `ℓ^q`. | Verified: `lp.tsum_mul_le_mul_norm` gives Hölder for the sequence spaces ℓᵖ and ℓ^q. |
modifiedHölder's inequality for Lebesgue measure4193c538fcce
| Field | From #3189 | To #3706 |
|---|
| note | The Lebesgue-measure case follows by specializing the general Bochner Hölder inequality `integral_mul_norm_le_Lp_mul_Lq` to `volume`. | Verified: the general Bochner Hölder inequality specializes to Lebesgue measure by choosing `μ = volume`. |
modifiedHölder's inequality for random variables52efed8d356f
| Field | From #3189 | To #3706 |
|---|
| note | The probability/random-variable formulation `E[|XY|] ≤ E[|X|^p]^{1/p}·E[|Y|^q]^{1/q}` is a special case of the general Bochner Hölder when `μ` is a probability measure. | Verified: the random-variable version is `integral_mul_norm_le_Lp_mul_Lq` applied to a probability measure. |
modifiedAbsolute moment inequality9e07f75e9c25
| Field | From #3189 | To #3706 |
|---|
| note | `MemLp.mono_exponent` shows that for a finite measure (in particular a probability measure), `MemLp f q μ` and `p ≤ q` imply `MemLp f p μ`, i.e. the lower absolute moment is finite. | Verified: `MemLp.mono_exponent` gives that under a finite measure lower `Lᵖ` membership follows from higher, i.e. the moment inclusion. |
modifiedHölder's inequality for product measures2de53c9d7d64
| Field | From #3189 | To #3706 |
|---|
| note | The general Hölder inequality applies to any measure, including product measures; combined with Tonelli/`lintegral_prod` it yields the iterated-integral form, though no dedicated combined lemma exists. | Verified: the general ENNReal Hölder inequality applies to any measure including product measures; combined with Tonelli yields the iterated form. |
modifiedHölder's inequality for vector-valued functions206589396aac
| Field | From #3189 | To #3706 |
|---|
| note | This abstract Hölder estimate for `‖b(f,g)‖` under a bilinear bound generalizes the vector-valued case; see also `MemLp.of_bilin` and `ContinuousLinearMap.holder`. | Verified: `eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm` is the abstract vector-valued/bilinear-bound Hölder estimate in Mathlib. |
modifiedEquality condition (vector-valued)19ce5e2ab2a3
| Field | From #3189 | To #3706 |
|---|
| note | Mathlib has no decl characterizing equality in Hölder's inequality for vector-valued functions. | Grep of Mathlib finds no characterization of the equality case of vector-valued Hölder. |
modifiedEquality condition in Hölder's inequalityb05062940368
| Field | From #3189 | To #3706 |
|---|
| note | Mathlib does not formalize the equality characterization for Hölder's inequality. | No lemma in Mathlib characterizes the equality case of Hölder's inequality. |
modifiedYoung's inequality for products42a4e44eaed1
| Field | From #3189 | To #3706 |
|---|
| note | `Real.young_inequality` proves `a·b ≤ aᵖ/p + bᵍ/q` for nonnegative `a, b` and conjugate exponents `p, q ∈ (1,∞)`, the key lemma invoked in the main proof. | Verified: `Real.young_inequality` proves `a·b ≤ aᵖ/p + bᵍ/q` for nonnegative reals and conjugate exponents. |
modifiedExtremal equality for L^p norm0c01176d1b72
| Field | From #3189 | To #3706 |
|---|
| note | `NNReal.isGreatest_Lp` proves the extremal characterization of the `ℓᵖ`-norm over a `Finset` (counting-measure case); the general integral version is not formalized. | Verified: `NNReal.isGreatest_Lp` gives the counting-measure/finite-sum extremal characterization; the general integral version is not formalized. |
modifiedFailure of extremal equality for p=∞0763d579bc7f
| Field | From #3189 | To #3706 |
|---|
| note | This counterexample/remark is not formalized in Mathlib. | This remark/counterexample is not present in Mathlib. |
modifiedSupremum not attained for p=11880cdc02d0f
| Field | From #3189 | To #3706 |
|---|
| note | This counterexample about non-attainment for p=1 is not formalized. | No Mathlib lemma states non-attainment of the L¹ dual supremum. |
modifiedBounded linear functional from L^p0374ccded0f0
| Field | From #3189 | To #3706 |
|---|
| note | `ContinuousLinearMap.lpPairing` constructs the bounded bilinear pairing `Lp E p →L Lp F q →L G` arising from Hölder, but Mathlib does not have a dedicated `L^q → (L^p)*` operator-norm/isometry decl in this generality. | Verified: `ContinuousLinearMap.lpPairing` builds the continuous bilinear pairing `Lp E p →L Lp F q →L G`, but no dedicated `L^q → (L^p)*` isometry decl exists. |
modifiedMinkowski inequality via extremal equalityd1f675869ac5
| Field | From #3189 | To #3706 |
|---|
| note | The Minkowski (Lᵖ triangle) inequality `‖f + g‖_p ≤ ‖f‖_p + ‖g‖_p` is formalized in Mathlib and can be derived via Hölder's extremal equality. | Verified: `ENNReal.lintegral_Lp_add_le` states Minkowski's inequality for lintegral Lᵖ-norms. |
modifiedGeneralized Hölder's inequality (n functions)70c81398ab54
| Field | From #3189 | To #3706 |
|---|
| note | `lintegral_prod_norm_pow_le` formalizes Hölder for a finite family of functions with weights summing to 1. | Verified: `lintegral_prod_norm_pow_le` formalizes Hölder for a finite family of functions with weighted exponents summing to 1. |
modifiedInterpolation via weighted harmonic mean5bbd53c432f6
| Field | From #3189 | To #3706 |
|---|
| note | The weighted-harmonic-mean L^p-norm interpolation inequality is not present as a named lemma in Mathlib. | No named weighted-harmonic-mean Lᵖ interpolation lemma found in Mathlib. |
modifiedLittlewood's inequality32d4848960c6
| Field | From #3189 | To #3706 |
|---|
| note | Littlewood's L^p interpolation inequality is not formalized in Mathlib. | Littlewood's three-exponent interpolation inequality is not present as a named lemma in Mathlib. |
modifiedLyapunov's inequalityf55b5177659b
| Field | From #3189 | To #3706 |
|---|
| note | `eLpNorm_le_eLpNorm_of_exponent_le` for `IsProbabilityMeasure` gives `‖f‖_p ≤ ‖f‖_q` when `p ≤ q`, which is Lyapunov's inequality on moments. | Verified: `eLpNorm_le_eLpNorm_of_exponent_le` (probability measure) yields Lyapunov's moment inequality. |
modifiedReverse Hölder inequality (two functions)8d5d9009d939
| Field | From #3189 | To #3706 |
|---|
| note | No reverse Hölder inequality is present in Mathlib. | Grep finds no reverse Hölder inequality in Mathlib. |
modifiedReverse Hölder inequality (multiple functions)8a7d3447f265
| Field | From #3189 | To #3706 |
|---|
| note | The multi-function reverse Hölder inequality is not formalized. | Multi-function reverse Hölder is not formalized in Mathlib. |
modifiedSymmetric form of Hölder's inequality130afd9c390e
| Field | From #3189 | To #3706 |
|---|
| note | The symmetric-form Hölder inequality for positive vectors is not formalized in Mathlib. | The symmetric-form Hölder inequality for positive vectors is not present in Mathlib. |
modifiedSymmetric Hölder for multiple vectorsa3f1fea622f1
| Field | From #3189 | To #3706 |
|---|
| note | Multi-vector symmetric Hölder is not formalized. | The multi-vector symmetric Hölder inequality is not present in Mathlib. |
modifiedConditional Hölder inequalitydb8d260ac662
| Field | From #3189 | To #3706 |
|---|
| note | Mathlib does not contain a conditional-expectation Hölder inequality. | No conditional-expectation Hölder inequality is present in Mathlib. |
modifiedHölder's inequality for increasing seminorms9ecc89f97b9f
| Field | From #3189 | To #3706 |
|---|
| note | The abstract Hölder inequality for increasing seminorms on a function algebra is not formalized. | The abstract Hölder inequality for increasing seminorms on a function algebra is not present in Mathlib. |
modifiedHölder divergences598225762d75
| Field | From #3189 | To #3706 |
|---|
| note | Hölder divergences (statistical dissimilarity measures) are not formalized in Mathlib. | Hölder divergences (statistical dissimilarity measures) are not present in Mathlib. |
addedPointwise product lies in L¹6eb6b848bdbd
addedL^q is the dual of L^p2737c82e78dc