feat (analysis/normed_space): Define real inner product space #1248

aceg00 · 2019-07-20T18:18:17Z

Define real inner product space and prove that it is a normed space. Next step is to define Hilbert space and prove the existence of orthogonal projection onto closed subspaces.

@amswerdlow defines complex inner product space in #840 . I think it may not be possible to treat the real and complex cases together, so I wrote a separate file.

The file discriminant.lean is the content of my previous PR #1245, and so it is temporary. People want me to do a bit more about solving quadratics, so I want to show the inner product space file for discussion while I work on quadratics.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

src/analysis/normed_space/real_inner_product.lean

The original definition introduces an instance loop. See Zulip talks: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ring.20tactic.20works.20at.20one.20place.2C.20fails.20at.20another

robertylewis · 2019-07-25T09:01:25Z

Could you update to meet the new documentation requirements? (https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/doc.md)

aceg00 · 2019-07-25T09:13:41Z

Hi @robertylewis,

I aimed to follow the new documentation requirements when I wrote the files. I think I must have did it incorrectly?

The file discriminant.lean is temporary. It is part of my previous PR #1245 . I tried to follow the doc requirements there.

robertylewis · 2019-07-25T09:23:48Z

Ah, I see. I think a header for discriminant.lean is all that's missing.

semorrison · 2019-07-25T21:56:16Z

I think we should have some discussion about a unified approach to real and complex normed/inner product/Hilbert spaces. Does something like this

import analysis.normed_space.basic

class scalars (α : Type) extends normed_field α :=
(embed_ℝ : ℝ → α)
(conj : α → α) -- TODO axioms about conj

instance embed_ℝ_coe (α : Type) [scalars α] : has_coe ℝ α :=
{ coe := scalars.embed_ℝ α }

variables (α : Type) [scalars α]

example : α := (1 : ℝ)

notation a `†`:120 := scalars.conj a

set_option class.instance_max_depth 34
class sesquilinear_space (𝕶 : Type) [scalars 𝕶] (α : Type*) [add_comm_group α] [vector_space 𝕶 α] :=
(inner_product : α → α → 𝕶)
(conj_symm : ∀ (x y : α), inner_product x y = (inner_product y x)†)
(linearity : ∀ (x y z : α), ∀ (a : 𝕶), inner_product (a • x + y) z = a * inner_product x z + inner_product y z)

class inner_product_space (𝕶 : Type) [scalars 𝕶] (α : Type*) [add_comm_group α] [vector_space 𝕶 α]
  extends sesquilinear_space 𝕶 α, normed_space 𝕶 α :=
(norm_sq : ∀ (x : α), inner_product x x = (norm x)^2)

get us off the ground?

Prove the existence of orthogonal projections onto complete subspaces in an inner product space.

aceg00 · 2019-07-31T09:54:03Z

Update : orthogonal projections onto complete subspaces

avigad

This looks like a good start on inner product spaces and projections!

avigad · 2019-08-03T02:13:11Z

src/algebra/ordered_field.lean

@@ -181,12 +181,18 @@ namespace nat

 variables {α : Type*} [linear_ordered_field α]

-lemma inv_pos_of_nat [linear_ordered_field α] {n : ℕ}  : 0 < ((n : α) + 1)⁻¹ :=
+lemma inv_pos_of_nat {n : ℕ} : 0 < ((n : α) + 1)⁻¹ :=


Can you get rid of the +1 and add the hypothesis n ≠ 0?

Sorry for the delay -- I was traveling for a few days. I am still not sure this is a great lemma to have in the library, and anyhow the name would be better as inv_of_nat_add_one_pos, but I don't feel strongly about it. I'll merge now.

avigad · 2019-08-03T02:13:39Z

src/algebra/ordered_field.lean

 inv_pos $ add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one

-lemma one_div_pos_of_nat [linear_ordered_field α] {n : ℕ} : 0 < 1 / ((n : α) + 1) :=


same comment here and below

src/algebra/quadratic_discriminant.lean

src/analysis/normed_space/real_inner_product.lean

avigad · 2019-08-03T02:27:22Z

src/order/conditionally_complete_lattice.lean

-/--When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is
-a linear order.-/
+/-- When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is
+a linear order. -/
 lemma exists_lt_of_lt_cSup (_ : s ≠ ∅) (_ : b < Sup s) : ∃a∈s, b < a :=


Why not give names to the hypotheses? That will guarantee that the theorem looks nice when users have to see it.

More than fifty hypotheses in this file have no name. Maybe it's better to add names in another PR.

avigad · 2019-08-08T00:36:58Z

src/algebra/ordered_field.lean

@@ -181,12 +181,18 @@ namespace nat

 variables {α : Type*} [linear_ordered_field α]

-lemma inv_pos_of_nat [linear_ordered_field α] {n : ℕ}  : 0 < ((n : α) + 1)⁻¹ :=
+lemma inv_pos_of_nat {n : ℕ} : 0 < ((n : α) + 1)⁻¹ :=


Sorry for the delay -- I was traveling for a few days. I am still not sure this is a great lemma to have in the library, and anyhow the name would be better as inv_of_nat_add_one_pos, but I don't feel strongly about it. I'll merge now.

…over-community#1248) * Inner product space * Change the definition of inner_product_space The original definition introduces an instance loop. See Zulip talks: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ring.20tactic.20works.20at.20one.20place.2C.20fails.20at.20another * Orthogonal Projection Prove the existence of orthogonal projections onto complete subspaces in an inner product space. * Fix names * small fixes

Inner product space

1d5150a

aceg00 requested a review from a team as a code owner July 20, 2019 18:18