Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
refactor(analysis/normed_space/real_inner_product): extend normed_sp…
Browse files Browse the repository at this point in the history 
…ace in the definition (#3060)

Currently, inner product spaces do not extend normed spaces, and a norm is constructed from the inner product. This makes it impossible to put an instance on reals, because it would lead to two non-defeq norms. We refactor inner product spaces to extend normed spaces, with the condition that the norm is equal (but maybe not defeq) to the square root of the inner product, to solve this issue.

The possibility to construct a norm from a well-behaved inner product is still given by a constructor `inner_product_space.of_core`.

We also register the inner product structure on a finite product of inner product spaces (not on the Pi type, which has the sup norm, but on `pi_Lp 2 one_le_two \alpha` which has the right norm).
  • Loading branch information
@sgouezel
sgouezel committed Jun 14, 2020
1 parent 85b8bdc commit 1f16da1
Show file tree
Hide file tree
Showing 2 changed files with 218 additions and 79 deletions.
295 changes: 217 additions & 78 deletions src/analysis/normed_space/real_inner_product.lean
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
/-
Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhouhang Zhou
Authors: Zhouhang Zhou, Sébastien Gouëzel
-/
import algebra.quadratic_discriminant
import analysis.special_functions.pow
import tactic.apply_fun
import tactic.monotonicity

import topology.metric_space.pi_Lp

/-!
# Inner Product Space
Expand Down Expand Up @@ -51,35 +50,198 @@ universes u v w

variables {α : Type u} {F : Type v} {G : Type w}


/-- Syntactic typeclass for types endowed with an inner product -/
class has_inner (α : Type*) := (inner : α → α → ℝ)

export has_inner (inner)

section prio

set_option default_priority 100 -- see Note [default priority]
-- see Note[vector space definition] for why we extend `module`.
/--
An inner product space is a real vector space with an additional operation called inner product.
Inner product spaces over complex vector space will be defined in another file.
The norm could be derived from the inner product, instead we require the existence of a norm and
the fact that it is equal to `sqrt (inner x x)` to be able to put instances on `ℝ` or product
spaces.
To construct a norm from an inner product, see `inner_product_space.of_core`.
-/
class inner_product_space (α : Type*) extends add_comm_group α, semimodule ℝ α, has_inner α :=
class inner_product_space (α : Type*) extends normed_group α, normed_space ℝ α, has_inner α :=
(norm_eq_sqrt_inner : ∀ (x : α), ∥x∥ = sqrt (inner x x))
(comm : ∀ x y, inner x y = inner y x)
(add_left : ∀ x y z, inner (x + y) z = inner x z + inner y z)
(smul_left : ∀ x y r, inner (r • x) y = r * inner x y)
end prio

/-!
### Constructing a normed space structure from a scalar product
In the definition of an inner product space, we require the existence of a norm, which is equal
(but maybe not defeq) to the square root of the scalar product. This makes it possible to put
an inner product space structure on spaces with a preexisting norm (for instance `ℝ`), with good
properties. However, sometimes, one would like to define the norm starting only from a well-behaved
scalar product. This is what we implement in this paragraph, starting from a structure
`inner_product_space.core` stating that we have a nice scalar product.
Our goal here is not to develop a whole theory with all the supporting API, as this will be done
below for `inner_product_space`. Instead, we implement the bare minimum to go as directly as
possible to the construction of the norm and the proof of the triangular inequality.
-/

/-- A structure requiring that a scalar product is positive definite and symmetric, from which one
can construct an `inner_product_space` instance in `inner_product_space.of_core`. -/
@[nolint has_inhabited_instance]
structure inner_product_space.core
(F : Type*) [add_comm_group F] [semimodule ℝ F] :=
(inner : F → F → ℝ)
(comm : ∀ x y, inner x y = inner y x)
(nonneg : ∀ x, 0 ≤ inner x x)
(definite : ∀ x, inner x x = 0 → x = 0)
(add_left : ∀ x y z, inner (x + y) z = inner x z + inner y z)
(smul_left : ∀ x y r, inner (r • x) y = r * inner x y)
end prio

/- We set `inner_product_space.core` to be a class as we will use it as such in the construction
of the normed space structure that it produces. However, all the instances we will use will be
local to this proof. -/
attribute [class] inner_product_space.core

namespace inner_product_space.of_core

variables [add_comm_group F] [semimodule ℝ F] [c : inner_product_space.core F]
include c

/-- Inner product constructed from an `inner_product_space.core` structure -/
def to_has_inner : has_inner F :=
{ inner := c.inner }

local attribute [instance] to_has_inner

lemma inner_comm (x y : F) : inner x y = inner y x := c.comm x y

lemma inner_add_left (x y z : F) : inner (x + y) z = inner x z + inner y z :=
c.add_left _ _ _

lemma inner_add_right (x y z : F) : inner x (y + z) = inner x y + inner x z :=
by { rw [inner_comm, inner_add_left], simp [inner_comm] }

lemma inner_smul_left (x y : F) (r : ℝ) : inner (r • x) y = r * inner x y :=
c.smul_left _ _ _

lemma inner_smul_right (x y : F) (r : ℝ) : inner x (r • y) = r * inner x y :=
by { rw [inner_comm, inner_smul_left, inner_comm] }

/-- Norm constructed from an `inner_product_space.core` structure, defined to be the square root
of the scalar product. -/
def to_has_norm : has_norm F :=
{ norm := λ x, sqrt (inner x x) }

local attribute [instance] to_has_norm

lemma norm_eq_sqrt_inner (x : F) : ∥x∥ = sqrt (inner x x) := rfl

lemma inner_self_eq_norm_square (x : F) : inner x x = ∥x∥ * ∥x∥ :=
(mul_self_sqrt (c.nonneg _)).symm

/-- Expand `inner (x + y) (x + y)` -/
lemma inner_add_add_self (x y : F) : inner (x + y) (x + y) = inner x x + 2 * inner x y + inner y y :=
by simpa [inner_add_left, inner_add_right, two_mul, add_assoc] using inner_comm _ _

/-- Cauchy–Schwarz inequality -/
lemma inner_mul_inner_self_le (x y : F) : inner x y * inner x y ≤ inner x x * inner y y :=
begin
have : ∀ t, 0 ≤ inner y y * t * t + 2 * inner x y * t + inner x x, from
assume t, calc
0 ≤ inner (x+t•y) (x+t•y) : c.nonneg _
... = inner y y * t * t + 2 * inner x y * t + inner x x :
by { simp only [inner_add_add_self, inner_smul_right, inner_smul_left], ring },
have := discriminant_le_zero this, rw discrim at this,
have h : (2 * inner x y)^2 - 4 * inner y y * inner x x =
4 * (inner x y * inner x y - inner x x * inner y y) := by ring,
rw h at this,
linarith
end

/-- Cauchy–Schwarz inequality with norm -/
lemma abs_inner_le_norm (x y : F) : abs (inner x y) ≤ ∥x∥ * ∥y∥ :=
nonneg_le_nonneg_of_squares_le (mul_nonneg (sqrt_nonneg _) (sqrt_nonneg _))
begin
rw abs_mul_abs_self,
have : ∥x∥ * ∥y∥ * (∥x∥ * ∥y∥) = inner x x * inner y y,
simp only [inner_self_eq_norm_square], ring,
rw this,
exact inner_mul_inner_self_le _ _
end

/-- Normed group structure constructed from an `inner_product_space.core` structure. -/
def to_normed_group : normed_group F :=
normed_group.of_core F
{ norm_eq_zero_iff := assume x,
begin
split,
{ assume h,
rw [norm_eq_sqrt_inner, sqrt_eq_zero] at h,
{ exact c.definite x h },
{ exact c.nonneg x } },
{ rintros rfl,
have : inner ((0 : ℝ) • (0 : F)) 0 = 0 * inner (0 : F) 0 := inner_smul_left _ _ _,
simp at this,
simp [norm, this] }
end,
norm_neg := assume x,
begin
have A : (- (1 : ℝ)) • x = -x, by simp,
rw [norm_eq_sqrt_inner, norm_eq_sqrt_inner, ← A, inner_smul_left, inner_smul_right],
simp,
end,
triangle := assume x y,
begin
have := calc
∥x + y∥ * ∥x + y∥ = inner (x + y) (x + y) : by rw inner_self_eq_norm_square
... = inner x x + 2 * inner x y + inner y y : inner_add_add_self _ _
... ≤ inner x x + 2 * (∥x∥ * ∥y∥) + inner y y :
by linarith [abs_inner_le_norm x y, le_abs_self (inner x y)]
... = (∥x∥ + ∥y∥) * (∥x∥ + ∥y∥) : by { simp only [inner_self_eq_norm_square], ring },
exact nonneg_le_nonneg_of_squares_le (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this
end }

local attribute [instance] to_normed_group

/-- Normed space structure constructed from an `inner_product_space.core` structure. -/
def to_normed_space : normed_space ℝ F :=
{ norm_smul_le := assume r x, le_of_eq $
begin
have A : 0 ≤ ∥r∥ * ∥x∥ := mul_nonneg (abs_nonneg _) (sqrt_nonneg _),
rw [norm_eq_sqrt_inner, sqrt_eq_iff_mul_self_eq _ A,
inner_smul_left, inner_smul_right, inner_self_eq_norm_square],
{ calc
abs(r) * ∥x∥ * (abs(r) * ∥x∥) = (abs(r) * abs(r)) * (∥x∥ * ∥x∥) : by ring
... = r * (r * (∥x∥ * ∥x∥)) : by { rw abs_mul_abs_self, ring } },
{ exact c.nonneg _ }
end }

end inner_product_space.of_core

/-- Given an `inner_product_space.core` structure on a space, one can use it to turn the space into
an inner product space, constructing the norm out of the inner product. -/
def inner_product_space.of_core [add_comm_group F] [semimodule ℝ F]
(c : inner_product_space.core F) : inner_product_space F :=
begin
letI : normed_group F := @inner_product_space.of_core.to_normed_group F _ _ c,
letI : normed_space ℝ F := @inner_product_space.of_core.to_normed_space F _ _ c,
exact { norm_eq_sqrt_inner := λ x, rfl, .. c }
end

/-! ### Properties of inner product spaces -/

variables [inner_product_space α]

export inner_product_space (norm_eq_sqrt_inner)

section basic_properties

lemma inner_comm (x y : α) : inner x y = inner y x := inner_product_space.comm x y

lemma inner_self_nonneg {x : α} : 0 ≤ inner x x := inner_product_space.nonneg _

lemma inner_add_left {x y z : α} : inner (x + y) z = inner x z + inner y z :=
inner_product_space.add_left _ _ _

Expand All @@ -99,7 +261,18 @@ by { rw [← zero_smul ℝ (0:α), inner_smul_left, zero_mul] }
by { rw [inner_comm, inner_zero_left] }

@[simp] lemma inner_self_eq_zero {x : α} : inner x x = 0 ↔ x = 0 :=
iff.intro (inner_product_space.definite _) (by { rintro rfl, exact inner_zero_left })
⟨λ h, by simpa [h] using norm_eq_sqrt_inner x, λ h, by simp [h]⟩

lemma inner_self_nonneg {x : α} : 0 ≤ inner x x :=
begin
classical,
by_cases h : x = 0,
{ simp [h] },
{ have : 0 < sqrt (inner x x),
{ rw ← norm_eq_sqrt_inner,
exact norm_pos_iff.mpr h },
exact le_of_lt (sqrt_pos.1 this) }
end

@[simp] lemma inner_self_nonpos {x : α} : inner x x ≤ 0 ↔ x = 0 :=
⟨λ h, inner_self_eq_zero.1 (le_antisymm h inner_self_nonneg),
Expand Down Expand Up @@ -154,14 +327,8 @@ end basic_properties

section norm

/-- An inner product naturally induces a norm. -/
@[priority 100] -- see Note [lower instance priority]
instance inner_product_space_has_norm : has_norm α := ⟨λx, sqrt (inner x x)⟩

lemma norm_eq_sqrt_inner {x : α} : ∥x∥ = sqrt (inner x x) := rfl

lemma inner_self_eq_norm_square (x : α) : inner x x = ∥x∥ * ∥x∥ :=
(mul_self_sqrt inner_self_nonneg).symm
by { rw norm_eq_sqrt_inner, exact (mul_self_sqrt inner_self_nonneg).symm }

/-- Expand the square -/
lemma norm_add_pow_two {x y : α} : ∥x + y∥^2 = ∥x∥^2 + 2 * inner x y + ∥y∥^2 :=
Expand All @@ -181,7 +348,7 @@ by { repeat {rw [← pow_two]}, exact norm_sub_pow_two }

/-- Cauchy–Schwarz inequality with norm -/
lemma abs_inner_le_norm (x y : α) : abs (inner x y) ≤ ∥x∥ * ∥y∥ :=
nonneg_le_nonneg_of_squares_le (mul_nonneg (sqrt_nonneg _) (sqrt_nonneg _))
nonneg_le_nonneg_of_squares_le (mul_nonneg (norm_nonneg _) (norm_nonneg _))
begin
rw abs_mul_abs_self,
have : ∥x∥ * ∥y∥ * (∥x∥ * ∥y∥) = inner x x * inner y y,
Expand Down Expand Up @@ -247,38 +414,6 @@ lemma norm_sub_square_eq_norm_square_add_norm_square {x y : α} (h : inner x y =
∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ :=
(norm_sub_square_eq_norm_square_add_norm_square_iff_inner_eq_zero x y).2 h

/-- An inner product space forms a normed group w.r.t. its associated norm. -/
@[priority 100] -- see Note [lower instance priority]
instance inner_product_space_is_normed_group : normed_group α :=
normed_group.of_core α
{ norm_eq_zero_iff := assume x, iff.intro
(λ h : sqrt (inner x x) = 0, inner_self_eq_zero.1 $ (sqrt_eq_zero inner_self_nonneg).1 h )
(by {rintro rfl, show sqrt (inner (0:α) 0) = 0, simp }),
triangle := assume x y,
begin
have := calc
∥x + y∥ * ∥x + y∥ = inner (x + y) (x + y) : (inner_self_eq_norm_square _).symm
... = inner x x + 2 * inner x y + inner y y : inner_add_add_self
... ≤ inner x x + 2 * (∥x∥ * ∥y∥) + inner y y :
by linarith [abs_inner_le_norm x y, le_abs_self (inner x y)]
... = (∥x∥ + ∥y∥) * (∥x∥ + ∥y∥) : by { simp only [inner_self_eq_norm_square], ring },
exact nonneg_le_nonneg_of_squares_le (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this
end,
norm_neg := λx, show sqrt (inner (-x) (-x)) = sqrt (inner x x), by simp }

/-- An inner product space forms a normed space over reals w.r.t. its associated norm. -/
instance inner_product_space_is_normed_space : normed_space ℝ α :=
{ norm_smul_le := assume r x, le_of_eq $
begin
rw [norm_eq_sqrt_inner, sqrt_eq_iff_mul_self_eq,
inner_smul_left, inner_smul_right, inner_self_eq_norm_square],
exact calc
abs(r) * ∥x∥ * (abs(r) * ∥x∥) = (abs(r) * abs(r)) * (∥x∥ * ∥x∥) : by ring
... = r * (r * (∥x∥ * ∥x∥)) : by { rw abs_mul_abs_self, ring },
exact inner_self_nonneg,
exact mul_nonneg (abs_nonneg _) (sqrt_nonneg _)
end }

/-- The inner product of two vectors, divided by the product of their
norms, has absolute value at most 1. -/
lemma abs_inner_div_norm_mul_norm_le_one (x y : α) : abs (inner x y / (∥x∥ * ∥y∥)) ≤ 1 :=
Expand Down Expand Up @@ -440,58 +575,62 @@ end

end norm

/-! ### Inner product space structure on product spaces -/

-- TODO [Lean 3.15]: drop some of these `show`s
/-- If `ι` is a finite type and each space `f i`, `i : ι`, is an inner product space,
then `Π i, f i` is an inner product space as well. This is not an instance to avoid conflict
with the default instance for the norm on `Π i, f i`. -/
def pi.inner_product_space (ι : Type*) [fintype ι] (f : ι → Type*) [Π i, inner_product_space (f i)] :
inner_product_space (Π i, f i) :=
then `Π i, f i` is an inner product space as well. Since `Π i, f i` is endowed with the sup norm,
we use instead `pi_Lp 2 one_le_two f` for the product space, which is endowed with the `L^2` norm.
-/
instance pi_Lp.inner_product_space
(ι : Type*) [fintype ι] (f : ι → Type*) [Π i, inner_product_space (f i)] :
inner_product_space (pi_Lp 2 one_le_two f) :=
{ inner := λ x y, ∑ i, inner (x i) (y i),
comm := λ x y, finset.sum_congr rfl $ λ i hi, inner_comm (x i) (y i),
nonneg := λ x, show (0:ℝ) ≤ ∑ i, inner (x i) (x i),
from finset.sum_nonneg (λ i hi, inner_self_nonneg),
definite := λ x h, begin
have : ∀ i ∈ (finset.univ : finset ι), 0 ≤ inner (x i) (x i) := λ i hi, inner_self_nonneg,
simpa [inner, finset.sum_eq_zero_iff_of_nonneg this, function.funext_iff] using h,
norm_eq_sqrt_inner := begin
assume x,
have : (2 : ℝ)⁻¹ * 2 = 1, by norm_num,
simp [inner, pi_Lp.norm_eq, norm_eq_sqrt_inner, sqrt_eq_rpow, ← rpow_mul (inner_self_nonneg),
this],
end,
comm := λ x y, finset.sum_congr rfl $ λ i hi, inner_comm (x i) (y i),
add_left := λ x y z,
show ∑ i, inner (x i + y i) (z i) = ∑ i, inner (x i) (z i) + ∑ i, inner (y i) (z i),
by simp only [inner_add_left, finset.sum_add_distrib],
smul_left := λ x y r,
show ∑ (i : ι), inner (r • x i) (y i) = r * ∑ i, inner (x i) (y i),
by simp only [finset.mul_sum, inner_smul_left] }

/-- The set of real numbers is an inner product space. While the norm given by this definition
is equal to the default norm `∥x∥ = abs x`, it is not definitionally equal, so we don't turn this
definition into an instance.
TODO: do the same trick as with `metric_space` and `emetric_space`? -/
def real.inner_product_space : inner_product_space ℝ :=
/-- The type of real numbers is an inner product space. -/
instance real.inner_product_space : inner_product_space ℝ :=
{ inner := (*),
norm_eq_sqrt_inner := λ x, by simp [inner, norm_eq_abs, sqrt_mul_self_eq_abs],
comm := mul_comm,
nonneg := mul_self_nonneg,
definite := λ x, mul_self_eq_zero.1,
add_left := add_mul,
smul_left := λ _ _ _, mul_assoc _ _ _ }

section instances
/-- The standard Euclidean space, functions on a finite type. For an `n`-dimensional space
use `euclidean_space (fin n)`. -/
@[derive add_comm_group, nolint unused_arguments]
def euclidean_space (n : Type*) [fintype n] : Type* := n → ℝ

variables {n : Type*} [fintype n]
@[reducible, nolint unused_arguments]
def euclidean_space (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), ℝ)

instance : inhabited (euclidean_space n) := ⟨0⟩
section pi_Lp
local attribute [reducible] pi_Lp
variables (n : Type*) [fintype n]

local attribute [instance] real.inner_product_space
instance : finite_dimensional ℝ (euclidean_space n) :=
by apply_instance

instance : inner_product_space (euclidean_space n) := pi.inner_product_space n (λ _, ℝ)
@[simp] lemma findim_euclidean_space :
finite_dimensional.findim ℝ (euclidean_space n) = fintype.card n :=
by simp

lemma euclidean_space.inner_def (x y : euclidean_space n) : inner x y = ∑ i, x i * y i := rfl
lemma findim_euclidean_space_fin {n : ℕ} :
finite_dimensional.findim ℝ (euclidean_space (fin n)) = n :=
by simp

end instances
end pi_Lp

/-! ### Orthogonal projection in inner product spaces -/
section orthogonal

open filter
Expand Down
Loading

0 comments on commit 1f16da1

Please sign in to comment.