Existing in Mathlib · Measure theory and analysis
Minkowski's Lᵖ Inequality
For exponent p at least 1, the extended Lᵖ size of the pointwise sum of two a.e.-strongly-measurable functions is no larger than the sum of their individual extended Lᵖ sizes.
- Lᵖ seminorm
- Minkowski inequality
- a.e.-strong measurability
- extended nonnegative reals
- essential supremum
- triangle inequality
Exact theorem
Exact Mathlib statement
theorem MeasureTheory.eLpNorm_add_le {α ε : Type*} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p : ℝ≥0∞} {μ : Measure α} {f g : α → ε} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hp1 : 1 ≤ p) : eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μThe theorem at a glance
Minkowski's Lᵖ inequality at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Minkowski's Lᵖ inequality at a glance
Detailed visual description
The poster states the exact eLpNorm inequality, keeps a.e.-strong measurability and the extended-nonnegative-real exponent visible, and summarizes Mathlib's two proof branches: essential-supremum subadditivity at p = ∞ and the finite-p integral Lᵖ inequality after rewriting through eLpNorm'. Its footer excludes finiteness, equality-case, and subunit-exponent claims.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Pointwise combination inside the joined size envelope
Detailed visual description
Six aligned cobalt diagonal-hatched inputs and six gold dotted inputs pair by position and merge into six emerald vertical-hatched outputs. Those outputs braid into one combined field and enter an emerald inner body wholly contained in a larger vessel split between the two input patterns. Dashed continuation cues avoid a finiteness claim, and the containment expresses a non-strict bound without printing the theorem inequality.
Why it matters
A mathematical landmark
Minkowski's inequality is the triangle inequality that makes Lᵖ analysis work for p at least 1. Mathlib's declaration is a useful exact endpoint because it includes the extended-valued eLp seminorm and handles the p = ∞ essential-supremum branch alongside finite exponents.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's extended eLp-seminorm triangle inequality. In the enclosing namespace context, f and g take values in an ESeminormedAddMonoid, p is an extended nonnegative real, and μ is a measure. A.e.-strong measurability of both functions and 1 ≤ p imply eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ. The declaration does not assume the seminorms are finite, characterize equality, turn the codomain into a finite-dimensional vector space, or give the constant-one inequality for 0 < p < 1.
- The selected declaration is the extended eLp-seminorm inequality for p : ℝ≥0∞ with 1 ≤ p; it is not a statement restricted to finite real p.
- The theorem does not assume or conclude that any eLp seminorm is finite, and it does not characterize the equality case.
- The selected declaration does not give the constant-one triangle inequality in the subunit range 0 < p < 1; Mathlib treats that range separately with a larger constant.
- The codomain scope is an ESeminormedAddMonoid, not specifically a finite-dimensional real or complex vector space.
- ProofAtlas is indexing an existing Mathlib theorem, and generated explanations and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
MeasureTheory.eLpNorm_add_lein mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.minkowski-lp-inequality.v001