Geometry of finite-dimensional ℓ^p spaces

DefinitionThe vector \((1, 1)\) in \(\ell^p_2\)#✓fully proved

For \(p \in [0, \infty]\), write \(\ell^p_2\) for the space \(\mathbb{R}^2\) regarded as the \(\ell^p\) product of two copies of \(\mathbb{R}\) (normed by the \(\ell^p\) norm when \(p \ge 1\)). The vector \(u_p \in \ell^p_2\) is \((1, 1)\), that is, \(e_0 + e_1\), where \(e_0 = (1, 0)\) and \(e_1 = (0, 1)\) are the standard basis vectors.

noncomputable def lpTwoPlus (p : ENNReal) : PiLp p (fun _ : Fin 2 => ℝ) :=
  PiLp.single p 0 1 + PiLp.single p 1 1

Used by 12

Used bySum of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\) · Difference of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\) · Norm of \((1, 1) + (1, -1)\) in \(\ell^p_2\) · The \(\ell^p\) norm of \((1, 1)\) for finite \(p\) · The \(\ell^\infty\) norm of \((1, 1)\) · The squared \(\ell^p\) norm of \((1, 1)\) for finite \(p\) · The difference of the parallelogram witnesses has norm two · The \(\ell^p\) norm on \(\mathbb{R}^2\) comes from no inner product unless \(p = 2\) · Two distinct \(\ell^1\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint · Two distinct \(\ell^\infty\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint · The parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm · The parallelogram law fails on \(\mathbb{R}^2\) with the \(\ell^p\) norm for \(p \neq 2\)

DefinitionThe vector \((1, -1)\) in \(\ell^p_2\)#✓fully proved

For \(p \in [0, \infty]\), write \(\ell^p_2\) for the space \(\mathbb{R}^2\) regarded as the \(\ell^p\) product of two copies of \(\mathbb{R}\) (normed by the \(\ell^p\) norm when \(p \ge 1\)). The vector \(v_p \in \ell^p_2\) is \((1, -1)\), that is, \(e_0 - e_1\), where \(e_0 = (1, 0)\) and \(e_1 = (0, 1)\) are the standard basis vectors.

noncomputable def lpTwoMinus (p : ENNReal) : PiLp p (fun _ : Fin 2 => ℝ) :=
  PiLp.single p 0 1 - PiLp.single p 1 1

Used by 10

Used bySum of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\) · Difference of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\) · Norm of \((1, 1) + (1, -1)\) in \(\ell^p_2\) · The \(\ell^p\) norm of \((1, -1)\) for finite \(p\) · The \(\ell^\infty\) norm of \((1, -1)\) · The difference of the parallelogram witnesses has norm two · The \(\ell^p\) norm on \(\mathbb{R}^2\) comes from no inner product unless \(p = 2\) · Two distinct \(\ell^\infty\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint · The parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm · The parallelogram law fails on \(\mathbb{R}^2\) with the \(\ell^p\) norm for \(p \neq 2\)

TheoremSum of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\)#✓fully proved

For every \(p \in [0, \infty]\), write \(\ell^p_2\) for the space \(\mathbb{R}^2\) regarded as the \(\ell^p\) product of two copies of \(\mathbb{R}\). The vectors \(u_p = (1, 1)\) and \(v_p = (1, -1)\) of \(\ell^p_2\) satisfy \(u_p + v_p = 2 e_0\), where \(e_0 = (1, 0)\) is the first standard basis vector.

theorem lpTwoPlus_add_lpTwoMinus :
    lpTwoPlus p + lpTwoMinus p = (2 : ℝ) • PiLp.single p 0 (1 : ℝ)

Uses 2 · Used by 2

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\)

Used byNorm of \((1, 1) + (1, -1)\) in \(\ell^p_2\) · Two distinct \(\ell^\infty\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint

TheoremDifference of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\)#✓fully proved

For every \(p \in [0, \infty]\), write \(\ell^p_2\) for the space \(\mathbb{R}^2\) regarded as the \(\ell^p\) product of two copies of \(\mathbb{R}\). The vectors \(u_p = (1, 1)\) and \(v_p = (1, -1)\) of \(\ell^p_2\) satisfy \(u_p - v_p = 2 e_1\), where \(e_1 = (0, 1)\) is the second standard basis vector.

theorem lpTwoPlus_sub_lpTwoMinus :
    lpTwoPlus p - lpTwoMinus p = (2 : ℝ) • PiLp.single p 1 (1 : ℝ)

Uses 2 · Used by 1

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\)

Used byThe difference of the parallelogram witnesses has norm two

TheoremNorm of \((1, 1) + (1, -1)\) in \(\ell^p_2\)#✓fully proved

For every \(p \in [1, \infty]\), let \(\ell^p_2\) be \(\mathbb{R}^2\) with the \(\ell^p\) norm, and let \(u_p = (1, 1)\) and \(v_p = (1, -1)\). Then \(\|u_p + v_p\| = 2\).

theorem norm_add_lpTwo : ‖lpTwoPlus p + lpTwoMinus p‖ = 2

Uses 3 · Used by 1

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\)

Proof usesSum of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\)

Used byThe parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

TheoremThe difference of the parallelogram witnesses has norm two#✓fully proved

For every extended real \(p \in [1, \infty]\), in \(\mathbb{R}^2\) with the \(\ell^p\) norm the vectors \(u = (1, 1)\) and \(v = (1, -1)\) satisfy \(\|u - v\| = 2\).

theorem norm_sub_lpTwo : ‖lpTwoPlus p - lpTwoMinus p‖ = 2

Uses 3 · Used by 1

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\)

Proof usesDifference of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\)

Used byThe parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

TheoremThe \(\ell^p\) norm of \((1, 1)\) for finite \(p\)#✓fully proved

For every real \(p\) with \(1 \le p < \infty\), the vector \((1, 1)\) of \(\mathbb{R}^2\) has \(\ell^p\) norm \(\|(1, 1)\|_p = 2^{1/p}\), where \(\|(x, y)\|_p = (|x|^p + |y|^p)^{1/p}\).

theorem norm_lpTwoPlus_of_ne_top (hp : p ≠ ⊤) :
    ‖lpTwoPlus p‖ = (2 : ℝ) ^ (1 / p.toReal)

Uses 1 · Used by 3

Statement usesThe vector \((1, 1)\) in \(\ell^p_2\)

Used byThe squared \(\ell^p\) norm of \((1, 1)\) for finite \(p\) · Two distinct \(\ell^1\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint · The parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

TheoremThe \(\ell^p\) norm of \((1, -1)\) for finite \(p\)#✓fully proved

For every real \(p\) with \(1 \le p < \infty\), the vector \((1, -1)\) of \(\mathbb{R}^2\) has \(\ell^p\) norm \(\|(1, -1)\|_p = 2^{1/p}\), where \(\|(x, y)\|_p = (|x|^p + |y|^p)^{1/p}\).

theorem norm_lpTwoMinus_of_ne_top (hp : p ≠ ⊤) :
    ‖lpTwoMinus p‖ = (2 : ℝ) ^ (1 / p.toReal)

Uses 1 · Used by 1

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\)

Used byThe parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

TheoremThe \(\ell^\infty\) norm of \((1, 1)\)#✓fully proved

In \(\mathbb{R}^2\) with the \(\ell^\infty\) norm \(\|(x, y)\|_\infty = \max(|x|, |y|)\), the vector \((1, 1)\) has norm \(\|(1, 1)\|_\infty = 1\).

theorem norm_lpTwoPlus_top : ‖lpTwoPlus (⊤ : ENNReal)‖ = 1

Uses 1 · Used by 2

Statement usesThe vector \((1, 1)\) in \(\ell^p_2\)

Used byTwo distinct \(\ell^\infty\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint · The parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

TheoremThe \(\ell^\infty\) norm of \((1, -1)\)#✓fully proved

In \(\mathbb{R}^2\) with the \(\ell^\infty\) norm \(\|(x, y)\|_\infty = \max(|x|, |y|)\), the vector \((1, -1)\) has norm \(\|(1, -1)\|_\infty = 1\).

theorem norm_lpTwoMinus_top : ‖lpTwoMinus (⊤ : ENNReal)‖ = 1

Uses 1 · Used by 2

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\)

Used byTwo distinct \(\ell^\infty\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint · The parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

TheoremThe squared \(\ell^p\) norm of \((1, 1)\) for finite \(p\)#✓fully proved

For every real \(p\) with \(1 \le p < \infty\), the vector \((1, 1)\) of \(\mathbb{R}^2\) satisfies \(\|(1, 1)\|_p^2 = 2^{2/p}\), where \(\|(x, y)\|_p = (|x|^p + |y|^p)^{1/p}\) is the \(\ell^p\) norm.

theorem norm_sq_lpTwoPlus_of_ne_top (hp : p ≠ ⊤) :
    ‖lpTwoPlus p‖ ^ 2 = (2 : ℝ) ^ ((2 : ℝ) / p.toReal)

Uses 2 · Used by 1

Statement usesThe vector \((1, 1)\) in \(\ell^p_2\)

Proof usesThe \(\ell^p\) norm of \((1, 1)\) for finite \(p\)

Used byThe parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

TheoremThe parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm#✓fully proved

Let \(p \in [1, \infty]\) and equip \(\mathbb{R}^2\) with the \(\ell^p\) norm. The vectors \(u = (1, 1)\) and \(v = (1, -1)\) satisfy \(\|u + v\|^2 + \|u - v\|^2 = 2 (\|u\|^2 + \|v\|^2)\) if and only if \(p = 2\).

theorem parallelogram_eq_iff_piLp_two :
    ‖lpTwoPlus p + lpTwoMinus p‖ ^ 2 + ‖lpTwoPlus p - lpTwoMinus p‖ ^ 2 =
        2 * (‖lpTwoPlus p‖ ^ 2 + ‖lpTwoMinus p‖ ^ 2) ↔ p = 2

Uses 9 · Used by 1

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\)

Proof usesNorm of \((1, 1) + (1, -1)\) in \(\ell^p_2\) · The \(\ell^p\) norm of \((1, -1)\) for finite \(p\) · The \(\ell^\infty\) norm of \((1, -1)\) · The \(\ell^p\) norm of \((1, 1)\) for finite \(p\) · The \(\ell^\infty\) norm of \((1, 1)\) · The squared \(\ell^p\) norm of \((1, 1)\) for finite \(p\) · The difference of the parallelogram witnesses has norm two

Used byThe parallelogram law fails on \(\mathbb{R}^2\) with the \(\ell^p\) norm for \(p \neq 2\)

TheoremThe parallelogram law fails on \(\mathbb{R}^2\) with the \(\ell^p\) norm for \(p \neq 2\)#✓fully proved

Let \(p \in [1, \infty]\) with \(p \neq 2\) and equip \(\mathbb{R}^2\) with the \(\ell^p\) norm. Then the vectors \(u = (1, 1)\) and \(v = (1, -1)\) satisfy \(\|u + v\|^2 + \|u - v\|^2 \neq 2 (\|u\|^2 + \|v\|^2)\).

theorem parallelogram_fails_piLp_two (hp : p ≠ 2) :
    ‖lpTwoPlus p + lpTwoMinus p‖ ^ 2 + ‖lpTwoPlus p - lpTwoMinus p‖ ^ 2 ≠
      2 * (‖lpTwoPlus p‖ ^ 2 + ‖lpTwoMinus p‖ ^ 2)

Uses 3 · Used by 1

Statement usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\)

Proof usesThe parallelogram law for \((1, 1)\) and \((1, -1)\) holds only for the \(\ell^2\) norm

Used byThe \(\ell^p\) norm on \(\mathbb{R}^2\) comes from no inner product unless \(p = 2\)

TheoremThe \(\ell^p\) norm on \(\mathbb{R}^2\) comes from no inner product unless \(p = 2\)#✓fully proved

Let \(p \in [1, \infty]\) with \(p \neq 2\). Then the normed space \(\mathbb{R}^2\) with the \(\ell^p\) norm carries no real inner product space structure, that is, there is no real inner product with \(\langle x, x \rangle = \|x\|^2\) for every \(x\).

Any such inner product would satisfy the parallelogram law, which fails for \((1, 1)\) and \((1, -1)\).

theorem not_innerProductSpace_piLp_two (hp : p ≠ 2) :
    ¬ Nonempty (InnerProductSpace ℝ (PiLp p (fun _ : Fin 2 => ℝ)))

Uses 3

Proof usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\) · The parallelogram law fails on \(\mathbb{R}^2\) with the \(\ell^p\) norm for \(p \neq 2\)

TheoremMidpoints of distinct \(\ell^p\) unit vectors in \(\mathbb{R}^2\) have norm less than one#✓fully proved

Let \(1 < p < \infty\) and equip \(\mathbb{R}^2\) with the \(\ell^p\) norm. If \(x \neq y\) are vectors with \(\|x\| = \|y\| = 1\), then \(\|\tfrac{1}{2} (x + y)\| < 1\).

theorem piLp_two_strictConvex (hp1 : 1 < p.toReal) (hp : p ≠ ⊤)
    (x y : PiLp p (fun _ : Fin 2 => ℝ)) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (hxy : x ≠ y) :
    ‖(1 / 2 : ℝ) • (x + y)‖ < 1

Used by 1

Used by\(\mathbb{R}^2\) with the \(\ell^p\) norm is strictly convex for \(1 < p < \infty\)

Theorem\(\mathbb{R}^2\) with the \(\ell^p\) norm is strictly convex for \(1 < p < \infty\)#✓fully proved

For \(1 < p < \infty\), the real normed space \(\mathbb{R}^2\) with the \(\ell^p\) norm is a strictly convex space: every closed ball of positive radius centred at the origin is a strictly convex set.

theorem strictConvexSpace_piLp_two (hp1 : 1 < p.toReal) (hp : p ≠ ⊤) :
    StrictConvexSpace ℝ (PiLp p (fun _ : Fin 2 => ℝ))

Uses 1

Proof usesMidpoints of distinct \(\ell^p\) unit vectors in \(\mathbb{R}^2\) have norm less than one

TheoremTwo distinct \(\ell^1\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint#✓fully proved

In \(\mathbb{R}^2\) with the \(\ell^1\) norm there exist vectors \(x \neq y\) with \(\|x\| = \|y\| = 1\) and \(\|\tfrac{1}{2} (x + y)\| = 1\).

For example, the unit vectors \((1, 0)\) and \((0, 1)\) have midpoint \((1/2, 1/2)\) of norm \(1\).

theorem not_strictConvex_piLp_two_one :
    ∃ x y : PiLp (1 : ENNReal) (fun _ : Fin 2 => ℝ), ‖x‖ = 1 ∧ ‖y‖ = 1 ∧ x ≠ y ∧
      ‖(1 / 2 : ℝ) • (x + y)‖ = 1

Uses 2 · Used by 1

Proof usesThe vector \((1, 1)\) in \(\ell^p_2\) · The \(\ell^p\) norm of \((1, 1)\) for finite \(p\)

Used by\(\mathbb{R}^2\) with the \(\ell^1\) norm is not strictly convex

Theorem\(\mathbb{R}^2\) with the \(\ell^1\) norm is not strictly convex#✓fully proved

The real normed space \(\mathbb{R}^2\) with the \(\ell^1\) norm is not a strictly convex space: not every closed ball of positive radius centred at the origin is a strictly convex set.

theorem not_strictConvexSpace_piLp_two_one :
    ¬ StrictConvexSpace ℝ (PiLp (1 : ENNReal) (fun _ : Fin 2 => ℝ))

Uses 1

Proof usesTwo distinct \(\ell^1\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint

TheoremTwo distinct \(\ell^\infty\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint#✓fully proved

In \(\mathbb{R}^2\) with the \(\ell^\infty\) norm there exist vectors \(x \neq y\) with \(\|x\| = \|y\| = 1\) and \(\|\tfrac{1}{2} (x + y)\| = 1\).

For example, the unit vectors \((1, 1)\) and \((1, -1)\) have midpoint \((1, 0)\) of norm \(1\).

theorem not_strictConvex_piLp_two_top :
    ∃ x y : PiLp (⊤ : ENNReal) (fun _ : Fin 2 => ℝ), ‖x‖ = 1 ∧ ‖y‖ = 1 ∧ x ≠ y ∧
      ‖(1 / 2 : ℝ) • (x + y)‖ = 1

Uses 5 · Used by 1

Proof usesThe vector \((1, -1)\) in \(\ell^p_2\) · The vector \((1, 1)\) in \(\ell^p_2\) · Sum of \((1, 1)\) and \((1, -1)\) in \(\ell^p_2\) · The \(\ell^\infty\) norm of \((1, -1)\) · The \(\ell^\infty\) norm of \((1, 1)\)

Used by\(\mathbb{R}^2\) with the \(\ell^\infty\) norm is not strictly convex

Theorem\(\mathbb{R}^2\) with the \(\ell^\infty\) norm is not strictly convex#✓fully proved

The real normed space \(\mathbb{R}^2\) with the \(\ell^\infty\) norm is not a strictly convex space: not every closed ball of positive radius centred at the origin is a strictly convex set.

theorem not_strictConvexSpace_piLp_two_top :
    ¬ StrictConvexSpace ℝ (PiLp (⊤ : ENNReal) (fun _ : Fin 2 => ℝ))

Uses 1

Proof usesTwo distinct \(\ell^\infty\) unit vectors in \(\mathbb{R}^2\) with a unit midpoint

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.