Revision #1719 → #2190 · back to history
modifiedSedrakyan's inequalitycc0b8e71d715
| Field | From #1719 | To #2190 |
|---|
| mathlib.decl | sq_sum_div_le_sum_sq_div | Finset.sq_sum_div_le_sum_sq_div |
| note | `sq_sum_div_le_sum_sq_div` is documented as Sedrakyan's/Titu's/Engel's lemma: (∑fᵢ)²/∑gᵢ ≤ ∑ fᵢ²/gᵢ. | `Finset.sq_sum_div_le_sum_sq_div` is documented as Sedrakyan's/Titu's/Engel's lemma: (∑fᵢ)²/∑gᵢ ≤ ∑ fᵢ²/gᵢ. |
modifiedCauchy–Schwarz in the plane R²e68fe1091fed
| Field | From #1719 | To #2190 |
|---|
| mathlib.decl | sum_mul_sq_le_sq_mul_sq | Finset.sum_mul_sq_le_sq_mul_sq |
| note | The R² dot-product case is the two-term instance of the general finite-sum Cauchy–Schwarz `sum_mul_sq_le_sq_mul_sq`. | The R² dot-product case is the two-term instance of the general finite-sum Cauchy–Schwarz `Finset.sum_mul_sq_le_sq_mul_sq`. |
modifiedCauchy–Schwarz in Rⁿae08abc6b425
| Field | From #1719 | To #2190 |
|---|
| mathlib.decl | sum_mul_sq_le_sq_mul_sq | Finset.sum_mul_sq_le_sq_mul_sq |
| note | `sum_mul_sq_le_sq_mul_sq` is exactly (∑fᵢgᵢ)² ≤ (∑fᵢ²)(∑gᵢ²), the Cauchy–Schwarz inequality for the dot product on Rⁿ. | `Finset.sum_mul_sq_le_sq_mul_sq` is exactly (∑fᵢgᵢ)² ≤ (∑fᵢ²)(∑gᵢ²), the Cauchy–Schwarz inequality for the dot product on Rⁿ. |
modifiedCovariance inequalityb6f49dc06d57
| Field | From #1719 | To #2190 |
|---|
| mathlib.decl | isPosSemidef_covarianceBilinDual | ProbabilityTheory.isPosSemidef_covarianceBilinDual |
modifiedMantel's theorem82b7fa8e9d15
| Field | From #1719 | To #2190 |
|---|
| mathlib.decl | isTuranMaximal_iff_nonempty_iso_turanGraph | SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph |
modifiedHölder generalization0c5dd1753149
| Field | From #1719 | To #2190 |
|---|
| mathlib.decl | inner_le_Lp_mul_Lq | Real.inner_le_Lp_mul_Lq |
| note | `inner_le_Lp_mul_Lq` is Hölder's inequality ∑fᵢgᵢ ≤ (∑fᵢ^p)^(1/p)(∑gᵢ^q)^(1/q), generalizing Cauchy–Schwarz. | `Real.inner_le_Lp_mul_Lq` is Hölder's inequality ∑fᵢgᵢ ≤ (∑|fᵢ|^p)^(1/p)(∑|gᵢ|^q)^(1/q), generalizing Cauchy–Schwarz. |
addedInner product space1e4b6866acfa
addedCauchy–Schwarz: ⟪x,y⟫·⟪y,x⟫ ≤ ⟪x,x⟫·⟪y,y⟫d47d08b153ab
addedLinear dependence3d68d859e865
addedVariance of a random variable97deb2c929c6
addedCovariance of two random variables6dc538b60f9c
addedNorm of a bounded linear operator on a Banach space909548dceca5