From 9ceb1141fab68a2cd3ec27621018539bf1139d87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Thu, 1 Oct 2020 07:41:14 +0000 Subject: [PATCH] feat(analysis/normed_space/inner_product): Define the inner product based on `is_R_or_C` (#4057) --- src/analysis/normed_space/basic.lean | 3 + src/analysis/normed_space/hahn_banach.lean | 4 +- src/analysis/normed_space/inner_product.lean | 1628 +++++++++++++++++ .../normed_space/real_inner_product.lean | 1186 ------------ src/data/complex/is_R_or_C.lean | 121 +- src/geometry/euclidean/basic.lean | 106 +- src/geometry/euclidean/circumcenter.lean | 16 +- src/geometry/euclidean/monge_point.lean | 10 +- src/geometry/euclidean/triangle.lean | 69 +- src/geometry/manifold/instances/real.lean | 44 +- src/linear_algebra/sesquilinear_form.lean | 18 + src/ring_theory/algebra.lean | 10 - 12 files changed, 1866 insertions(+), 1349 deletions(-) create mode 100644 src/analysis/normed_space/inner_product.lean delete mode 100644 src/analysis/normed_space/real_inner_product.lean diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean index 851279e1ae3de..970c001a8b4bc 100644 --- a/src/analysis/normed_space/basic.lean +++ b/src/analysis/normed_space/basic.lean @@ -812,6 +812,9 @@ begin rwa [ne.def, norm_eq_zero] } end +@[simp] lemma abs_norm_eq_norm (z : β) : abs ∥z∥ = ∥z∥ := + (abs_eq (norm_nonneg z)).mpr (or.inl rfl) + lemma dist_smul [normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y := by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub] diff --git a/src/analysis/normed_space/hahn_banach.lean b/src/analysis/normed_space/hahn_banach.lean index 47603325e7990..eaf28a444b970 100644 --- a/src/analysis/normed_space/hahn_banach.lean +++ b/src/analysis/normed_space/hahn_banach.lean @@ -93,11 +93,11 @@ variables {F : Type*} [normed_group F] [normed_space ℂ F] -- Inlining the following two definitions causes a type mismatch between -- subspace ℝ (semimodule.restrict_scalars ℝ ℂ F) and subspace ℂ F. /-- Restrict a `ℂ`-subspace to an `ℝ`-subspace. -/ -noncomputable def restrict_scalars (p : subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ ℂ F +noncomputable def restrict_scalars (p : subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ private lemma apply_real (p : subspace ℂ F) (f' : p →L[ℝ] ℝ) : ∃ g : F →L[ℝ] ℝ, (∀ x : restrict_scalars p, g x = f' x) ∧ ∥g∥ = ∥f'∥ := - exists_extension_norm_eq (p.restrict_scalars ℝ ℂ F) f' + exists_extension_norm_eq (p.restrict_scalars ℝ) f' open complex diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean new file mode 100644 index 0000000000000..d3c6141b1b859 --- /dev/null +++ b/src/analysis/normed_space/inner_product.lean @@ -0,0 +1,1628 @@ +/- +Copyright (c) 2019 Zhouhang Zhou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zhouhang Zhou, Sébastien Gouëzel, Frédéric Dupuis +-/ + +import linear_algebra.bilinear_form +import linear_algebra.sesquilinear_form +import analysis.special_functions.pow +import topology.metric_space.pi_Lp +import data.complex.is_R_or_C + +/-! +# Inner Product Space + +This file defines inner product spaces and proves its basic properties. + +An inner product space is a vector space endowed with an inner product. It generalizes the notion of +dot product in `ℝ^n` and provides the means of defining the length of a vector and the angle between +two vectors. In particular vectors `x` and `y` are orthogonal if their inner product equals zero. +We define both the real and complex cases at the same time using the `is_R_or_C` typeclass. + + +## Main results + +- We define the class `inner_product_space 𝕜 E` extending `normed_space 𝕜 E` with a number of basic + properties, most notably the Cauchy-Schwarz inequality. Here `𝕜` is understood to be either `ℝ` + or `ℂ`, through the `is_R_or_C` typeclass. +- We show that if `f i` is an inner product space for each `i`, then so is `Π i, f i` +- We define `euclidean_space 𝕜 n` to be `n → 𝕜` for any `fintype n`, and show that + this an inner product space. +- Existence of orthogonal projection onto nonempty complete subspace: + Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace. + Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`. + The point `v` is usually called the orthogonal projection of `u` onto `K`. + +## Notation + +We globally denote the real and complex inner products by `⟪·, ·⟫_ℝ` and `⟪·, ·⟫_ℂ` respectively. +We also provide two notation namespaces: `real_inner_product_space`, `complex_inner_product_space`, +which respectively introduce the plain notation `⟪·, ·⟫` for the the real and complex inner product. + +## Implementation notes + +We choose the convention that inner products are conjugate linear in the first argument and linear +in the second. + +## TODO + +- Fix the section on the existence of minimizers and orthogonal projections to make sure that it + also applies in the complex case. + +## Tags + +inner product space, norm + +## References +* [Clément & Martin, *The Lax-Milgram Theorem. A detailed proof to be formalized in Coq*] +* [Clément & Martin, *A Coq formal proof of the Lax–Milgram theorem*] + +The Coq code is available at the following address: +-/ + +noncomputable theory + +open is_R_or_C real +open_locale big_operators classical + +variables {𝕜 E F : Type*} [is_R_or_C 𝕜] +local notation `𝓚` := @is_R_or_C.of_real 𝕜 _ + +/-- Syntactic typeclass for types endowed with an inner product -/ +class has_inner (𝕜 E : Type*) := (inner : E → E → 𝕜) + +export has_inner (inner) + +notation `⟪`x`, `y`⟫_ℝ` := @inner ℝ _ _ x y +notation `⟪`x`, `y`⟫_ℂ` := @inner ℂ _ _ x y + +section notations + +localized "notation `⟪`x`, `y`⟫` := @inner ℝ _ _ x y" in real_inner_product_space +localized "notation `⟪`x`, `y`⟫` := @inner ℂ _ _ x y" in complex_inner_product_space + +end notations + +/-- +An inner product space is a vector space with an additional operation called inner product. +The norm could be derived from the inner product, instead we require the existence of a norm and +the fact that `∥x∥^2 = re ⟪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*) (E : Type*) [is_R_or_C 𝕜] + extends normed_group E, normed_space 𝕜 E, has_inner 𝕜 E := +(norm_sq_eq_inner : ∀ (x : E), ∥x∥^2 = re (inner x x)) +(conj_sym : ∀ x y, conj (inner y x) = inner x y) +(nonneg_im : ∀ x, im (inner x 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 = (conj r) * inner x y) + +/- This instance generates the type-class problem `inner_product_space ?m E` when looking for + `normed_group E`. However, since `?m` can only ever be `ℝ` or `ℂ`, this should not cause + problems. -/ +attribute [nolint dangerous_instance] inner_product_space.to_normed_group + +/-! +### Constructing a normed space structure from an inner 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 + (𝕜 : Type*) (F : Type*) + [is_R_or_C 𝕜] [add_comm_group F] [semimodule 𝕜 F] := +(inner : F → F → 𝕜) +(conj_sym : ∀ x y, conj (inner y x) = inner x y) +(nonneg_im : ∀ x, im (inner x x) = 0) +(nonneg_re : ∀ x, re (inner x x) ≥ 0) +(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 = (conj r) * inner x y) + +/- 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 + +local notation `⟪`x`, `y`⟫` := @inner 𝕜 F _ x y +local notation `𝓚` := @is_R_or_C.of_real 𝕜 _ +local notation `norm_sqK` := @is_R_or_C.norm_sq 𝕜 _ +local notation `reK` := @is_R_or_C.re 𝕜 _ +local notation `ext_iff` := @is_R_or_C.ext_iff 𝕜 _ +local postfix `†`:90 := @is_R_or_C.conj 𝕜 _ + +/-- Inner product defined by the `inner_product_space.core` structure. -/ +def to_has_inner : has_inner 𝕜 F := { inner := c.inner } +local attribute [instance] to_has_inner + +/-- The norm squared function for `inner_product_space.core` structure. -/ +def norm_sq (x : F) := reK ⟪x, x⟫ + +local notation `norm_sqF` := @norm_sq 𝕜 F _ _ _ _ + +lemma inner_conj_sym (x y : F) : ⟪y, x⟫† = ⟪x, y⟫ := c.conj_sym x y + +lemma inner_self_nonneg {x : F} : 0 ≤ re ⟪x, x⟫ := c.nonneg_re _ + +lemma inner_self_nonneg_im {x : F} : im ⟪x, x⟫ = 0 := c.nonneg_im _ + +lemma inner_self_im_zero {x : F} : im ⟪x, x⟫ = 0 := c.nonneg_im _ + +lemma inner_add_left {x y z : F} : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ := +c.add_left _ _ _ + +lemma inner_add_right {x y z : F} : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ := +by rw [←inner_conj_sym, inner_add_left, ring_hom.map_add]; simp only [inner_conj_sym] + +lemma inner_norm_sq_eq_inner_self (x : F) : 𝓚 (norm_sqF x) = ⟪x, x⟫ := +begin + rw ext_iff, + exact ⟨by simp only [of_real_re]; refl, by simp only [inner_self_nonneg_im, of_real_im]⟩ +end + +lemma inner_re_symm {x y : F} : re ⟪x, y⟫ = re ⟪y, x⟫ := +by rw [←inner_conj_sym, conj_re] + +lemma inner_im_symm {x y : F} : im ⟪x, y⟫ = -im ⟪y, x⟫ := +by rw [←inner_conj_sym, conj_im] + +lemma inner_smul_left {x y : F} {r : 𝕜} : ⟪r • x, y⟫ = r† * ⟪x, y⟫ := +c.smul_left _ _ _ + +lemma inner_smul_right {x y : F} {r : 𝕜} : ⟪x, r • y⟫ = r * ⟪x, y⟫ := +by rw [←inner_conj_sym, inner_smul_left]; simp only [conj_conj, inner_conj_sym, ring_hom.map_mul] + +lemma inner_zero_left {x : F} : ⟪0, x⟫ = 0 := +by rw [←zero_smul 𝕜 (0 : F), inner_smul_left]; simp only [zero_mul, ring_hom.map_zero] + +lemma inner_zero_right {x : F} : ⟪x, 0⟫ = 0 := +by rw [←inner_conj_sym, inner_zero_left]; simp only [ring_hom.map_zero] + +lemma inner_self_eq_zero {x : F} : ⟪x, x⟫ = 0 ↔ x = 0 := +iff.intro (c.definite _) (by { rintro rfl, exact inner_zero_left }) + +lemma inner_self_re_to_K {x : F} : 𝓚 (re ⟪x, x⟫) = ⟪x, x⟫ := +by norm_num [ext_iff, inner_self_nonneg_im] + +lemma inner_abs_conj_sym {x y : F} : abs ⟪x, y⟫ = abs ⟪y, x⟫ := + by rw [←inner_conj_sym, abs_conj] + +lemma inner_neg_left {x y : F} : ⟪-x, y⟫ = -⟪x, y⟫ := +by { rw [← neg_one_smul 𝕜 x, inner_smul_left], simp } + +lemma inner_neg_right {x y : F} : ⟪x, -y⟫ = -⟪x, y⟫ := +by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_hom.map_neg, inner_conj_sym] + +lemma inner_sub_left {x y z : F} : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫ := +by { simp [sub_eq_add_neg, inner_add_left, inner_neg_left] } + +lemma inner_sub_right {x y z : F} : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫ := +by { simp [sub_eq_add_neg, inner_add_right, inner_neg_right] } + +lemma inner_mul_conj_re_abs {x y : F} : re (⟪x, y⟫ * ⟪y, x⟫) = abs (⟪x, y⟫ * ⟪y, x⟫) := +by { rw[←inner_conj_sym, mul_comm], exact re_eq_abs_of_mul_conj (inner y x), } + +/-- Expand `inner (x + y) (x + y)` -/ +lemma inner_add_add_self {x y : F} : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ := +by simp only [inner_add_left, inner_add_right]; ring + +/- Expand `inner (x - y) (x - y)` -/ +lemma inner_sub_sub_self {x y : F} : ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫ := +by simp only [inner_sub_left, inner_sub_right]; ring + +/-- +Cauchy–Schwarz inequality. This proof follows "Proof 2" on Wikipedia. +We need this for the `core` structure to prove the triangle inequality below when +showing the core is a normed group. +-/ +lemma inner_mul_inner_self_le (x y : F) : abs ⟪x, y⟫ * abs ⟪y, x⟫ ≤ re ⟪x, x⟫ * re ⟪y, y⟫ := +begin + by_cases hy : y = 0, + { rw [hy], simp only [is_R_or_C.abs_zero, inner_zero_left, mul_zero, add_monoid_hom.map_zero] }, + { change y ≠ 0 at hy, + have hy' : ⟪y, y⟫ ≠ 0 := λ h, by rw [inner_self_eq_zero] at h; exact hy h, + set T := ⟪y, x⟫ / ⟪y, y⟫ with hT, + have h₁ : re ⟪y, x⟫ = re ⟪x, y⟫ := inner_re_symm, + have h₂ : im ⟪y, x⟫ = -im ⟪x, y⟫ := inner_im_symm, + have h₃ : ⟪y, x⟫ * ⟪x, y⟫ * ⟪y, y⟫ / (⟪y, y⟫ * ⟪y, y⟫) = ⟪y, x⟫ * ⟪x, y⟫ / ⟪y, y⟫, + { rw [mul_div_assoc], + have : ⟪y, y⟫ / (⟪y, y⟫ * ⟪y, y⟫) = 1 / ⟪y, y⟫ := + by rw [div_mul_eq_div_mul_one_div, div_self hy', one_mul], + rw [this, div_eq_mul_inv, one_mul, ←div_eq_mul_inv] }, + have h₄ : ⟪y, y⟫ = 𝓚 (re ⟪y, y⟫) := by simp only [inner_self_re_to_K], + have h₅ : re ⟪y, y⟫ > 0, + { refine lt_of_le_of_ne inner_self_nonneg _, + intro H, + apply hy', + rw ext_iff, + exact ⟨by simp [H],by simp [inner_self_nonneg_im]⟩ }, + have h₆ : re ⟪y, y⟫ ≠ 0 := ne_of_gt h₅, + have hmain := calc + 0 ≤ re ⟪x - T • y, x - T • y⟫ + : inner_self_nonneg + ... = re ⟪x, x⟫ - re ⟪T • y, x⟫ - re ⟪x, T • y⟫ + re ⟪T • y, T • y⟫ + : by simp [inner_sub_sub_self, inner_smul_left, inner_smul_right, h₁, h₂] + ... = re ⟪x, x⟫ - re (T† * ⟪y, x⟫) - re (T * ⟪x, y⟫) + re (T * T† * ⟪y, y⟫) + : by simp [inner_smul_left, inner_smul_right, mul_assoc] + ... = re ⟪x, x⟫ - re (⟪x, y⟫ / ⟪y, y⟫ * ⟪y, x⟫) + : by field_simp [-mul_re, inner_conj_sym, hT, conj_div, h₁, h₃] + ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫) + : by rw [div_mul_eq_mul_div_comm, ←mul_div_assoc] + ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / 𝓚 (re ⟪y, y⟫)) + : by conv_lhs { rw [h₄] } + ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫) / re ⟪y, y⟫ + : by rw [div_re_of_real] + ... = re ⟪x, x⟫ - abs (⟪x, y⟫ * ⟪y, x⟫) / re ⟪y, y⟫ + : by rw [inner_mul_conj_re_abs] + ... = re ⟪x, x⟫ - abs ⟪x, y⟫ * abs ⟪y, x⟫ / re ⟪y, y⟫ + : by rw is_R_or_C.abs_mul, + have hmain' : abs ⟪x, y⟫ * abs ⟪y, x⟫ / re ⟪y, y⟫ ≤ re ⟪x, x⟫ := by linarith, + have := (mul_le_mul_right h₅).mpr hmain', + rwa [div_mul_cancel (abs ⟪x, y⟫ * abs ⟪y, x⟫) h₆] at this } +end + +/-- Norm constructed from a `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 (re ⟪x, x⟫) } + +local attribute [instance] to_has_norm + +lemma norm_eq_sqrt_inner (x : F) : ∥x∥ = sqrt (re ⟪x, x⟫) := rfl + +lemma inner_self_eq_norm_square (x : F) : re ⟪x, x⟫ = ∥x∥ * ∥x∥ := +by rw[norm_eq_sqrt_inner, ←sqrt_mul inner_self_nonneg (re ⟪x, x⟫), + sqrt_mul_self inner_self_nonneg] + +lemma sqrt_norm_sq_eq_norm {x : F} : sqrt (norm_sqF x) = ∥x∥ := rfl + +/-- Cauchy–Schwarz inequality with norm -/ +lemma abs_inner_le_norm (x y : F) : abs ⟪x, y⟫ ≤ ∥x∥ * ∥y∥ := +nonneg_le_nonneg_of_squares_le (mul_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) +begin + have H : ∥x∥ * ∥y∥ * (∥x∥ * ∥y∥) = re ⟪y, y⟫ * re ⟪x, x⟫, + { simp only [inner_self_eq_norm_square], ring, }, + rw H, + conv + begin + to_lhs, congr, rw[inner_abs_conj_sym], + end, + exact inner_mul_inner_self_le y x, +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, + { intro H, + change sqrt (re ⟪x, x⟫) = 0 at H, + rw [sqrt_eq_zero inner_self_nonneg] at H, + apply (inner_self_eq_zero : ⟪x, x⟫ = 0 ↔ x = 0).mp, + rw ext_iff, + exact ⟨by simp [H], by simp [inner_self_im_zero]⟩ }, + { rintro rfl, + change sqrt (re ⟪0, 0⟫) = 0, + simp only [sqrt_zero, inner_zero_right, add_monoid_hom.map_zero] } + end, + triangle := assume x y, + begin + have h₁ : abs ⟪x, y⟫ ≤ ∥x∥ * ∥y∥ := abs_inner_le_norm _ _, + have h₂ : re ⟪x, y⟫ ≤ abs ⟪x, y⟫ := re_le_abs _, + have h₃ : re ⟪x, y⟫ ≤ ∥x∥ * ∥y∥ := by linarith, + have h₄ : re ⟪y, x⟫ ≤ ∥x∥ * ∥y∥ := by rwa [←inner_conj_sym, conj_re], + have : ∥x + y∥ * ∥x + y∥ ≤ (∥x∥ + ∥y∥) * (∥x∥ + ∥y∥), + { simp [←inner_self_eq_norm_square, inner_add_add_self, add_mul, mul_add, mul_comm], + linarith }, + exact nonneg_le_nonneg_of_squares_le (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this + end, + norm_neg := λ x, by simp only [norm, inner_neg_left, neg_neg, inner_neg_right] } + +local attribute [instance] to_normed_group + +/-- Normed space structure constructed from a `inner_product_space.core` structure -/ +def to_normed_space : normed_space 𝕜 F := +{ norm_smul_le := assume r x, + begin + rw [norm_eq_sqrt_inner, inner_smul_left, inner_smul_right, ←mul_assoc], + rw [conj_mul_eq_norm_sq_left, of_real_mul_re, sqrt_mul, ←inner_norm_sq_eq_inner_self, of_real_re], + { simp [sqrt_norm_sq_eq_norm, is_R_or_C.sqrt_norm_sq_eq_norm] }, + { exact norm_sq_nonneg r } + end } + +end inner_product_space.of_core + +/-- Given a `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_sq_eq_inner := λ x, + begin + have h₁ : ∥x∥^2 = (sqrt (re (c.inner x x))) ^ 2 := rfl, + have h₂ : 0 ≤ re (c.inner x x) := inner_product_space.of_core.inner_self_nonneg, + simp [h₁, sqr_sqrt, h₂], + end, + ..c } +end + +/-! ### Properties of inner product spaces -/ + +variables [inner_product_space 𝕜 E] [inner_product_space ℝ F] +local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y +local notation `⟪`x`, `y`⟫_ℝ` := @inner ℝ _ _ x y +local notation `⟪`x`, `y`⟫_ℂ` := @inner ℂ _ _ x y +local notation `IK` := @is_R_or_C.I 𝕜 _ +local notation `absR` := _root_.abs +local postfix `†`:90 := @is_R_or_C.conj 𝕜 _ +local postfix `⋆`:90 := complex.conj + +export inner_product_space (norm_sq_eq_inner) + +section basic_properties + +lemma inner_conj_sym (x y : E) : ⟪y, x⟫† = ⟪x, y⟫ := inner_product_space.conj_sym _ _ +lemma real_inner_comm (x y : F) : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := inner_conj_sym x y + +lemma inner_eq_zero_sym {x y : E} : ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0 := +⟨λ h, by simp [←inner_conj_sym, h], λ h, by simp [←inner_conj_sym, h]⟩ + +lemma inner_self_nonneg_im {x : E} : im ⟪x, x⟫ = 0 := inner_product_space.nonneg_im _ + +lemma inner_self_im_zero {x : E} : im ⟪x, x⟫ = 0 := inner_product_space.nonneg_im _ + +lemma inner_add_left {x y z : E} : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ := +inner_product_space.add_left _ _ _ + +lemma inner_add_right {x y z : E} : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ := +begin + rw [←inner_conj_sym, inner_add_left, ring_hom.map_add], + conv_rhs { rw ←inner_conj_sym, conv { congr, skip, rw ←inner_conj_sym } } +end + +lemma inner_re_symm {x y : E} : re ⟪x, y⟫ = re ⟪y, x⟫ := +by rw [←inner_conj_sym, conj_re] + +lemma inner_im_symm {x y : E} : im ⟪x, y⟫ = -im ⟪y, x⟫ := +by rw [←inner_conj_sym, conj_im] + +lemma inner_smul_left {x y : E} {r : 𝕜} : ⟪r • x, y⟫ = r† * ⟪x, y⟫ := +inner_product_space.smul_left _ _ _ +lemma real_inner_smul_left {x y : F} {r : ℝ} : ⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ := inner_smul_left + +lemma inner_smul_right {x y : E} {r : 𝕜} : ⟪x, r • y⟫ = r * ⟪x, y⟫ := +by rw [←inner_conj_sym, inner_smul_left, ring_hom.map_mul, conj_conj, inner_conj_sym] +lemma real_inner_smul_right {x y : F} {r : ℝ} : ⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ := inner_smul_right + +/-- The inner product as a sesquilinear form. -/ +def sesq_form_of_inner : sesq_form 𝕜 E conj_to_ring_equiv := +{ sesq := λ x y, ⟪y, x⟫, -- Note that sesquilinear forms are linear in the first argument + sesq_add_left := λ x y z, inner_add_right, + sesq_add_right := λ x y z, inner_add_left, + sesq_smul_left := λ r x y, inner_smul_right, + sesq_smul_right := λ r x y, inner_smul_left } + +/-- The real inner product as a bilinear form. -/ +def bilin_form_of_real_inner : bilin_form ℝ F := +{ bilin := inner, + bilin_add_left := λ x y z, inner_add_left, + bilin_smul_left := λ a x y, inner_smul_left, + bilin_add_right := λ x y z, inner_add_right, + bilin_smul_right := λ a x y, inner_smul_right } + +/-- An inner product with a sum on the left. -/ +lemma sum_inner {ι : Type*} (s : finset ι) (f : ι → E) (x : E) : + ⟪∑ i in s, f i, x⟫ = ∑ i in s, ⟪f i, x⟫ := +sesq_form.map_sum_right (sesq_form_of_inner) _ _ _ + +/-- An inner product with a sum on the right. -/ +lemma inner_sum {ι : Type*} (s : finset ι) (f : ι → E) (x : E) : + ⟪x, ∑ i in s, f i⟫ = ∑ i in s, ⟪x, f i⟫ := +sesq_form.map_sum_left (sesq_form_of_inner) _ _ _ + +@[simp] lemma inner_zero_left {x : E} : ⟪0, x⟫ = 0 := +by rw [← zero_smul 𝕜 (0:E), inner_smul_left, ring_hom.map_zero, zero_mul] + +lemma inner_re_zero_left {x : E} : re ⟪0, x⟫ = 0 := +by simp only [inner_zero_left, add_monoid_hom.map_zero] + +@[simp] lemma inner_zero_right {x : E} : ⟪x, 0⟫ = 0 := +by rw [←inner_conj_sym, inner_zero_left, ring_hom.map_zero] + +lemma inner_re_zero_right {x : E} : re ⟪x, 0⟫ = 0 := +by simp only [inner_zero_right, add_monoid_hom.map_zero] + +lemma inner_self_nonneg {x : E} : 0 ≤ re ⟪x, x⟫ := +by rw [←norm_sq_eq_inner]; exact pow_nonneg (norm_nonneg x) 2 +lemma real_inner_self_nonneg {x : F} : 0 ≤ ⟪x, x⟫_ℝ := @inner_self_nonneg ℝ F _ _ x + +@[simp] lemma inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0 := +begin + split, + { intro h, + have h₁ : re ⟪x, x⟫ = 0 := by rw is_R_or_C.ext_iff at h; simp [h.1], + rw [←norm_sq_eq_inner x] at h₁, + rw [←norm_eq_zero], + exact pow_eq_zero h₁ }, + { rintro rfl, + exact inner_zero_left } +end + +@[simp] lemma inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 := +begin + split, + { intro h, + rw ←inner_self_eq_zero, + have H₁ : re ⟪x, x⟫ ≥ 0, exact inner_self_nonneg, + have H₂ : re ⟪x, x⟫ = 0, exact le_antisymm h H₁, + rw is_R_or_C.ext_iff, + exact ⟨by simp [H₂], by simp [inner_self_nonneg_im]⟩ }, + { rintro rfl, + simp only [inner_zero_left, add_monoid_hom.map_zero] } +end + +lemma real_inner_self_nonpos {x : F} : ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0 := +by { have h := @inner_self_nonpos ℝ F _ _ x, simpa using h } + +@[simp] lemma inner_self_re_to_K {x : E} : 𝓚 (re ⟪x, x⟫) = ⟪x, x⟫ := +by rw is_R_or_C.ext_iff; exact ⟨by simp, by simp [inner_self_nonneg_im]⟩ + +lemma inner_self_re_abs {x : E} : re ⟪x, x⟫ = abs ⟪x, x⟫ := +begin + have H : ⟪x, x⟫ = 𝓚 (re ⟪x, x⟫) + 𝓚 (im ⟪x, x⟫) * I, + { rw re_add_im, }, + rw [H, is_add_hom.map_add re (𝓚 (re ⟪x, x⟫)) ((𝓚 (im ⟪x, x⟫)) * I)], + rw [mul_re, I_re, mul_zero, I_im, zero_sub, tactic.ring.add_neg_eq_sub], + rw [of_real_re, of_real_im, sub_zero, inner_self_nonneg_im], + simp only [abs_of_real, add_zero, of_real_zero, zero_mul], + exact (_root_.abs_of_nonneg inner_self_nonneg).symm, +end + +lemma inner_self_abs_to_K {x : E} : 𝓚 (abs ⟪x, x⟫) = ⟪x, x⟫ := +by { rw[←inner_self_re_abs], exact inner_self_re_to_K } + +lemma real_inner_self_abs {x : F} : absR ⟪x, x⟫_ℝ = ⟪x, x⟫_ℝ := +by { have h := @inner_self_abs_to_K ℝ F _ _ x, simpa using h } + +lemma inner_abs_conj_sym {x y : E} : abs ⟪x, y⟫ = abs ⟪y, x⟫ := +by rw [←inner_conj_sym, abs_conj] + +@[simp] lemma inner_neg_left {x y : E} : ⟪-x, y⟫ = -⟪x, y⟫ := +by { rw [← neg_one_smul 𝕜 x, inner_smul_left], simp } + +@[simp] lemma inner_neg_right {x y : E} : ⟪x, -y⟫ = -⟪x, y⟫ := +by rw [←inner_conj_sym, inner_neg_left]; simp only [ring_hom.map_neg, inner_conj_sym] + +lemma inner_neg_neg {x y : E} : ⟪-x, -y⟫ = ⟪x, y⟫ := by simp + +@[simp] lemma inner_self_conj {x : E} : ⟪x, x⟫† = ⟪x, x⟫ := +by rw [is_R_or_C.ext_iff]; exact ⟨by rw [conj_re], by rw [conj_im, inner_self_im_zero, neg_zero]⟩ + +lemma inner_sub_left {x y z : E} : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫ := +by { simp [sub_eq_add_neg, inner_add_left] } + +lemma inner_sub_right {x y z : E} : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫ := +by { simp [sub_eq_add_neg, inner_add_right] } + +lemma inner_mul_conj_re_abs {x y : E} : re (⟪x, y⟫ * ⟪y, x⟫) = abs (⟪x, y⟫ * ⟪y, x⟫) := +by { rw[←inner_conj_sym, mul_comm], exact re_eq_abs_of_mul_conj (inner y x), } + +/-- Expand `⟪x + y, x + y⟫` -/ +lemma inner_add_add_self {x y : E} : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ := +by simp only [inner_add_left, inner_add_right]; ring + +/-- Expand `⟪x + y, x + y⟫_ℝ` -/ +lemma real_inner_add_add_self {x y : F} : ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ := +begin + have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [←inner_conj_sym]; refl, + simp [inner_add_add_self, this], + ring, +end + +/- Expand `⟪x - y, x - y⟫` -/ +lemma inner_sub_sub_self {x y : E} : ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫ := +by simp only [inner_sub_left, inner_sub_right]; ring + +/-- Expand `⟪x - y, x - y⟫_ℝ` -/ +lemma real_inner_sub_sub_self {x y : F} : ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ := +begin + have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [←inner_conj_sym]; refl, + simp [inner_sub_sub_self, this], + ring, +end + +/-- Parallelogram law -/ +lemma parallelogram_law {x y : E} : + ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ = 2 * (⟪x, x⟫ + ⟪y, y⟫) := +by simp [inner_add_add_self, inner_sub_sub_self, two_mul, sub_eq_add_neg, add_comm, add_left_comm] + +/-- Cauchy–Schwarz inequality. This proof follows "Proof 2" on Wikipedia. -/ +lemma inner_mul_inner_self_le (x y : E) : abs ⟪x, y⟫ * abs ⟪y, x⟫ ≤ re ⟪x, x⟫ * re ⟪y, y⟫ := +begin + by_cases hy : y = 0, + { rw [hy], simp only [is_R_or_C.abs_zero, inner_zero_left, mul_zero, add_monoid_hom.map_zero] }, + { change y ≠ 0 at hy, + have hy' : ⟪y, y⟫ ≠ 0 := λ h, by rw [inner_self_eq_zero] at h; exact hy h, + set T := ⟪y, x⟫ / ⟪y, y⟫ with hT, + have h₁ : re ⟪y, x⟫ = re ⟪x, y⟫ := inner_re_symm, + have h₂ : im ⟪y, x⟫ = -im ⟪x, y⟫ := inner_im_symm, + have h₃ : ⟪y, x⟫ * ⟪x, y⟫ * ⟪y, y⟫ / (⟪y, y⟫ * ⟪y, y⟫) = ⟪y, x⟫ * ⟪x, y⟫ / ⟪y, y⟫, + { rw [mul_div_assoc], + have : ⟪y, y⟫ / (⟪y, y⟫ * ⟪y, y⟫) = 1 / ⟪y, y⟫ := + by rw [div_mul_eq_div_mul_one_div, div_self hy', one_mul], + rw [this, div_eq_mul_inv, one_mul, ←div_eq_mul_inv] }, + have h₄ : ⟪y, y⟫ = 𝓚 (re ⟪y, y⟫) := by simp, + have h₅ : re ⟪y, y⟫ > 0, + { refine lt_of_le_of_ne inner_self_nonneg _, + intro H, + apply hy', + rw is_R_or_C.ext_iff, + exact ⟨by simp [H],by simp [inner_self_nonneg_im]⟩ }, + have h₆ : re ⟪y, y⟫ ≠ 0 := ne_of_gt h₅, + have hmain := calc + 0 ≤ re ⟪x - T • y, x - T • y⟫ + : inner_self_nonneg + ... = re ⟪x, x⟫ - re ⟪T • y, x⟫ - re ⟪x, T • y⟫ + re ⟪T • y, T • y⟫ + : by simp [inner_sub_sub_self, inner_smul_left, inner_smul_right, h₁, h₂] + ... = re ⟪x, x⟫ - re (T† * ⟪y, x⟫) - re (T * ⟪x, y⟫) + re (T * T† * ⟪y, y⟫) + : by simp [inner_smul_left, inner_smul_right, mul_assoc] + ... = re ⟪x, x⟫ - re (⟪x, y⟫ / ⟪y, y⟫ * ⟪y, x⟫) + : by field_simp [-mul_re, hT, conj_div, h₁, h₃, inner_conj_sym] + ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / ⟪y, y⟫) + : by rw [div_mul_eq_mul_div_comm, ←mul_div_assoc] + ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫ / 𝓚 (re ⟪y, y⟫)) + : by conv_lhs { rw [h₄] } + ... = re ⟪x, x⟫ - re (⟪x, y⟫ * ⟪y, x⟫) / re ⟪y, y⟫ + : by rw [div_re_of_real] + ... = re ⟪x, x⟫ - abs (⟪x, y⟫ * ⟪y, x⟫) / re ⟪y, y⟫ + : by rw [inner_mul_conj_re_abs] + ... = re ⟪x, x⟫ - abs ⟪x, y⟫ * abs ⟪y, x⟫ / re ⟪y, y⟫ + : by rw is_R_or_C.abs_mul, + have hmain' : abs ⟪x, y⟫ * abs ⟪y, x⟫ / re ⟪y, y⟫ ≤ re ⟪x, x⟫ := by linarith, + have := (mul_le_mul_right h₅).mpr hmain', + rwa [div_mul_cancel (abs ⟪x, y⟫ * abs ⟪y, x⟫) h₆] at this } +end + +/-- Cauchy–Schwarz inequality for real inner products. -/ +lemma real_inner_mul_inner_self_le (x y : F) : ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ := +begin + have h₁ : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [←inner_conj_sym]; refl, + have h₂ := @inner_mul_inner_self_le ℝ F _ _ x y, + dsimp at h₂, + have h₃ := abs_mul_abs_self ⟪x, y⟫_ℝ, + rw [h₁] at h₂, + simpa [h₃] using h₂, +end + +/-- A family of vectors is linearly independent if they are nonzero +and orthogonal. -/ +lemma linear_independent_of_ne_zero_of_inner_eq_zero {ι : Type*} {v : ι → E} + (hz : ∀ i, v i ≠ 0) (ho : ∀ i j, i ≠ j → ⟪v i, v j⟫ = 0) : linear_independent 𝕜 v := +begin + rw linear_independent_iff', + intros s g hg i hi, + have h' : g i * inner (v i) (v i) = inner (v i) (∑ j in s, g j • v j), + { rw inner_sum, + symmetry, + convert finset.sum_eq_single i _ _, + { rw inner_smul_right }, + { intros j hj hji, + rw [inner_smul_right, ho i j hji.symm, mul_zero] }, + { exact λ h, false.elim (h hi) } }, + simpa [hg, hz] using h' +end + +end basic_properties + +section norm + +lemma norm_eq_sqrt_inner (x : E) : ∥x∥ = sqrt (re ⟪x, x⟫) := +begin + have h₁ : ∥x∥^2 = re ⟪x, x⟫ := norm_sq_eq_inner x, + have h₂ := congr_arg sqrt h₁, + simpa using h₂, +end + +lemma norm_eq_sqrt_real_inner (x : F) : ∥x∥ = sqrt ⟪x, x⟫_ℝ := +by { have h := @norm_eq_sqrt_inner ℝ F _ _ x, simpa using h } + +lemma inner_self_eq_norm_square (x : E) : re ⟪x, x⟫ = ∥x∥ * ∥x∥ := +by rw[norm_eq_sqrt_inner, ←sqrt_mul inner_self_nonneg (re ⟪x, x⟫), + sqrt_mul_self inner_self_nonneg] + +lemma real_inner_self_eq_norm_square (x : F) : ⟪x, x⟫_ℝ = ∥x∥ * ∥x∥ := +by { have h := @inner_self_eq_norm_square ℝ F _ _ x, simpa using h } + + +/-- Expand the square -/ +lemma norm_add_pow_two {x y : E} : ∥x + y∥^2 = ∥x∥^2 + 2 * (re ⟪x, y⟫) + ∥y∥^2 := +begin + repeat {rw [pow_two, ←inner_self_eq_norm_square]}, + rw[inner_add_add_self, two_mul], + simp only [add_assoc, add_left_inj, add_right_inj, add_monoid_hom.map_add], + rw [←inner_conj_sym, conj_re], +end + +/-- Expand the square -/ +lemma norm_add_pow_two_real {x y : F} : ∥x + y∥^2 = ∥x∥^2 + 2 * ⟪x, y⟫_ℝ + ∥y∥^2 := +by { have h := @norm_add_pow_two ℝ F _ _, simpa using h } + +/-- Expand the square -/ +lemma norm_add_mul_self {x y : E} : ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + 2 * (re ⟪x, y⟫) + ∥y∥ * ∥y∥ := +by { repeat {rw [← pow_two]}, exact norm_add_pow_two } + +/-- Expand the square -/ +lemma norm_add_mul_self_real {x y : F} : ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + 2 * ⟪x, y⟫_ℝ + ∥y∥ * ∥y∥ := +by { have h := @norm_add_mul_self ℝ F _ _, simpa using h } + +/-- Expand the square -/ +lemma norm_sub_pow_two {x y : E} : ∥x - y∥^2 = ∥x∥^2 - 2 * (re ⟪x, y⟫) + ∥y∥^2 := +begin + repeat {rw [pow_two, ←inner_self_eq_norm_square]}, + rw[inner_sub_sub_self], + calc + re (⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫) + = re ⟪x, x⟫ - re ⟪x, y⟫ - re ⟪y, x⟫ + re ⟪y, y⟫ : by simp + ... = -re ⟪y, x⟫ - re ⟪x, y⟫ + re ⟪x, x⟫ + re ⟪y, y⟫ : by ring + ... = -re (⟪x, y⟫†) - re ⟪x, y⟫ + re ⟪x, x⟫ + re ⟪y, y⟫ : by rw[inner_conj_sym] + ... = -re ⟪x, y⟫ - re ⟪x, y⟫ + re ⟪x, x⟫ + re ⟪y, y⟫ : by rw[conj_re] + ... = re ⟪x, x⟫ - 2*re ⟪x, y⟫ + re ⟪y, y⟫ : by ring +end + +/-- Expand the square -/ +lemma norm_sub_pow_two_real {x y : F} : ∥x - y∥^2 = ∥x∥^2 - 2 * ⟪x, y⟫_ℝ + ∥y∥^2 := +by { have h := @norm_sub_pow_two ℝ F _ _, simpa using h } + +/-- Expand the square -/ +lemma norm_sub_mul_self {x y : E} : ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ - 2 * re ⟪x, y⟫ + ∥y∥ * ∥y∥ := +by { repeat {rw [← pow_two]}, exact norm_sub_pow_two } + +/-- Expand the square -/ +lemma norm_sub_mul_self_real {x y : F} : ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ - 2 * ⟪x, y⟫_ℝ + ∥y∥ * ∥y∥ := +by { have h := @norm_sub_mul_self ℝ F _ _, simpa using h } + +/-- Cauchy–Schwarz inequality with norm -/ +lemma abs_inner_le_norm (x y : E) : abs ⟪x, y⟫ ≤ ∥x∥ * ∥y∥ := +nonneg_le_nonneg_of_squares_le (mul_nonneg (norm_nonneg _) (norm_nonneg _)) +begin + have : ∥x∥ * ∥y∥ * (∥x∥ * ∥y∥) = (re ⟪x, x⟫) * (re ⟪y, y⟫), + simp only [inner_self_eq_norm_square], ring, + rw this, + conv_lhs { congr, skip, rw [inner_abs_conj_sym] }, + exact inner_mul_inner_self_le _ _ +end + +/-- Cauchy–Schwarz inequality with norm -/ +lemma abs_real_inner_le_norm (x y : F) : absR ⟪x, y⟫_ℝ ≤ ∥x∥ * ∥y∥ := +by { have h := @abs_inner_le_norm ℝ F _ _ x y, simpa using h } + +include 𝕜 +lemma parallelogram_law_with_norm {x y : E} : + ∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥) := +begin + simp only [(inner_self_eq_norm_square _).symm], + rw[←add_monoid_hom.map_add, parallelogram_law, two_mul, two_mul], + simp only [add_monoid_hom.map_add], +end +omit 𝕜 + +lemma parallelogram_law_with_norm_real {x y : F} : + ∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥) := +by { have h := @parallelogram_law_with_norm ℝ F _ _ x y, simpa using h } + +/-- Polarization identity: The real inner product, in terms of the norm. -/ +lemma real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two (x y : F) : + ⟪x, y⟫_ℝ = (∥x + y∥ * ∥x + y∥ - ∥x∥ * ∥x∥ - ∥y∥ * ∥y∥) / 2 := +by rw norm_add_mul_self; ring + +/-- Polarization identity: The real inner product, in terms of the norm. -/ +lemma real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two (x y : F) : + ⟪x, y⟫_ℝ = (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ - ∥x - y∥ * ∥x - y∥) / 2 := +by rw norm_sub_mul_self; ring + +/-- Pythagorean theorem, if-and-only-if vector inner product form. -/ +lemma norm_add_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero (x y : F) : + ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ ⟪x, y⟫_ℝ = 0 := +begin + rw [norm_add_mul_self, add_right_cancel_iff, add_right_eq_self, mul_eq_zero], + norm_num +end + +/-- Pythagorean theorem, vector inner product form. -/ +lemma norm_add_square_eq_norm_square_add_norm_square_real {x y : F} (h : ⟪x, y⟫_ℝ = 0) : + ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ := +(norm_add_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero x y).2 h + +/-- Pythagorean theorem, subtracting vectors, if-and-only-if vector +inner product form. -/ +lemma norm_sub_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero (x y : F) : + ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ ⟪x, y⟫_ℝ = 0 := +begin + rw [norm_sub_mul_self, add_right_cancel_iff, sub_eq_add_neg, add_right_eq_self, neg_eq_zero, + mul_eq_zero], + norm_num +end + +/-- Pythagorean theorem, subtracting vectors, vector inner product +form. -/ +lemma norm_sub_square_eq_norm_square_add_norm_square_real {x y : F} (h : ⟪x, y⟫_ℝ = 0) : + ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ := +(norm_sub_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero x y).2 h + +/-- The sum and difference of two vectors are orthogonal if and only +if they have the same norm. -/ +lemma real_inner_add_sub_eq_zero_iff (x y : F) : ⟪x + y, x - y⟫_ℝ = 0 ↔ ∥x∥ = ∥y∥ := +begin + conv_rhs { rw ←mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _) }, + simp only [←inner_self_eq_norm_square, inner_add_left, inner_sub_right, + real_inner_comm y x, sub_eq_zero, re_to_real], + split, + { intro h, + rw [add_comm] at h, + linarith }, + { intro h, + linarith } +end + +/-- The real inner product of two vectors, divided by the product of their +norms, has absolute value at most 1. -/ +lemma abs_real_inner_div_norm_mul_norm_le_one (x y : F) : absR (⟪x, y⟫_ℝ / (∥x∥ * ∥y∥)) ≤ 1 := +begin + rw _root_.abs_div, + by_cases h : 0 = absR (∥x∥ * ∥y∥), + { rw [←h, div_zero], + norm_num }, + { change 0 ≠ absR (∥x∥ * ∥y∥) at h, + rw div_le_iff' (lt_of_le_of_ne (ge_iff_le.mp (_root_.abs_nonneg (∥x∥ * ∥y∥))) h), + convert abs_real_inner_le_norm x y using 1, + rw [_root_.abs_mul, _root_.abs_of_nonneg (norm_nonneg x), _root_.abs_of_nonneg (norm_nonneg y), mul_one] } +end + +/-- The inner product of a vector with a multiple of itself. -/ +lemma real_inner_smul_self_left (x : F) (r : ℝ) : ⟪r • x, x⟫_ℝ = r * (∥x∥ * ∥x∥) := +by rw [real_inner_smul_left, ←real_inner_self_eq_norm_square] + +/-- The inner product of a vector with a multiple of itself. -/ +lemma real_inner_smul_self_right (x : F) (r : ℝ) : ⟪x, r • x⟫_ℝ = r * (∥x∥ * ∥x∥) := +by rw [inner_smul_right, ←real_inner_self_eq_norm_square] + +/-- The inner product of a nonzero vector with a nonzero multiple of +itself, divided by the product of their norms, has absolute value +1. -/ +lemma abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul + {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) : absR ⟪x, r • x⟫_ℝ / (∥x∥ * ∥r • x∥) = 1 := +begin + simp [real_inner_smul_self_right, norm_smul, _root_.abs_mul, norm_eq_abs], + conv_lhs { congr, rw [←mul_assoc, mul_comm] }, + apply div_self, + intro h, + rcases (mul_eq_zero.mp h) with h₁|h₂, + { exact hx (norm_eq_zero.mp h₁) }, + { rcases (mul_eq_zero.mp h₂) with h₂'|h₂'', + { rw [_root_.abs_eq_zero] at h₂', + exact hr h₂' }, + { exact hx (norm_eq_zero.mp h₂'') } } +end + +/-- The inner product of a nonzero vector with a positive multiple of +itself, divided by the product of their norms, has value 1. -/ +lemma real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul + {x : F} {r : ℝ} (hx : x ≠ 0) (hr : 0 < r) : ⟪x, r • x⟫_ℝ / (∥x∥ * ∥r • x∥) = 1 := +begin + rw [real_inner_smul_self_right, norm_smul, norm_eq_abs, ←mul_assoc ∥x∥, mul_comm _ (absR r), + mul_assoc, _root_.abs_of_nonneg (le_of_lt hr), div_self], + exact mul_ne_zero (ne_of_gt hr) + (λ h, hx (norm_eq_zero.1 (eq_zero_of_mul_self_eq_zero h))) +end + +/-- The inner product of a nonzero vector with a negative multiple of +itself, divided by the product of their norms, has value -1. -/ +lemma real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul + {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r < 0) : ⟪x, r • x⟫_ℝ / (∥x∥ * ∥r • x∥) = -1 := +begin + rw [real_inner_smul_self_right, norm_smul, real.norm_eq_abs, ←mul_assoc ∥x∥, mul_comm _ (absR r), + mul_assoc, abs_of_neg hr, ←neg_mul_eq_neg_mul, div_neg_eq_neg_div, div_self], + exact mul_ne_zero (ne_of_lt hr) + (λ h, hx (norm_eq_zero.1 (eq_zero_of_mul_self_eq_zero h))) +end + +/-- The inner product of two vectors, divided by the product of their +norms, has absolute value 1 if and only if they are nonzero and one is +a multiple of the other. One form of equality case for Cauchy-Schwarz. -/ +lemma abs_real_inner_div_norm_mul_norm_eq_one_iff (x y : F) : + absR (⟪x, y⟫_ℝ / (∥x∥ * ∥y∥)) = 1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r ≠ 0 ∧ y = r • x) := +begin + split, + { intro h, + have hx0 : x ≠ 0, + { intro hx0, + rw [hx0, inner_zero_left, zero_div] at h, + norm_num at h, + exact h }, + refine and.intro hx0 _, + set r := inner x y / (∥x∥ * ∥x∥) with hr, + use r, + set t := y - r • x with ht, + have ht0 : ⟪x, t⟫_ℝ = 0, + { rw [ht, inner_sub_right, inner_smul_right, hr, ←real_inner_self_eq_norm_square, + div_mul_cancel _ (λ h, hx0 (inner_self_eq_zero.1 h)), sub_self] }, + rw [←sub_add_cancel y (r • x), ←ht, inner_add_right, ht0, zero_add, inner_smul_right, + real_inner_self_eq_norm_square, ←mul_assoc, mul_comm, + mul_div_mul_left _ _ (λ h, hx0 (norm_eq_zero.1 h)), _root_.abs_div, _root_.abs_mul, + _root_.abs_of_nonneg (norm_nonneg _), _root_.abs_of_nonneg (norm_nonneg _), ←real.norm_eq_abs, + ←norm_smul] at h, + have hr0 : r ≠ 0, + { intro hr0, + rw [hr0, zero_smul, norm_zero, zero_div] at h, + norm_num at h }, + refine and.intro hr0 _, + have h2 : ∥r • x∥ ^ 2 = ∥t + r • x∥ ^ 2, + { rw [eq_of_div_eq_one h] }, + rw [pow_two, pow_two, ←real_inner_self_eq_norm_square, ←real_inner_self_eq_norm_square, + inner_add_add_self] at h2, + conv_rhs at h2 { + congr, + congr, + skip, + rw [real_inner_smul_left, ht0, mul_zero] + }, + symmetry' at h2, + have h₁ : ⟪t, r • x⟫_ℝ = 0 := by rw [inner_smul_right, real_inner_comm, ht0, mul_zero], + rw [add_zero, h₁, add_left_eq_self, add_zero, inner_self_eq_zero] at h2, + rw h2 at ht, + exact eq_of_sub_eq_zero ht.symm }, + { intro h, + rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, + rw hy, + rw [_root_.abs_div, _root_.abs_mul, abs_norm_eq_norm, abs_norm_eq_norm], + exact abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr } +end + +/-- The inner product of two vectors, divided by the product of their +norms, has value 1 if and only if they are nonzero and one is +a positive multiple of the other. -/ +lemma real_inner_div_norm_mul_norm_eq_one_iff (x y : F) : + ⟪x, y⟫_ℝ / (∥x∥ * ∥y∥) = 1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x) := +begin + split, + { intro h, + have ha := h, + apply_fun absR at ha, + norm_num at ha, + rcases (abs_real_inner_div_norm_mul_norm_eq_one_iff x y).1 ha with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, + use [hx, r], + refine and.intro _ hy, + by_contradiction hrneg, + rw hy at h, + rw real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul hx + (lt_of_le_of_ne (le_of_not_lt hrneg) hr) at h, + norm_num at h }, + { intro h, + rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, + rw hy, + exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr } +end + +/-- The inner product of two vectors, divided by the product of their +norms, has value -1 if and only if they are nonzero and one is +a negative multiple of the other. -/ +lemma real_inner_div_norm_mul_norm_eq_neg_one_iff (x y : F) : + ⟪x, y⟫_ℝ / (∥x∥ * ∥y∥) = -1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r < 0 ∧ y = r • x) := +begin + split, + { intro h, + have ha := h, + apply_fun absR at ha, + norm_num at ha, + rcases (abs_real_inner_div_norm_mul_norm_eq_one_iff x y).1 ha with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, + use [hx, r], + refine and.intro _ hy, + by_contradiction hrpos, + rw hy at h, + rw real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx + (lt_of_le_of_ne (le_of_not_lt hrpos) hr.symm) at h, + norm_num at h }, + { intro h, + rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, + rw hy, + exact real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul hx hr } +end + +/-- The inner product of two weighted sums, where the weights in each +sum add to 0, in terms of the norms of pairwise differences. -/ +lemma inner_sum_smul_sum_smul_of_sum_eq_zero {ι₁ : Type*} {s₁ : finset ι₁} {w₁ : ι₁ → ℝ} + (v₁ : ι₁ → F) (h₁ : ∑ i in s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : finset ι₂} {w₂ : ι₂ → ℝ} + (v₂ : ι₂ → F) (h₂ : ∑ i in s₂, w₂ i = 0) : + ⟪(∑ i₁ in s₁, w₁ i₁ • v₁ i₁), (∑ i₂ in s₂, w₂ i₂ • v₂ i₂)⟫_ℝ = + (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (∥v₁ i₁ - v₂ i₂∥ * ∥v₁ i₁ - v₂ i₂∥)) / 2 := +by simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right, + real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, + ←div_sub_div_same, ←div_add_div_same, mul_sub_left_distrib, left_distrib, + finset.sum_sub_distrib, finset.sum_add_distrib, ←finset.mul_sum, ←finset.sum_mul, + h₁, h₂, zero_mul, mul_zero, finset.sum_const_zero, zero_add, zero_sub, finset.mul_sum, + neg_div, finset.sum_div, mul_div_assoc, mul_assoc] + +end norm + +/-! ### Inner product space structure on product spaces -/ + +/- + 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. 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), + norm_sq_eq_inner := + begin + intro x, + have h₁ : ∑ (i : ι), ∥x i∥ ^ (2 : ℕ) = ∑ (i : ι), ∥x i∥ ^ (2 : ℝ), + { apply finset.sum_congr rfl, + intros j hj, + simp [←rpow_nat_cast] }, + have h₂ : 0 ≤ ∑ (i : ι), ∥x i∥ ^ (2 : ℝ), + { rw [←h₁], + exact finset.sum_nonneg (λ (j : ι) (hj : j ∈ finset.univ), pow_nonneg (norm_nonneg (x j)) 2) }, + simp [norm, add_monoid_hom.map_sum, ←norm_sq_eq_inner], + rw [←rpow_nat_cast ((∑ (i : ι), ∥x i∥ ^ (2 : ℝ)) ^ (2 : ℝ)⁻¹) 2], + rw [←rpow_mul h₂], + norm_num [h₁], + end, + conj_sym := + begin + intros x y, + unfold inner, + rw [←finset.sum_hom finset.univ conj], + apply finset.sum_congr rfl, + rintros z -, + apply inner_conj_sym, + apply_instance + end, + nonneg_im := + begin + intro x, + unfold inner, + rw[←finset.sum_hom finset.univ im], + apply finset.sum_eq_zero, + rintros z -, + exact inner_self_nonneg_im, + apply_instance + end, + 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) = (conj r) * ∑ i, inner (x i) (y i), + by simp only [finset.mul_sum, inner_smul_left] +} + +/-- A field `𝕜` satisfying `is_R_or_C` is itself a `𝕜`-inner product space. -/ +instance is_R_or_C.inner_product_space : inner_product_space 𝕜 𝕜 := +{ inner := (λ x y, (conj x) * y), + norm_sq_eq_inner := λ x, by unfold inner; rw [mul_comm, mul_conj, of_real_re, norm_sq, norm_sq_eq_def], + conj_sym := λ x y, by simp [mul_comm], + nonneg_im := λ x, by rw[mul_im, conj_re, conj_im]; ring, + add_left := λ x y z, by simp [inner, add_mul], + smul_left := λ x y z, by simp [inner, mul_assoc] } + + +/-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space +use `euclidean_space 𝕜 (fin n)`. -/ +@[reducible, nolint unused_arguments] +def euclidean_space (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [is_R_or_C 𝕜] + (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), 𝕜) + +section is_R_or_C_to_real + +variables {G : Type*} + +variables (𝕜) +include 𝕜 + +/-- A general inner product implies a real inner product. This is not registered as an instance +since it creates problems with the case `𝕜 = ℝ`. -/ +def has_inner.is_R_or_C_to_real : has_inner ℝ E := +{ inner := λ x y, re ⟪x, y⟫ } + +lemma real_inner_eq_re_inner (x y : E) : + @has_inner.inner ℝ E (has_inner.is_R_or_C_to_real 𝕜) x y = re ⟪x, y⟫ := rfl + +/-- A general inner product space structure implies a real inner product structure. This is not +registered as an instance since it creates problems with the case `𝕜 = ℝ`, but in can be used in a +proof to obtain a real inner product space structure from a given `𝕜`-inner product space +structure. -/ +def inner_product_space.is_R_or_C_to_real : inner_product_space ℝ E := +{ norm_sq_eq_inner := norm_sq_eq_inner, + conj_sym := λ x y, inner_re_symm, + nonneg_im := λ x, rfl, + add_left := λ x y z, by { change re ⟪x + y, z⟫ = re ⟪x, z⟫ + re ⟪y, z⟫, simp [inner_add_left] }, + smul_left := + begin + intros x y r, + change re ⟪(algebra_map ℝ 𝕜 r) • x, y⟫ = r * re ⟪x, y⟫, + have : algebra_map ℝ 𝕜 r = r • (1 : 𝕜) := by simp [algebra_map, algebra.smul_def'], + simp [this, inner_smul_left, smul_coe_mul_ax], + end, + ..has_inner.is_R_or_C_to_real 𝕜, + ..normed_space.restrict_scalars' ℝ 𝕜 E } + +omit 𝕜 + +/-- A complex inner product implies a real inner product -/ +instance inner_product_space.complex_to_real [inner_product_space ℂ G] : inner_product_space ℝ G := +inner_product_space.is_R_or_C_to_real ℂ + +end is_R_or_C_to_real + +section pi_Lp +local attribute [reducible] pi_Lp +variables {ι : Type*} [fintype ι] + +instance : finite_dimensional 𝕜 (euclidean_space 𝕜 ι) := by apply_instance + +@[simp] lemma findim_euclidean_space : + finite_dimensional.findim 𝕜 (euclidean_space 𝕜 ι) = fintype.card ι := by simp + +lemma findim_euclidean_space_fin {n : ℕ} : + finite_dimensional.findim 𝕜 (euclidean_space 𝕜 (fin n)) = n := by simp + +end pi_Lp + + +/-! ### Orthogonal projection in inner product spaces -/ + +section orthogonal + +open filter + +/-- +Existence of minimizers +Let `u` be a point in a real inner product space, and let `K` be a nonempty complete convex subset. +Then there exists a (unique) `v` in `K` that minimizes the distance `∥u - v∥` to `u`. + -/ +-- FIXME this monolithic proof causes a deterministic timeout with `-T50000` +-- It should be broken in a sequence of more manageable pieces, +-- perhaps with individual statements for the three steps below. +theorem exists_norm_eq_infi_of_complete_convex {K : set F} (ne : K.nonempty) (h₁ : is_complete K) + (h₂ : convex K) : ∀ u : F, ∃ v ∈ K, ∥u - v∥ = ⨅ w : K, ∥u - w∥ := assume u, +begin + let δ := ⨅ w : K, ∥u - w∥, + letI : nonempty K := ne.to_subtype, + have zero_le_δ : 0 ≤ δ := le_cinfi (λ _, norm_nonneg _), + have δ_le : ∀ w : K, δ ≤ ∥u - w∥, + from cinfi_le ⟨0, set.forall_range_iff.2 $ λ _, norm_nonneg _⟩, + have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩, + -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K` + -- such that `∥u - w n∥ < δ + 1 / (n + 1)` (which implies `∥u - w n∥ --> δ`); + -- maybe this should be a separate lemma + have exists_seq : ∃ w : ℕ → K, ∀ n, ∥u - w n∥ < δ + 1 / (n + 1), + { have hδ : ∀n:ℕ, δ < δ + 1 / (n + 1), from + λ n, lt_add_of_le_of_pos (le_refl _) nat.one_div_pos_of_nat, + have h := λ n, exists_lt_of_cinfi_lt (hδ n), + let w : ℕ → K := λ n, classical.some (h n), + exact ⟨w, λ n, classical.some_spec (h n)⟩ }, + rcases exists_seq with ⟨w, hw⟩, + have norm_tendsto : tendsto (λ n, ∥u - w n∥) at_top (nhds δ), + { have h : tendsto (λ n:ℕ, δ) at_top (nhds δ) := tendsto_const_nhds, + have h' : tendsto (λ n:ℕ, δ + 1 / (n + 1)) at_top (nhds δ), + { convert h.add tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero] }, + exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h' + (λ x, δ_le _) (λ x, le_of_lt (hw _)) }, + -- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence + have seq_is_cauchy : cauchy_seq (λ n, ((w n):F)), + { rw cauchy_seq_iff_le_tendsto_0, -- splits into three goals + let b := λ n:ℕ, (8 * δ * (1/(n+1)) + 4 * (1/(n+1)) * (1/(n+1))), + use (λn, sqrt (b n)), + split, + -- first goal : `∀ (n : ℕ), 0 ≤ sqrt (b n)` + assume n, exact sqrt_nonneg _, + split, + -- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ sqrt (b N)` + assume p q N hp hq, + let wp := ((w p):F), let wq := ((w q):F), + let a := u - wq, let b := u - wp, + let half := 1 / (2:ℝ), let div := 1 / ((N:ℝ) + 1), + have : 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ = + 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) := + calc + 4 * ∥u - half•(wq + wp)∥ * ∥u - half•(wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ + = (2*∥u - half•(wq + wp)∥) * (2 * ∥u - half•(wq + wp)∥) + ∥wp-wq∥*∥wp-wq∥ : by ring + ... = (absR ((2:ℝ)) * ∥u - half•(wq + wp)∥) * (absR ((2:ℝ)) * ∥u - half•(wq+wp)∥) + ∥wp-wq∥*∥wp-wq∥ : + by { rw _root_.abs_of_nonneg, exact add_nonneg zero_le_one zero_le_one } + ... = ∥(2:ℝ) • (u - half • (wq + wp))∥ * ∥(2:ℝ) • (u - half • (wq + wp))∥ + ∥wp-wq∥ * ∥wp-wq∥ : + by simp [norm_smul] + ... = ∥a + b∥ * ∥a + b∥ + ∥a - b∥ * ∥a - b∥ : + begin + rw [smul_sub, smul_smul, mul_one_div_cancel (_root_.two_ne_zero : (2 : ℝ) ≠ 0), + ← one_add_one_eq_two, add_smul], + simp only [one_smul], + have eq₁ : wp - wq = a - b := calc + wp - wq = (u - wq) - (u - wp) : by rw [sub_sub_assoc_swap, add_sub_assoc, sub_add_sub_cancel'] + ... = a - b : rfl, + have eq₂ : u + u - (wq + wp) = a + b, show u + u - (wq + wp) = (u - wq) + (u - wp), abel, + rw [eq₁, eq₂], + end + ... = 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) : parallelogram_law_with_norm, + have eq : δ ≤ ∥u - half • (wq + wp)∥, + { rw smul_add, + apply δ_le', apply h₂, + repeat {exact subtype.mem _}, + repeat {exact le_of_lt one_half_pos}, + exact add_halves 1 }, + have eq₁ : 4 * δ * δ ≤ 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥, + { mono, mono, norm_num, apply mul_nonneg, norm_num, exact norm_nonneg _ }, + have eq₂ : ∥a∥ * ∥a∥ ≤ (δ + div) * (δ + div) := + mul_self_le_mul_self (norm_nonneg _) + (le_trans (le_of_lt $ hw q) (add_le_add_left (nat.one_div_le_one_div hq) _)), + have eq₂' : ∥b∥ * ∥b∥ ≤ (δ + div) * (δ + div) := + mul_self_le_mul_self (norm_nonneg _) + (le_trans (le_of_lt $ hw p) (add_le_add_left (nat.one_div_le_one_div hp) _)), + rw dist_eq_norm, + apply nonneg_le_nonneg_of_squares_le, { exact sqrt_nonneg _ }, + rw mul_self_sqrt, + exact calc + ∥wp - wq∥ * ∥wp - wq∥ = 2 * (∥a∥*∥a∥ + ∥b∥*∥b∥) - 4 * ∥u - half • (wq+wp)∥ * ∥u - half • (wq+wp)∥ : + by { rw ← this, simp } + ... ≤ 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) - 4 * δ * δ : sub_le_sub_left eq₁ _ + ... ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ : + sub_le_sub_right (mul_le_mul_of_nonneg_left (add_le_add eq₂ eq₂') (by norm_num)) _ + ... = 8 * δ * div + 4 * div * div : by ring, + exact add_nonneg (mul_nonneg (mul_nonneg (by norm_num) zero_le_δ) (le_of_lt nat.one_div_pos_of_nat)) + (mul_nonneg (mul_nonneg (by norm_num) (le_of_lt nat.one_div_pos_of_nat)) (le_of_lt nat.one_div_pos_of_nat)), + -- third goal : `tendsto (λ (n : ℕ), sqrt (b n)) at_top (𝓝 0)` + apply tendsto.comp, + { convert continuous_sqrt.continuous_at, exact sqrt_zero.symm }, + have eq₁ : tendsto (λ (n : ℕ), 8 * δ * (1 / (n + 1))) at_top (nhds (0:ℝ)), + { convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_at_top_nhds_0_nat, + simp only [mul_zero] }, + have : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1))) at_top (nhds (0:ℝ)), + { convert (@tendsto_const_nhds _ _ _ (4:ℝ) _).mul tendsto_one_div_add_at_top_nhds_0_nat, + simp only [mul_zero] }, + have eq₂ : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (nhds (0:ℝ)), + { convert this.mul tendsto_one_div_add_at_top_nhds_0_nat, + simp only [mul_zero] }, + convert eq₁.add eq₂, simp only [add_zero] }, + -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`. + -- Prove that it satisfies all requirements. + rcases cauchy_seq_tendsto_of_is_complete h₁ (λ n, _) seq_is_cauchy with ⟨v, hv, w_tendsto⟩, + use v, use hv, + have h_cont : continuous (λ v, ∥u - v∥) := + continuous.comp continuous_norm (continuous.sub continuous_const continuous_id), + have : tendsto (λ n, ∥u - w n∥) at_top (nhds ∥u - v∥), + convert (tendsto.comp h_cont.continuous_at w_tendsto), + exact tendsto_nhds_unique this norm_tendsto, + exact subtype.mem _ +end + +/-- Characterization of minimizers for the projection on a convex set in a real inner product +space. -/ +theorem norm_eq_infi_iff_real_inner_le_zero {K : set F} (h : convex K) {u : F} {v : F} + (hv : v ∈ K) : ∥u - v∥ = (⨅ w : K, ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := +iff.intro +begin + assume eq w hw, + let δ := ⨅ w : K, ∥u - w∥, let p := ⟪u - v, w - v⟫_ℝ, let q := ∥w - v∥^2, + letI : nonempty K := ⟨⟨v, hv⟩⟩, + have zero_le_δ : 0 ≤ δ, + apply le_cinfi, intro, exact norm_nonneg _, + have δ_le : ∀ w : K, δ ≤ ∥u - w∥, + assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _, + have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩, + have : ∀θ:ℝ, 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q, + assume θ hθ₁ hθ₂, + have : ∥u - v∥^2 ≤ ∥u - v∥^2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ*θ*∥w - v∥^2 := + calc + ∥u - v∥^2 ≤ ∥u - (θ•w + (1-θ)•v)∥^2 : + begin + simp only [pow_two], apply mul_self_le_mul_self (norm_nonneg _), + rw [eq], apply δ_le', + apply h hw hv, + exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _], + end + ... = ∥(u - v) - θ • (w - v)∥^2 : + begin + have : u - (θ•w + (1-θ)•v) = (u - v) - θ • (w - v), + { rw [smul_sub, sub_smul, one_smul], + simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev] }, + rw this + end + ... = ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 : + begin + rw [norm_sub_pow_two, inner_smul_right, norm_smul], + simp only [pow_two], + show ∥u-v∥*∥u-v∥-2*(θ*inner(u-v)(w-v))+absR (θ)*∥w-v∥*(absR (θ)*∥w-v∥)= + ∥u-v∥*∥u-v∥-2*θ*inner(u-v)(w-v)+θ*θ*(∥w-v∥*∥w-v∥), + rw abs_of_pos hθ₁, ring + end, + have eq₁ : ∥u-v∥^2-2*θ*inner(u-v)(w-v)+θ*θ*∥w-v∥^2=∥u-v∥^2+(θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)), abel, + rw [eq₁, le_add_iff_nonneg_right] at this, + have eq₂ : θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)=θ*(θ*∥w-v∥^2-2*inner(u-v)(w-v)), ring, + rw eq₂ at this, + have := le_of_sub_nonneg (nonneg_of_mul_nonneg_left this hθ₁), + exact this, + by_cases hq : q = 0, + { rw hq at this, + have : p ≤ 0, + have := this (1:ℝ) (by norm_num) (by norm_num), + linarith, + exact this }, + { have q_pos : 0 < q, + apply lt_of_le_of_ne, exact pow_two_nonneg _, intro h, exact hq h.symm, + by_contradiction hp, rw not_le at hp, + let θ := min (1:ℝ) (p / q), + have eq₁ : θ*q ≤ p := calc + θ*q ≤ (p/q) * q : mul_le_mul_of_nonneg_right (min_le_right _ _) (pow_two_nonneg _) + ... = p : div_mul_cancel _ hq, + have : 2 * p ≤ p := calc + 2 * p ≤ θ*q : by { refine this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num) } + ... ≤ p : eq₁, + linarith } +end +begin + assume h, + letI : nonempty K := ⟨⟨v, hv⟩⟩, + apply le_antisymm, + { apply le_cinfi, assume w, + apply nonneg_le_nonneg_of_squares_le (norm_nonneg _), + have := h w w.2, + exact calc + ∥u - v∥ * ∥u - v∥ ≤ ∥u - v∥ * ∥u - v∥ - 2 * inner (u - v) ((w:F) - v) : by linarith + ... ≤ ∥u - v∥^2 - 2 * inner (u - v) ((w:F) - v) + ∥(w:F) - v∥^2 : + by { rw pow_two, refine le_add_of_nonneg_right _, exact pow_two_nonneg _ } + ... = ∥(u - v) - (w - v)∥^2 : norm_sub_pow_two.symm + ... = ∥u - w∥ * ∥u - w∥ : + by { have : (u - v) - (w - v) = u - w, abel, rw [this, pow_two] } }, + { show (⨅ (w : K), ∥u - w∥) ≤ (λw:K, ∥u - w∥) ⟨v, hv⟩, + apply cinfi_le, use 0, rintros y ⟨z, rfl⟩, exact norm_nonneg _ } +end + +/-- +Existence of projections on complete subspaces. +Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace. +Then there exists a (unique) `v` in `K` that minimizes the distance `∥u - v∥` to `u`. +This point `v` is usually called the orthogonal projection of `u` onto `K`. +-/ +theorem exists_norm_eq_infi_of_complete_subspace (K : subspace 𝕜 E) + (h : is_complete (↑K : set E)) : ∀ u : E, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (K : set E), ∥u - w∥ := +begin + letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜, + let K' : subspace ℝ E := K.restrict_scalars ℝ, + exact exists_norm_eq_infi_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex +end + +/-- +Characterization of minimizers in the projection on a subspace, in the real case. +Let `u` be a point in a real inner product space, and let `K` be a nonempty subspace. +Then point `v` minimizes the distance `∥u - v∥` over points in `K` if and only if +for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`). +This is superceded by `norm_eq_infi_iff_inner_eq_zero` that gives the same conclusion over +any `is_R_or_C` field. +-/ +theorem norm_eq_infi_iff_real_inner_eq_zero (K : subspace ℝ F) {u : F} {v : F} + (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set F), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0 := +iff.intro +begin + assume h, + have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0, + { rwa [norm_eq_infi_iff_real_inner_le_zero] at h, exacts [K.convex, hv] }, + assume w hw, + have le : ⟪u - v, w⟫_ℝ ≤ 0, + let w' := w + v, + have : w' ∈ K := submodule.add_mem _ hw hv, + have h₁ := h w' this, + have h₂ : w' - v = w, simp only [add_neg_cancel_right, sub_eq_add_neg], + rw h₂ at h₁, exact h₁, + have ge : ⟪u - v, w⟫_ℝ ≥ 0, + let w'' := -w + v, + have : w'' ∈ K := submodule.add_mem _ (submodule.neg_mem _ hw) hv, + have h₁ := h w'' this, + have h₂ : w'' - v = -w, simp only [neg_inj, add_neg_cancel_right, sub_eq_add_neg], + rw [h₂, inner_neg_right] at h₁, + linarith, + exact le_antisymm le ge +end +begin + assume h, + have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0, + assume w hw, + let w' := w - v, + have : w' ∈ K := submodule.sub_mem _ hw hv, + have h₁ := h w' this, + exact le_of_eq h₁, + rwa norm_eq_infi_iff_real_inner_le_zero, + exacts [submodule.convex _, hv] +end + +/-- +Characterization of minimizers in the projection on a subspace. +Let `u` be a point in an inner product space, and let `K` be a nonempty subspace. +Then point `v` minimizes the distance `∥u - v∥` over points in `K` if and only if +for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`) +-/ +theorem norm_eq_infi_iff_inner_eq_zero (K : subspace 𝕜 E) {u : E} {v : E} + (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set E), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0 := +begin + letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜, + let K' : subspace ℝ E := K.restrict_scalars ℝ, + split, + { assume H, + have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (norm_eq_infi_iff_real_inner_eq_zero K' hv).1 H, + assume w hw, + apply ext, + { simp [A w hw] }, + { symmetry, calc + im (0 : 𝕜) = 0 : im.map_zero + ... = re ⟪u - v, (-I) • w⟫ : (A _ (K.smul_mem (-I) hw)).symm + ... = re ((-I) * ⟪u - v, w⟫) : by rw inner_smul_right + ... = im ⟪u - v, w⟫ : by simp } }, + { assume H, + have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0, + { assume w hw, + rw [real_inner_eq_re_inner, H w hw], + exact zero_re' }, + exact (norm_eq_infi_iff_real_inner_eq_zero K' hv).2 this } +end + +/-- The orthogonal projection onto a complete subspace, as an +unbundled function. This definition is only intended for use in +setting up the bundled version `orthogonal_projection` and should not +be used once that is defined. -/ +def orthogonal_projection_fn {K : subspace 𝕜 E} (h : is_complete (K : set E)) (v : E) := +(exists_norm_eq_infi_of_complete_subspace K h v).some + +/-- The unbundled orthogonal projection is in the given subspace. +This lemma is only intended for use in setting up the bundled version +and should not be used once that is defined. -/ +lemma orthogonal_projection_fn_mem {K : submodule 𝕜 E} (h : is_complete (K : set E)) (v : E) : + orthogonal_projection_fn h v ∈ K := +(exists_norm_eq_infi_of_complete_subspace K h v).some_spec.some + +/-- The characterization of the unbundled orthogonal projection. This +lemma is only intended for use in setting up the bundled version +and should not be used once that is defined. -/ +lemma orthogonal_projection_fn_inner_eq_zero {K : submodule 𝕜 E} (h : is_complete (K : set E)) + (v : E) : ∀ w ∈ K, ⟪v - orthogonal_projection_fn h v, w⟫ = 0 := +begin + rw ←norm_eq_infi_iff_inner_eq_zero K (orthogonal_projection_fn_mem h v), + exact (exists_norm_eq_infi_of_complete_subspace K h v).some_spec.some_spec +end + +/-- The unbundled orthogonal projection is the unique point in `K` +with the orthogonality property. This lemma is only intended for use +in setting up the bundled version and should not be used once that is +defined. -/ +lemma eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero {K : submodule 𝕜 E} + (h : is_complete (K : set E)) {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) : + v = orthogonal_projection_fn h u := +begin + rw [←sub_eq_zero, ←inner_self_eq_zero], + have hvs : v - orthogonal_projection_fn h u ∈ K := + submodule.sub_mem K hvm (orthogonal_projection_fn_mem h u), + have huo : ⟪u - orthogonal_projection_fn h u, v - orthogonal_projection_fn h u⟫ = 0 := + orthogonal_projection_fn_inner_eq_zero h u _ hvs, + have huv : ⟪u - v, v - orthogonal_projection_fn h u⟫ = 0 := hvo _ hvs, + have houv : ⟪(u - orthogonal_projection_fn h u) - (u - v), v - orthogonal_projection_fn h u⟫ = 0, + { rw [inner_sub_left, huo, huv, sub_zero] }, + rwa sub_sub_sub_cancel_left at houv +end + +/-- The orthogonal projection onto a complete subspace. For most +purposes, `orthogonal_projection`, which removes the `is_complete` +hypothesis and is the identity map when the subspace is not complete, +should be used instead. -/ +def orthogonal_projection_of_complete {K : submodule 𝕜 E} (h : is_complete (K : set E)) : + linear_map 𝕜 E E := +{ to_fun := orthogonal_projection_fn h, + map_add' := λ x y, begin + have hm : orthogonal_projection_fn h x + orthogonal_projection_fn h y ∈ K := + submodule.add_mem K (orthogonal_projection_fn_mem h x) (orthogonal_projection_fn_mem h y), + have ho : + ∀ w ∈ K, ⟪x + y - (orthogonal_projection_fn h x + orthogonal_projection_fn h y), w⟫ = 0, + { intros w hw, + rw [add_sub_comm, inner_add_left, orthogonal_projection_fn_inner_eq_zero h _ w hw, + orthogonal_projection_fn_inner_eq_zero h _ w hw, add_zero] }, + rw eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hm ho + end, + map_smul' := λ c x, begin + have hm : c • orthogonal_projection_fn h x ∈ K := + submodule.smul_mem K _ (orthogonal_projection_fn_mem h x), + have ho : ∀ w ∈ K, ⟪c • x - c • orthogonal_projection_fn h x, w⟫ = 0, + { intros w hw, + rw [←smul_sub, inner_smul_left, orthogonal_projection_fn_inner_eq_zero h _ w hw, mul_zero] }, + rw eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hm ho + end } + +/-- The orthogonal projection onto a subspace, which is expected to be +complete. If the subspace is not complete, this uses the identity map +instead. -/ +def orthogonal_projection (K : submodule 𝕜 E) : linear_map 𝕜 E E := +if h : is_complete (K : set E) then orthogonal_projection_of_complete h else linear_map.id + +/-- The definition of `orthogonal_projection` using `if`. -/ +lemma orthogonal_projection_def (K : submodule 𝕜 E) : + orthogonal_projection K = + if h : is_complete (K : set E) then orthogonal_projection_of_complete h else linear_map.id := +rfl + +@[simp] +lemma orthogonal_projection_fn_eq {K : submodule 𝕜 E} (h : is_complete (K : set E)) (v : E) : + orthogonal_projection_fn h v = orthogonal_projection K v := +by { rw [orthogonal_projection_def, dif_pos h], refl } + +/-- The orthogonal projection is in the given subspace. -/ +lemma orthogonal_projection_mem {K : submodule 𝕜 E} (h : is_complete (K : set E)) (v : E) : + orthogonal_projection K v ∈ K := +begin + rw ←orthogonal_projection_fn_eq h, + exact orthogonal_projection_fn_mem h v +end + +/-- The characterization of the orthogonal projection. -/ +@[simp] +lemma orthogonal_projection_inner_eq_zero (K : submodule 𝕜 E) (v : E) : + ∀ w ∈ K, ⟪v - orthogonal_projection K v, w⟫ = 0 := +begin + simp_rw orthogonal_projection_def, + split_ifs, + { exact orthogonal_projection_fn_inner_eq_zero h v }, + { simp }, +end + +/-- The orthogonal projection is the unique point in `K` with the +orthogonality property. -/ +lemma eq_orthogonal_projection_of_mem_of_inner_eq_zero {K : submodule 𝕜 E} + (h : is_complete (K : set E)) {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) : + v = orthogonal_projection K u := +begin + rw ←orthogonal_projection_fn_eq h, + exact eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hvm hvo +end + +/-- The subspace of vectors orthogonal to a given subspace. -/ +def submodule.orthogonal (K : submodule 𝕜 E) : submodule 𝕜 E := +{ carrier := {v | ∀ u ∈ K, ⟪u, v⟫ = 0}, + zero_mem' := λ _ _, inner_zero_right, + add_mem' := λ x y hx hy u hu, by rw [inner_add_right, hx u hu, hy u hu, add_zero], + smul_mem' := λ c x hx u hu, by rw [inner_smul_right, hx u hu, mul_zero] } + +/-- When a vector is in `K.orthogonal`. -/ +lemma submodule.mem_orthogonal (K : submodule 𝕜 E) (v : E) : + v ∈ K.orthogonal ↔ ∀ u ∈ K, ⟪u, v⟫ = 0 := +iff.rfl + +/-- When a vector is in `K.orthogonal`, with the inner product the +other way round. -/ +lemma submodule.mem_orthogonal' (K : submodule 𝕜 E) (v : E) : + v ∈ K.orthogonal ↔ ∀ u ∈ K, ⟪v, u⟫ = 0 := +by simp_rw [submodule.mem_orthogonal, inner_eq_zero_sym] + +/-- A vector in `K` is orthogonal to one in `K.orthogonal`. -/ +lemma submodule.inner_right_of_mem_orthogonal {u v : E} {K : submodule 𝕜 E} (hu : u ∈ K) + (hv : v ∈ K.orthogonal) : ⟪u, v⟫ = 0 := +(K.mem_orthogonal v).1 hv u hu + +/-- A vector in `K.orthogonal` is orthogonal to one in `K`. -/ +lemma submodule.inner_left_of_mem_orthogonal {u v : E} {K : submodule 𝕜 E} (hu : u ∈ K) + (hv : v ∈ K.orthogonal) : ⟪v, u⟫ = 0 := +by rw [inner_eq_zero_sym]; exact submodule.inner_right_of_mem_orthogonal hu hv + +/-- `K` and `K.orthogonal` have trivial intersection. -/ +lemma submodule.orthogonal_disjoint (K : submodule 𝕜 E) : disjoint K K.orthogonal := +begin + simp_rw [submodule.disjoint_def, submodule.mem_orthogonal], + exact λ x hx ho, inner_self_eq_zero.1 (ho x hx) +end + +variables (𝕜 E) + +/-- `submodule.orthogonal` gives a `galois_connection` between +`submodule 𝕜 E` and its `order_dual`. -/ +lemma submodule.orthogonal_gc : + @galois_connection (submodule 𝕜 E) (order_dual $ submodule 𝕜 E) _ _ + submodule.orthogonal submodule.orthogonal := +λ K₁ K₂, ⟨λ h v hv u hu, submodule.inner_left_of_mem_orthogonal hv (h hu), + λ h v hv u hu, submodule.inner_left_of_mem_orthogonal hv (h hu)⟩ + +variables {𝕜 E} + +/-- `submodule.orthogonal` reverses the `≤` ordering of two +subspaces. -/ +lemma submodule.orthogonal_le {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) : + K₂.orthogonal ≤ K₁.orthogonal := +(submodule.orthogonal_gc 𝕜 E).monotone_l h + + +/-- `K` is contained in `K.orthogonal.orthogonal`. -/ +lemma submodule.le_orthogonal_orthogonal (K : submodule 𝕜 E) : K ≤ K.orthogonal.orthogonal := +(submodule.orthogonal_gc 𝕜 E).le_u_l _ + +/-- The inf of two orthogonal subspaces equals the subspace orthogonal +to the sup. -/ +lemma submodule.inf_orthogonal (K₁ K₂ : submodule 𝕜 E) : + K₁.orthogonal ⊓ K₂.orthogonal = (K₁ ⊔ K₂).orthogonal := +(submodule.orthogonal_gc 𝕜 E).l_sup.symm + +/-- The inf of an indexed family of orthogonal subspaces equals the +subspace orthogonal to the sup. -/ +lemma submodule.infi_orthogonal {ι : Type*} (K : ι → submodule 𝕜 E) : + (⨅ i, (K i).orthogonal) = (supr K).orthogonal := +(submodule.orthogonal_gc 𝕜 E).l_supr.symm + +/-- The inf of a set of orthogonal subspaces equals the subspace +orthogonal to the sup. -/ +lemma submodule.Inf_orthogonal (s : set $ submodule 𝕜 E) : + (⨅ K ∈ s, submodule.orthogonal K) = (Sup s).orthogonal := +(submodule.orthogonal_gc 𝕜 E).l_Sup.symm + +/-- If `K₁` is complete and contained in `K₂`, `K₁` and `K₁.orthogonal ⊓ K₂` span `K₂`. -/ +lemma submodule.sup_orthogonal_inf_of_is_complete {K₁ K₂ : submodule 𝕜 E} (h : K₁ ≤ K₂) + (hc : is_complete (K₁ : set E)) : K₁ ⊔ (K₁.orthogonal ⊓ K₂) = K₂ := +begin + ext x, + rw submodule.mem_sup, + rcases exists_norm_eq_infi_of_complete_subspace K₁ hc x with ⟨v, hv, hvm⟩, + rw norm_eq_infi_iff_inner_eq_zero K₁ hv at hvm, + split, + { rintro ⟨y, hy, z, hz, rfl⟩, + exact K₂.add_mem (h hy) hz.2 }, + { exact λ hx, ⟨v, hv, x - v, ⟨(K₁.mem_orthogonal' _).2 hvm, K₂.sub_mem hx (h hv)⟩, + add_sub_cancel'_right _ _⟩ } +end + +/-- If `K` is complete, `K` and `K.orthogonal` span the whole +space. -/ +lemma submodule.sup_orthogonal_of_is_complete {K : submodule 𝕜 E} (h : is_complete (K : set E)) : + K ⊔ K.orthogonal = ⊤ := +begin + convert submodule.sup_orthogonal_inf_of_is_complete (le_top : K ≤ ⊤) h, + simp +end + +/-- If `K` is complete, `K` and `K.orthogonal` are complements of each +other. -/ +lemma submodule.is_compl_orthogonal_of_is_complete_real {K : submodule 𝕜 E} + (h : is_complete (K : set E)) : is_compl K K.orthogonal := +⟨K.orthogonal_disjoint, le_of_eq (submodule.sup_orthogonal_of_is_complete h).symm⟩ + +open finite_dimensional + +/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁` +containined in it, the dimensions of `K₁` and the intersection of its +orthogonal subspace with `K₂` add to that of `K₂`. -/ +lemma submodule.findim_add_inf_findim_orthogonal {K₁ K₂ : submodule 𝕜 E} + [finite_dimensional 𝕜 K₂] (h : K₁ ≤ K₂) : + findim 𝕜 K₁ + findim 𝕜 (K₁.orthogonal ⊓ K₂ : submodule 𝕜 E) = findim 𝕜 K₂ := +begin + haveI := submodule.finite_dimensional_of_le h, + have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁.orthogonal ⊓ K₂), + rw [←inf_assoc, (submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, findim_bot, + submodule.sup_orthogonal_inf_of_is_complete h + (submodule.complete_of_finite_dimensional _)] at hd, + rw add_zero at hd, + exact hd.symm +end +end orthogonal diff --git a/src/analysis/normed_space/real_inner_product.lean b/src/analysis/normed_space/real_inner_product.lean deleted file mode 100644 index 2b665cc5176c7..0000000000000 --- a/src/analysis/normed_space/real_inner_product.lean +++ /dev/null @@ -1,1186 +0,0 @@ -/- -Copyright (c) 2019 Zhouhang Zhou. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Zhouhang Zhou, Sébastien Gouëzel --/ -import algebra.quadratic_discriminant -import linear_algebra.bilinear_form -import tactic.apply_fun -import tactic.monotonicity -import topology.metric_space.pi_Lp - -/-! -# Inner Product Space - -This file defines real inner product space and proves its basic properties. - -An inner product space is a vector space endowed with an inner product. It generalizes the notion of -dot product in `ℝ^n` and provides the means of defining the length of a vector and the angle between -two vectors. In particular vectors `x` and `y` are orthogonal if their inner product equals zero. - -## Main statements - -Existence of orthogonal projection onto nonempty complete subspace: -Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace. -Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`. -The point `v` is usually called the orthogonal projection of `u` onto `K`. - -## Implementation notes - -We decide to develop the theory of real inner product spaces and that of complex inner product -spaces separately. - -## Tags - -inner product space, norm, orthogonal projection - -## References -* [Clément & Martin, *The Lax-Milgram Theorem. A detailed proof to be formalized in Coq*] -* [Clément & Martin, *A Coq formal proof of the Lax–Milgram theorem*] - -The Coq code is available at the following address: --/ - -noncomputable theory - -open real set -open_locale big_operators -open_locale classical -open_locale topological_space - -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) - --- the norm is embedded in the inner product space structure --- to avoid definitional equality issues. See Note [forgetful inheritance]. - -/-- -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 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) - -/-! -### 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) - -/- 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_add_left {x y z : α} : inner (x + y) z = inner x z + inner y z := -inner_product_space.add_left _ _ _ - -lemma inner_add_right {x y z : α} : 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 : α} {r : ℝ} : inner (r • x) y = r * inner x y := -inner_product_space.smul_left _ _ _ - -lemma inner_smul_right {x y : α} {r : ℝ} : inner x (r • y) = r * inner x y := -by { rw [inner_comm, inner_smul_left, inner_comm] } - -variables (α) - -/-- The inner product as a bilinear form. -/ -def bilin_form_of_inner : bilin_form ℝ α := -{ bilin := inner, - bilin_add_left := λ x y z, inner_add_left, - bilin_smul_left := λ a x y, inner_smul_left, - bilin_add_right := λ x y z, inner_add_right, - bilin_smul_right := λ a x y, inner_smul_right } - -variables {α} - -/-- An inner product with a sum on the left. -/ -lemma sum_inner {ι : Type*} (s : finset ι) (f : ι → α) (x : α) : - inner (∑ i in s, f i) x = ∑ i in s, inner (f i) x := -bilin_form.map_sum_left (bilin_form_of_inner α) _ _ _ - -/-- An inner product with a sum on the right. -/ -lemma inner_sum {ι : Type*} (s : finset ι) (f : ι → α) (x : α) : - inner x (∑ i in s, f i) = ∑ i in s, inner x (f i) := -bilin_form.map_sum_right (bilin_form_of_inner α) _ _ _ - -@[simp] lemma inner_zero_left {x : α} : inner 0 x = 0 := -by { rw [← zero_smul ℝ (0:α), inner_smul_left, zero_mul] } - -@[simp] lemma inner_zero_right {x : α} : inner x 0 = 0 := -by { rw [inner_comm, inner_zero_left] } - -@[simp] lemma inner_self_eq_zero {x : α} : inner x x = 0 ↔ x = 0 := -⟨λ 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), - λ h, h.symm ▸ le_of_eq inner_zero_left⟩ - -@[simp] lemma inner_neg_left {x y : α} : inner (-x) y = -inner x y := -by { rw [← neg_one_smul ℝ x, inner_smul_left], simp } - -@[simp] lemma inner_neg_right {x y : α} : inner x (-y) = -inner x y := -by { rw [inner_comm, inner_neg_left, inner_comm] } - -@[simp] lemma inner_neg_neg {x y : α} : inner (-x) (-y) = inner x y := by simp - -lemma inner_sub_left {x y z : α} : inner (x - y) z = inner x z - inner y z := -by { simp [sub_eq_add_neg, inner_add_left] } - -lemma inner_sub_right {x y z : α} : inner x (y - z) = inner x y - inner x z := -by { simp [sub_eq_add_neg, inner_add_right] } - -/-- Expand `inner (x + y) (x + y)` -/ -lemma inner_add_add_self {x y : α} : 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 _ _ - -/-- Expand `inner (x - y) (x - y)` -/ -lemma inner_sub_sub_self {x y : α} : inner (x - y) (x - y) = inner x x - 2 * inner x y + inner y y := -begin - simp only [inner_sub_left, inner_sub_right, two_mul], - simpa [sub_eq_add_neg, add_comm, add_left_comm] using inner_comm _ _ -end - -/-- Parallelogram law -/ -lemma parallelogram_law {x y : α} : - inner (x + y) (x + y) + inner (x - y) (x - y) = 2 * (inner x x + inner y y) := -by simp [inner_add_add_self, inner_sub_sub_self, two_mul, sub_eq_add_neg, add_comm, add_left_comm] - -/-- Cauchy–Schwarz inequality -/ -lemma inner_mul_inner_self_le (x y : α) : 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) : inner_self_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 - -/-- A family of vectors is linearly independent if they are nonzero -and orthogonal. -/ -lemma linear_independent_of_ne_zero_of_inner_eq_zero {ι : Type*} {v : ι → α} - (hz : ∀ i, v i ≠ 0) (ho : ∀ i j, i ≠ j → inner (v i) (v j) = 0) : linear_independent ℝ v := -begin - rw linear_independent_iff', - intros s g hg i hi, - have h' : g i * inner (v i) (v i) = inner (∑ j in s, g j • v j) (v i), - { rw sum_inner, - symmetry, - convert finset.sum_eq_single i _ _, - { rw inner_smul_left }, - { intros j hj hji, - rw [inner_smul_left, ho j i hji, mul_zero] }, - { exact λ h, false.elim (h hi) } }, - simpa [hg, hz] using h' -end - -end basic_properties - -section norm - -lemma inner_self_eq_norm_square (x : α) : inner x x = ∥x∥ * ∥x∥ := -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 := -by { repeat {rw [pow_two, ← inner_self_eq_norm_square]}, exact inner_add_add_self } - -/-- Same lemma as above but in a different form -/ -lemma norm_add_mul_self {x y : α} : ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + 2 * inner x y + ∥y∥ * ∥y∥ := -by { repeat {rw [← pow_two]}, exact norm_add_pow_two } - -/-- Expand the square -/ -lemma norm_sub_pow_two {x y : α} : ∥x - y∥^2 = ∥x∥^2 - 2 * inner x y + ∥y∥^2 := -by { repeat {rw [pow_two, ← inner_self_eq_norm_square]}, exact inner_sub_sub_self } - -/-- Same lemma as above but in a different form -/ -lemma norm_sub_mul_self {x y : α} : ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ - 2 * inner x y + ∥y∥ * ∥y∥ := -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 (norm_nonneg _) (norm_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 - -lemma parallelogram_law_with_norm {x y : α} : - ∥x + y∥ * ∥x + y∥ + ∥x - y∥ * ∥x - y∥ = 2 * (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥) := -by { simp only [(inner_self_eq_norm_square _).symm], exact parallelogram_law } - -/-- The inner product, in terms of the norm. -/ -lemma inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two (x y : α) : - inner x y = (∥x + y∥ * ∥x + y∥ - ∥x∥ * ∥x∥ - ∥y∥ * ∥y∥) / 2 := -begin - rw norm_add_mul_self, - ring -end - -/-- The inner product, in terms of the norm. -/ -lemma inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two (x y : α) : - inner x y = (∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ - ∥x - y∥ * ∥x - y∥) / 2 := -begin - rw norm_sub_mul_self, - ring -end - -/-- The inner product, in terms of the norm. -/ -lemma inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four (x y : α) : - inner x y = (∥x + y∥ * ∥x + y∥ - ∥x - y∥ * ∥x - y∥) / 4 := -begin - rw [norm_add_mul_self, norm_sub_mul_self], - ring -end - -/-- Pythagorean theorem, if-and-only-if vector inner product form. -/ -lemma norm_add_square_eq_norm_square_add_norm_square_iff_inner_eq_zero (x y : α) : - ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ inner x y = 0 := -begin - rw [norm_add_mul_self, add_right_cancel_iff, add_right_eq_self, mul_eq_zero], - norm_num -end - -/-- Pythagorean theorem, vector inner product form. -/ -lemma norm_add_square_eq_norm_square_add_norm_square {x y : α} (h : inner x y = 0) : - ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ := -(norm_add_square_eq_norm_square_add_norm_square_iff_inner_eq_zero x y).2 h - -/-- Pythagorean theorem, subtracting vectors, if-and-only-if vector -inner product form. -/ -lemma norm_sub_square_eq_norm_square_add_norm_square_iff_inner_eq_zero (x y : α) : - ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ inner x y = 0 := -begin - rw [norm_sub_mul_self, add_right_cancel_iff, sub_eq_add_neg, add_right_eq_self, neg_eq_zero, - mul_eq_zero], - norm_num -end - -/-- Pythagorean theorem, subtracting vectors, vector inner product -form. -/ -lemma norm_sub_square_eq_norm_square_add_norm_square {x y : α} (h : inner x y = 0) : - ∥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 - -/-- The sum and difference of two vectors are orthogonal if and only -if they have the same norm. -/ -lemma inner_add_sub_eq_zero_iff (x y : α) : inner (x + y) (x - y) = 0 ↔ ∥x∥ = ∥y∥ := -begin - conv_rhs { rw ←mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _) }, - simp [←inner_self_eq_norm_square, inner_add_left, inner_sub_right, inner_comm y x, - sub_eq_zero, add_comm (inner x y)] -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 := -begin - rw abs_div, - by_cases h : 0 = abs (∥x∥ * ∥y∥), - { rw [←h, div_zero], - norm_num }, - { rw div_le_iff' (lt_of_le_of_ne (ge_iff_le.mp (abs_nonneg (∥x∥ * ∥y∥))) h), - convert abs_inner_le_norm x y using 1, - rw [abs_mul, abs_of_nonneg (norm_nonneg x), abs_of_nonneg (norm_nonneg y), mul_one] } -end - -/-- The inner product of a vector with a multiple of itself. -/ -lemma inner_smul_self_left (x : α) (r : ℝ) : inner (r • x) x = r * (∥x∥ * ∥x∥) := -by rw [inner_smul_left, ←inner_self_eq_norm_square] - -/-- The inner product of a vector with a multiple of itself. -/ -lemma inner_smul_self_right (x : α) (r : ℝ) : inner x (r • x) = r * (∥x∥ * ∥x∥) := -by rw [inner_smul_right, ←inner_self_eq_norm_square] - -/-- The inner product of a nonzero vector with a nonzero multiple of -itself, divided by the product of their norms, has absolute value -1. -/ -lemma abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul - {x : α} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) : abs (inner x (r • x) / (∥x∥ * ∥r • x∥)) = 1 := -begin - rw [inner_smul_self_right, norm_smul, real.norm_eq_abs, ←mul_assoc ∥x∥, mul_comm _ (abs r), - mul_assoc, abs_div, abs_mul r, abs_mul (abs r), abs_abs, div_self], - exact mul_ne_zero (λ h, hr (eq_zero_of_abs_eq_zero h)) - (λ h, hx (norm_eq_zero.1 (eq_zero_of_mul_self_eq_zero (eq_zero_of_abs_eq_zero h)))) -end - -/-- The inner product of a nonzero vector with a positive multiple of -itself, divided by the product of their norms, has value 1. -/ -lemma inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul - {x : α} {r : ℝ} (hx : x ≠ 0) (hr : 0 < r) : inner x (r • x) / (∥x∥ * ∥r • x∥) = 1 := -begin - rw [inner_smul_self_right, norm_smul, real.norm_eq_abs, ←mul_assoc ∥x∥, mul_comm _ (abs r), - mul_assoc, abs_of_nonneg (le_of_lt hr), div_self], - exact mul_ne_zero (ne_of_gt hr) - (λ h, hx (norm_eq_zero.1 (eq_zero_of_mul_self_eq_zero h))) -end - -/-- The inner product of a nonzero vector with a negative multiple of -itself, divided by the product of their norms, has value -1. -/ -lemma inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul - {x : α} {r : ℝ} (hx : x ≠ 0) (hr : r < 0) : inner x (r • x) / (∥x∥ * ∥r • x∥) = -1 := -begin - rw [inner_smul_self_right, norm_smul, real.norm_eq_abs, ←mul_assoc ∥x∥, mul_comm _ (abs r), - mul_assoc, abs_of_neg hr, ←neg_mul_eq_neg_mul, div_neg_eq_neg_div, div_self], - exact mul_ne_zero (ne_of_lt hr) - (λ h, hx (norm_eq_zero.1 (eq_zero_of_mul_self_eq_zero h))) -end - -/-- The inner product of two vectors, divided by the product of their -norms, has absolute value 1 if and only if they are nonzero and one is -a multiple of the other. One form of equality case for Cauchy-Schwarz. -/ -lemma abs_inner_div_norm_mul_norm_eq_one_iff (x y : α) : - abs (inner x y / (∥x∥ * ∥y∥)) = 1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r ≠ 0 ∧ y = r • x) := -begin - split, - { intro h, - have hx0 : x ≠ 0, - { intro hx0, - rw [hx0, inner_zero_left, zero_div] at h, - norm_num at h, - exact h }, - refine and.intro hx0 _, - set r := inner x y / (∥x∥ * ∥x∥) with hr, - use r, - set t := y - r • x with ht, - have ht0 : inner x t = 0, - { rw [ht, inner_sub_right, inner_smul_right, hr, ←inner_self_eq_norm_square, - div_mul_cancel _ (λ h, hx0 (inner_self_eq_zero.1 h)), sub_self] }, - rw [←sub_add_cancel y (r • x), ←ht, inner_add_right, ht0, zero_add, inner_smul_right, - inner_self_eq_norm_square, ←mul_assoc, mul_comm, - mul_div_mul_left _ _ (λ h, hx0 (norm_eq_zero.1 h)), abs_div, abs_mul, - abs_of_nonneg (norm_nonneg _), abs_of_nonneg (norm_nonneg _), ←real.norm_eq_abs, - ←norm_smul] at h, - have hr0 : r ≠ 0, - { intro hr0, - rw [hr0, zero_smul, norm_zero, zero_div] at h, - norm_num at h }, - refine and.intro hr0 _, - have h2 : ∥r • x∥ ^ 2 = ∥t + r • x∥ ^ 2, - { rw [eq_of_div_eq_one h] }, - rw [pow_two, pow_two, ←inner_self_eq_norm_square, ←inner_self_eq_norm_square, - inner_add_add_self] at h2, - conv_rhs at h2 { - congr, - congr, - skip, - rw [inner_smul_right, inner_comm, ht0, mul_zero, mul_zero] - }, - symmetry' at h2, - rw [add_zero, add_left_eq_self, inner_self_eq_zero] at h2, - rw h2 at ht, - exact eq_of_sub_eq_zero ht.symm }, - { intro h, - rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, - rw hy, - exact abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr } -end - -/-- The inner product of two vectors, divided by the product of their -norms, has value 1 if and only if they are nonzero and one is -a positive multiple of the other. -/ -lemma inner_div_norm_mul_norm_eq_one_iff (x y : α) : - inner x y / (∥x∥ * ∥y∥) = 1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x) := -begin - split, - { intro h, - have ha := h, - apply_fun abs at ha, - norm_num at ha, - rcases (abs_inner_div_norm_mul_norm_eq_one_iff x y).1 ha with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, - use [hx, r], - refine and.intro _ hy, - by_contradiction hrneg, - rw hy at h, - rw inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul hx - (lt_of_le_of_ne (le_of_not_lt hrneg) hr) at h, - norm_num at h }, - { intro h, - rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, - rw hy, - exact inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr } -end - -/-- The inner product of two vectors, divided by the product of their -norms, has value -1 if and only if they are nonzero and one is -a negative multiple of the other. -/ -lemma inner_div_norm_mul_norm_eq_neg_one_iff (x y : α) : - inner x y / (∥x∥ * ∥y∥) = -1 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r < 0 ∧ y = r • x) := -begin - split, - { intro h, - have ha := h, - apply_fun abs at ha, - norm_num at ha, - rcases (abs_inner_div_norm_mul_norm_eq_one_iff x y).1 ha with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, - use [hx, r], - refine and.intro _ hy, - by_contradiction hrpos, - rw hy at h, - rw inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx - (lt_of_le_of_ne (le_of_not_lt hrpos) hr.symm) at h, - norm_num at h }, - { intro h, - rcases h with ⟨hx, ⟨r, ⟨hr, hy⟩⟩⟩, - rw hy, - exact inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul hx hr } -end - -/-- The inner product of two weighted sums, where the weights in each -sum add to 0, in terms of the norms of pairwise differences. -/ -lemma inner_sum_smul_sum_smul_of_sum_eq_zero {ι₁ : Type*} {s₁ : finset ι₁} {w₁ : ι₁ → ℝ} - (v₁ : ι₁ → α) (h₁ : ∑ i in s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : finset ι₂} {w₂ : ι₂ → ℝ} - (v₂ : ι₂ → α) (h₂ : ∑ i in s₂, w₂ i = 0) : - inner (∑ i₁ in s₁, w₁ i₁ • v₁ i₁) (∑ i₂ in s₂, w₂ i₂ • v₂ i₂) = - (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (∥v₁ i₁ - v₂ i₂∥ * ∥v₁ i₁ - v₂ i₂∥)) / 2 := -by simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, - inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, - ←div_sub_div_same, ←div_add_div_same, mul_sub_left_distrib, left_distrib, - finset.sum_sub_distrib, finset.sum_add_distrib, ←finset.mul_sum, ←finset.sum_mul, - h₁, h₂, zero_mul, mul_zero, finset.sum_const_zero, zero_add, zero_sub, finset.mul_sum, - neg_div, finset.sum_div, mul_div_assoc, mul_assoc] - -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. 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), - 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 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, - add_left := add_mul, - smul_left := λ _ _ _, mul_assoc _ _ _ } - -/-- The standard Euclidean space, functions on a finite type. For an `n`-dimensional space -use `euclidean_space (fin n)`. -/ -@[reducible, nolint unused_arguments] -def euclidean_space (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), ℝ) - -section pi_Lp -local attribute [reducible] pi_Lp -variables (n : Type*) [fintype n] - -instance : finite_dimensional ℝ (euclidean_space n) := -by apply_instance - -@[simp] lemma findim_euclidean_space : - finite_dimensional.findim ℝ (euclidean_space n) = fintype.card n := -by simp - -lemma findim_euclidean_space_fin {n : ℕ} : - finite_dimensional.findim ℝ (euclidean_space (fin n)) = n := -by simp - -end pi_Lp - -/-! ### Orthogonal projection in inner product spaces -/ -section orthogonal - -open filter - -/-- -Existence of minimizers -Let `u` be a point in an inner product space, and let `K` be a nonempty complete convex subset. -Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`. - -/ --- FIXME this monolithic proof causes a deterministic timeout with `-T50000` --- It should be broken in a sequence of more manageable pieces, --- perhaps with individual statements for the three steps below. -theorem exists_norm_eq_infi_of_complete_convex {K : set α} (ne : K.nonempty) (h₁ : is_complete K) - (h₂ : convex K) : ∀ u : α, ∃ v ∈ K, ∥u - v∥ = ⨅ w : K, ∥u - w∥ := assume u, -begin - let δ := ⨅ w : K, ∥u - w∥, - letI : nonempty K := ne.to_subtype, - have zero_le_δ : 0 ≤ δ := le_cinfi (λ _, norm_nonneg _), - have δ_le : ∀ w : K, δ ≤ ∥u - w∥, - from cinfi_le ⟨0, forall_range_iff.2 $ λ _, norm_nonneg _⟩, - have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩, - -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K` - -- such that `∥u - w n∥ < δ + 1 / (n + 1)` (which implies `∥u - w n∥ --> δ`); - -- maybe this should be a separate lemma - have exists_seq : ∃ w : ℕ → K, ∀ n, ∥u - w n∥ < δ + 1 / (n + 1), - { have hδ : ∀n:ℕ, δ < δ + 1 / (n + 1), from - λ n, lt_add_of_le_of_pos (le_refl _) nat.one_div_pos_of_nat, - have h := λ n, exists_lt_of_cinfi_lt (hδ n), - let w : ℕ → K := λ n, classical.some (h n), - exact ⟨w, λ n, classical.some_spec (h n)⟩ }, - rcases exists_seq with ⟨w, hw⟩, - have norm_tendsto : tendsto (λ n, ∥u - w n∥) at_top (𝓝 δ), - { have h : tendsto (λ n:ℕ, δ) at_top (𝓝 δ) := tendsto_const_nhds, - have h' : tendsto (λ n:ℕ, δ + 1 / (n + 1)) at_top (𝓝 δ), - { convert h.add tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero] }, - exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h' - (λ x, δ_le _) (λ x, le_of_lt (hw _)) }, - -- Step 2: Prove that the sequence `w : ℕ → K` is a Cauchy sequence - have seq_is_cauchy : cauchy_seq (λ n, ((w n):α)), - { rw cauchy_seq_iff_le_tendsto_0, -- splits into three goals - let b := λ n:ℕ, (8 * δ * (1/(n+1)) + 4 * (1/(n+1)) * (1/(n+1))), - use (λn, sqrt (b n)), - split, - -- first goal : `∀ (n : ℕ), 0 ≤ sqrt (b n)` - assume n, exact sqrt_nonneg _, - split, - -- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ sqrt (b N)` - assume p q N hp hq, - let wp := ((w p):α), let wq := ((w q):α), - let a := u - wq, let b := u - wp, - let half := 1 / (2:ℝ), let div := 1 / ((N:ℝ) + 1), - have : 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ = - 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) := - calc - 4 * ∥u - half•(wq + wp)∥ * ∥u - half•(wq + wp)∥ + ∥wp - wq∥ * ∥wp - wq∥ - = (2*∥u - half•(wq + wp)∥) * (2 * ∥u - half•(wq + wp)∥) + ∥wp-wq∥*∥wp-wq∥ : by ring - ... = (abs((2:ℝ)) * ∥u - half•(wq + wp)∥) * (abs((2:ℝ)) * ∥u - half•(wq+wp)∥) + ∥wp-wq∥*∥wp-wq∥ : - by { rw abs_of_nonneg, exact add_nonneg zero_le_one zero_le_one } - ... = ∥(2:ℝ) • (u - half • (wq + wp))∥ * ∥(2:ℝ) • (u - half • (wq + wp))∥ + ∥wp-wq∥ * ∥wp-wq∥ : - by { rw [norm_smul], refl } - ... = ∥a + b∥ * ∥a + b∥ + ∥a - b∥ * ∥a - b∥ : - begin - rw [smul_sub, smul_smul, mul_one_div_cancel (two_ne_zero : (2 : ℝ) ≠ 0), - ← one_add_one_eq_two, add_smul], - simp only [one_smul], - have eq₁ : wp - wq = a - b, show wp - wq = (u - wq) - (u - wp), abel, - have eq₂ : u + u - (wq + wp) = a + b, show u + u - (wq + wp) = (u - wq) + (u - wp), abel, - rw [eq₁, eq₂], - end - ... = 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) : parallelogram_law_with_norm, - have eq : δ ≤ ∥u - half • (wq + wp)∥, - { rw smul_add, - apply δ_le', apply h₂, - repeat {exact subtype.mem _}, - repeat {exact le_of_lt one_half_pos}, - exact add_halves 1 }, - have eq₁ : 4 * δ * δ ≤ 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥, - { mono, mono, norm_num, apply mul_nonneg, norm_num, exact norm_nonneg _ }, - have eq₂ : ∥a∥ * ∥a∥ ≤ (δ + div) * (δ + div) := - mul_self_le_mul_self (norm_nonneg _) - (le_trans (le_of_lt $ hw q) (add_le_add_left (nat.one_div_le_one_div hq) _)), - have eq₂' : ∥b∥ * ∥b∥ ≤ (δ + div) * (δ + div) := - mul_self_le_mul_self (norm_nonneg _) - (le_trans (le_of_lt $ hw p) (add_le_add_left (nat.one_div_le_one_div hp) _)), - rw dist_eq_norm, - apply nonneg_le_nonneg_of_squares_le, { exact sqrt_nonneg _ }, - rw mul_self_sqrt, - exact calc - ∥wp - wq∥ * ∥wp - wq∥ = 2 * (∥a∥*∥a∥ + ∥b∥*∥b∥) - 4 * ∥u - half • (wq+wp)∥ * ∥u - half • (wq+wp)∥ : - by { rw ← this, simp } - ... ≤ 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) - 4 * δ * δ : sub_le_sub_left eq₁ _ - ... ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ : - sub_le_sub_right (mul_le_mul_of_nonneg_left (add_le_add eq₂ eq₂') (by norm_num)) _ - ... = 8 * δ * div + 4 * div * div : by ring, - exact add_nonneg (mul_nonneg (mul_nonneg (by norm_num) zero_le_δ) (le_of_lt nat.one_div_pos_of_nat)) - (mul_nonneg (mul_nonneg (by norm_num) (le_of_lt nat.one_div_pos_of_nat)) (le_of_lt nat.one_div_pos_of_nat)), - -- third goal : `tendsto (λ (n : ℕ), sqrt (b n)) at_top (𝓝 0)` - apply tendsto.comp, - { convert continuous_sqrt.continuous_at, exact sqrt_zero.symm }, - have eq₁ : tendsto (λ (n : ℕ), 8 * δ * (1 / (n + 1))) at_top (𝓝 (0:ℝ)), - { convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_at_top_nhds_0_nat, - simp only [mul_zero] }, - have : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)), - { convert (@tendsto_const_nhds _ _ _ (4:ℝ) _).mul tendsto_one_div_add_at_top_nhds_0_nat, - simp only [mul_zero] }, - have eq₂ : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)), - { convert this.mul tendsto_one_div_add_at_top_nhds_0_nat, - simp only [mul_zero] }, - convert eq₁.add eq₂, simp only [add_zero] }, - -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`. - -- Prove that it satisfies all requirements. - rcases cauchy_seq_tendsto_of_is_complete h₁ (λ n, _) seq_is_cauchy with ⟨v, hv, w_tendsto⟩, - use v, use hv, - have h_cont : continuous (λ v, ∥u - v∥) := - continuous.comp continuous_norm (continuous.sub continuous_const continuous_id), - have : tendsto (λ n, ∥u - w n∥) at_top (𝓝 ∥u - v∥), - convert (tendsto.comp h_cont.continuous_at w_tendsto), - exact tendsto_nhds_unique this norm_tendsto, - exact subtype.mem _ -end - -/-- Characterization of minimizers in the above theorem -/ -theorem norm_eq_infi_iff_inner_le_zero {K : set α} (h : convex K) {u : α} {v : α} - (hv : v ∈ K) : ∥u - v∥ = (⨅ w : K, ∥u - w∥) ↔ ∀ w ∈ K, inner (u - v) (w - v) ≤ 0 := -iff.intro -begin - assume eq w hw, - let δ := ⨅ w : K, ∥u - w∥, let p := inner (u - v) (w - v), let q := ∥w - v∥^2, - letI : nonempty K := ⟨⟨v, hv⟩⟩, - have zero_le_δ : 0 ≤ δ, - apply le_cinfi, intro, exact norm_nonneg _, - have δ_le : ∀ w : K, δ ≤ ∥u - w∥, - assume w, apply cinfi_le, use (0:ℝ), rintros _ ⟨_, rfl⟩, exact norm_nonneg _, - have δ_le' : ∀ w ∈ K, δ ≤ ∥u - w∥ := assume w hw, δ_le ⟨w, hw⟩, - have : ∀θ:ℝ, 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q, - assume θ hθ₁ hθ₂, - have : ∥u - v∥^2 ≤ ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 := - calc - ∥u - v∥^2 ≤ ∥u - (θ•w + (1-θ)•v)∥^2 : - begin - simp only [pow_two], apply mul_self_le_mul_self (norm_nonneg _), - rw [eq], apply δ_le', - apply h hw hv, - exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _], - end - ... = ∥(u - v) - θ • (w - v)∥^2 : - begin - have : u - (θ•w + (1-θ)•v) = (u - v) - θ • (w - v), - { rw [smul_sub, sub_smul, one_smul], - simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev] }, - rw this - end - ... = ∥u - v∥^2 - 2 * θ * inner (u - v) (w - v) + θ*θ*∥w - v∥^2 : - begin - rw [norm_sub_pow_two, inner_smul_right, norm_smul], - simp only [pow_two], - show ∥u-v∥*∥u-v∥-2*(θ*inner(u-v)(w-v))+abs(θ)*∥w-v∥*(abs(θ)*∥w-v∥)= - ∥u-v∥*∥u-v∥-2*θ*inner(u-v)(w-v)+θ*θ*(∥w-v∥*∥w-v∥), - rw abs_of_pos hθ₁, ring - end, - have eq₁ : ∥u-v∥^2-2*θ*inner(u-v)(w-v)+θ*θ*∥w-v∥^2=∥u-v∥^2+(θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)), abel, - rw [eq₁, le_add_iff_nonneg_right] at this, - have eq₂ : θ*θ*∥w-v∥^2-2*θ*inner(u-v)(w-v)=θ*(θ*∥w-v∥^2-2*inner(u-v)(w-v)), ring, - rw eq₂ at this, - have := le_of_sub_nonneg (nonneg_of_mul_nonneg_left this hθ₁), - exact this, - by_cases hq : q = 0, - { rw hq at this, - have : p ≤ 0, - have := this (1:ℝ) (by norm_num) (by norm_num), - linarith, - exact this }, - { have q_pos : 0 < q, - apply lt_of_le_of_ne, exact pow_two_nonneg _, intro h, exact hq h.symm, - by_contradiction hp, rw not_le at hp, - let θ := min (1:ℝ) (p / q), - have eq₁ : θ*q ≤ p := calc - θ*q ≤ (p/q) * q : mul_le_mul_of_nonneg_right (min_le_right _ _) (pow_two_nonneg _) - ... = p : div_mul_cancel _ hq, - have : 2 * p ≤ p := calc - 2 * p ≤ θ*q : by { refine this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num) } - ... ≤ p : eq₁, - linarith } -end -begin - assume h, - letI : nonempty K := ⟨⟨v, hv⟩⟩, - apply le_antisymm, - { apply le_cinfi, assume w, - apply nonneg_le_nonneg_of_squares_le (norm_nonneg _), - have := h w w.2, - exact calc - ∥u - v∥ * ∥u - v∥ ≤ ∥u - v∥ * ∥u - v∥ - 2 * inner (u - v) ((w:α) - v) : by linarith - ... ≤ ∥u - v∥^2 - 2 * inner (u - v) ((w:α) - v) + ∥(w:α) - v∥^2 : - by { rw pow_two, refine le_add_of_nonneg_right _, exact pow_two_nonneg _ } - ... = ∥(u - v) - (w - v)∥^2 : norm_sub_pow_two.symm - ... = ∥u - w∥ * ∥u - w∥ : - by { have : (u - v) - (w - v) = u - w, abel, rw [this, pow_two] } }, - { show (⨅ (w : K), ∥u - w∥) ≤ (λw:K, ∥u - w∥) ⟨v, hv⟩, - apply cinfi_le, use 0, rintros y ⟨z, rfl⟩, exact norm_nonneg _ } -end - -/-- -Existence of minimizers. -Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace. -Then there exists a unique `v` in `K` that minimizes the distance `∥u - v∥` to `u`. -This point `v` is usually called the orthogonal projection of `u` onto `K`. --/ -theorem exists_norm_eq_infi_of_complete_subspace (K : subspace ℝ α) - (h : is_complete (↑K : set α)) : ∀ u : α, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (↑K : set α), ∥u - w∥ := -exists_norm_eq_infi_of_complete_convex ⟨0, K.zero_mem⟩ h K.convex - -/-- -Characterization of minimizers in the above theorem. -Let `u` be a point in an inner product space, and let `K` be a nonempty subspace. -Then point `v` minimizes the distance `∥u - v∥` if and only if -for all `w ∈ K`, `inner (u - v) w = 0` (i.e., `u - v` is orthogonal to the subspace `K`) --/ -theorem norm_eq_infi_iff_inner_eq_zero (K : subspace ℝ α) {u : α} {v : α} - (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set α), ∥u - w∥) ↔ ∀ w ∈ K, inner (u - v) w = 0 := -iff.intro -begin - assume h, - have h : ∀ w ∈ K, inner (u - v) (w - v) ≤ 0, - { rwa [norm_eq_infi_iff_inner_le_zero] at h, exacts [K.convex, hv] }, - assume w hw, - have le : inner (u - v) w ≤ 0, - let w' := w + v, - have : w' ∈ K := submodule.add_mem _ hw hv, - have h₁ := h w' this, - have h₂ : w' - v = w, simp only [add_neg_cancel_right, sub_eq_add_neg], - rw h₂ at h₁, exact h₁, - have ge : inner (u - v) w ≥ 0, - let w'' := -w + v, - have : w'' ∈ K := submodule.add_mem _ (submodule.neg_mem _ hw) hv, - have h₁ := h w'' this, - have h₂ : w'' - v = -w, simp only [neg_inj, add_neg_cancel_right, sub_eq_add_neg], - rw [h₂, inner_neg_right] at h₁, - linarith, - exact le_antisymm le ge -end -begin - assume h, - have : ∀ w ∈ K, inner (u - v) (w - v) ≤ 0, - assume w hw, - let w' := w - v, - have : w' ∈ K := submodule.sub_mem _ hw hv, - have h₁ := h w' this, - exact le_of_eq h₁, - rwa norm_eq_infi_iff_inner_le_zero, - exacts [submodule.convex _, hv] -end - -/-- The orthogonal projection onto a complete subspace, as an -unbundled function. This definition is only intended for use in -setting up the bundled version `orthogonal_projection` and should not -be used once that is defined. -/ -def orthogonal_projection_fn {K : submodule ℝ α} (h : is_complete (K : set α)) (v : α) := -(exists_norm_eq_infi_of_complete_subspace K h v).some - -/-- The unbundled orthogonal projection is in the given subspace. -This lemma is only intended for use in setting up the bundled version -and should not be used once that is defined. -/ -lemma orthogonal_projection_fn_mem {K : submodule ℝ α} (h : is_complete (K : set α)) (v : α) : - orthogonal_projection_fn h v ∈ K := -(exists_norm_eq_infi_of_complete_subspace K h v).some_spec.some - -/-- The characterization of the unbundled orthogonal projection. This -lemma is only intended for use in setting up the bundled version -and should not be used once that is defined. -/ -lemma orthogonal_projection_fn_inner_eq_zero {K : submodule ℝ α} (h : is_complete (K : set α)) - (v : α) : ∀ w ∈ K, inner (v - orthogonal_projection_fn h v) w = 0 := -begin - rw ←norm_eq_infi_iff_inner_eq_zero K (orthogonal_projection_fn_mem h v), - exact (exists_norm_eq_infi_of_complete_subspace K h v).some_spec.some_spec -end - -/-- The unbundled orthogonal projection is the unique point in `K` -with the orthogonality property. This lemma is only intended for use -in setting up the bundled version and should not be used once that is -defined. -/ -lemma eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero {K : submodule ℝ α} - (h : is_complete (K : set α)) {u v : α} (hvm : v ∈ K) (hvo : ∀ w ∈ K, inner (u - v) w = 0) : - v = orthogonal_projection_fn h u := -begin - rw [←sub_eq_zero, ←inner_self_eq_zero], - have hvs : v - orthogonal_projection_fn h u ∈ K := - submodule.sub_mem K hvm (orthogonal_projection_fn_mem h u), - have huo : inner (u - orthogonal_projection_fn h u) (v - orthogonal_projection_fn h u) = 0 := - orthogonal_projection_fn_inner_eq_zero h u _ hvs, - have huv : inner (u - v) (v - orthogonal_projection_fn h u) = 0 := hvo _ hvs, - have houv : inner ((u - orthogonal_projection_fn h u) - (u - v)) - (v - orthogonal_projection_fn h u) = 0, - { rw [inner_sub_left, huo, huv, sub_zero] }, - rwa sub_sub_sub_cancel_left at houv -end - -/-- The orthogonal projection onto a complete subspace. For most -purposes, `orthogonal_projection`, which removes the `is_complete` -hypothesis and is the identity map when the subspace is not complete, -should be used instead. -/ -def orthogonal_projection_of_complete {K : submodule ℝ α} (h : is_complete (K : set α)) : - linear_map ℝ α α := -{ to_fun := orthogonal_projection_fn h, - map_add' := λ x y, begin - have hm : orthogonal_projection_fn h x + orthogonal_projection_fn h y ∈ K := - submodule.add_mem K (orthogonal_projection_fn_mem h x) (orthogonal_projection_fn_mem h y), - have ho : - ∀ w ∈ K, inner (x + y - (orthogonal_projection_fn h x + orthogonal_projection_fn h y)) w = 0, - { intros w hw, - rw [add_sub_comm, inner_add_left, orthogonal_projection_fn_inner_eq_zero h _ w hw, - orthogonal_projection_fn_inner_eq_zero h _ w hw, add_zero] }, - rw eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hm ho - end, - map_smul' := λ c x, begin - have hm : c • orthogonal_projection_fn h x ∈ K := - submodule.smul_mem K _ (orthogonal_projection_fn_mem h x), - have ho : ∀ w ∈ K, inner (c • x - c • orthogonal_projection_fn h x) w = 0, - { intros w hw, - rw [←smul_sub, inner_smul_left, orthogonal_projection_fn_inner_eq_zero h _ w hw, mul_zero] }, - rw eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hm ho - end } - -/-- The orthogonal projection onto a subspace, which is expected to be -complete. If the subspace is not complete, this uses the identity map -instead. -/ -def orthogonal_projection (K : submodule ℝ α) : linear_map ℝ α α := -if h : is_complete (K : set α) then orthogonal_projection_of_complete h else linear_map.id - -/-- The definition of `orthogonal_projection` using `if`. -/ -lemma orthogonal_projection_def (K : submodule ℝ α) : - orthogonal_projection K = - if h : is_complete (K : set α) then orthogonal_projection_of_complete h else linear_map.id := -rfl - -@[simp] -lemma orthogonal_projection_fn_eq {K : submodule ℝ α} (h : is_complete (K : set α)) (v : α) : - orthogonal_projection_fn h v = orthogonal_projection K v := -by { rw [orthogonal_projection_def, dif_pos h], refl } - -/-- The orthogonal projection is in the given subspace. -/ -lemma orthogonal_projection_mem {K : submodule ℝ α} (h : is_complete (K : set α)) (v : α) : - orthogonal_projection K v ∈ K := -begin - rw ←orthogonal_projection_fn_eq h, - exact orthogonal_projection_fn_mem h v -end - -/-- The characterization of the orthogonal projection. -/ -@[simp] -lemma orthogonal_projection_inner_eq_zero (K : submodule ℝ α) (v : α) : - ∀ w ∈ K, inner (v - orthogonal_projection K v) w = 0 := -begin - simp_rw orthogonal_projection_def, - split_ifs, - { exact orthogonal_projection_fn_inner_eq_zero h v }, - { simp }, -end - -/-- The orthogonal projection is the unique point in `K` with the -orthogonality property. -/ -lemma eq_orthogonal_projection_of_mem_of_inner_eq_zero {K : submodule ℝ α} - (h : is_complete (K : set α)) {u v : α} (hvm : v ∈ K) (hvo : ∀ w ∈ K, inner (u - v) w = 0) : - v = orthogonal_projection K u := -begin - rw ←orthogonal_projection_fn_eq h, - exact eq_orthogonal_projection_fn_of_mem_of_inner_eq_zero h hvm hvo -end - -/-- The subspace of vectors orthogonal to a given subspace. -/ -def submodule.orthogonal (K : submodule ℝ α) : submodule ℝ α := -{ carrier := {v | ∀ u ∈ K, inner u v = 0}, - zero_mem' := λ _ _, inner_zero_right, - add_mem' := λ x y hx hy u hu, by rw [inner_add_right, hx u hu, hy u hu, add_zero], - smul_mem' := λ c x hx u hu, by rw [inner_smul_right, hx u hu, mul_zero] } - -/-- When a vector is in `K.orthogonal`. -/ -lemma submodule.mem_orthogonal (K : submodule ℝ α) (v : α) : - v ∈ K.orthogonal ↔ ∀ u ∈ K, inner u v = 0 := -iff.rfl - -/-- When a vector is in `K.orthogonal`, with the inner product the -other way round. -/ -lemma submodule.mem_orthogonal' (K : submodule ℝ α) (v : α) : - v ∈ K.orthogonal ↔ ∀ u ∈ K, inner v u = 0 := -by simp_rw [submodule.mem_orthogonal, inner_comm] - -/-- A vector in `K` is orthogonal to one in `K.orthogonal`. -/ -lemma submodule.inner_right_of_mem_orthogonal {u v : α} {K : submodule ℝ α} (hu : u ∈ K) - (hv : v ∈ K.orthogonal) : inner u v = 0 := -(K.mem_orthogonal v).1 hv u hu - -/-- A vector in `K.orthogonal` is orthogonal to one in `K`. -/ -lemma submodule.inner_left_of_mem_orthogonal {u v : α} {K : submodule ℝ α} (hu : u ∈ K) - (hv : v ∈ K.orthogonal) : inner v u = 0 := -inner_comm u v ▸ submodule.inner_right_of_mem_orthogonal hu hv - -/-- `K` and `K.orthogonal` have trivial intersection. -/ -lemma submodule.orthogonal_disjoint (K : submodule ℝ α) : disjoint K K.orthogonal := -begin - simp_rw [submodule.disjoint_def, submodule.mem_orthogonal], - exact λ x hx ho, inner_self_eq_zero.1 (ho x hx) -end - -variables (α) - -/-- `submodule.orthogonal` gives a `galois_connection` between -`submodule ℝ α` and its `order_dual`. -/ -lemma submodule.orthogonal_gc : - @galois_connection (submodule ℝ α) (order_dual $ submodule ℝ α) _ _ - submodule.orthogonal submodule.orthogonal := -λ K₁ K₂, ⟨λ h v hv u hu, submodule.inner_left_of_mem_orthogonal hv (h hu), - λ h v hv u hu, submodule.inner_left_of_mem_orthogonal hv (h hu)⟩ - -variables {α} - -/-- `submodule.orthogonal` reverses the `≤` ordering of two -subspaces. -/ -lemma submodule.orthogonal_le {K₁ K₂ : submodule ℝ α} (h : K₁ ≤ K₂) : - K₂.orthogonal ≤ K₁.orthogonal := -(submodule.orthogonal_gc α).monotone_l h - -/-- `K` is contained in `K.orthogonal.orthogonal`. -/ -lemma submodule.le_orthogonal_orthogonal (K : submodule ℝ α) : K ≤ K.orthogonal.orthogonal := -(submodule.orthogonal_gc α).le_u_l _ - -/-- The inf of two orthogonal subspaces equals the subspace orthogonal -to the sup. -/ -lemma submodule.inf_orthogonal (K₁ K₂ : submodule ℝ α) : - K₁.orthogonal ⊓ K₂.orthogonal = (K₁ ⊔ K₂).orthogonal := -(submodule.orthogonal_gc α).l_sup.symm - -/-- The inf of an indexed family of orthogonal subspaces equals the -subspace orthogonal to the sup. -/ -lemma submodule.infi_orthogonal {ι : Type*} (K : ι → submodule ℝ α) : - (⨅ i, (K i).orthogonal) = (supr K).orthogonal := -(submodule.orthogonal_gc α).l_supr.symm - -/-- The inf of a set of orthogonal subspaces equals the subspace -orthogonal to the sup. -/ -lemma submodule.Inf_orthogonal (s : set $ submodule ℝ α) : - (⨅ K ∈ s, submodule.orthogonal K) = (Sup s).orthogonal := -(submodule.orthogonal_gc α).l_Sup.symm - -/-- If `K₁` is complete and contained in `K₂`, `K₁` and `K₁.orthogonal ⊓ K₂` span `K₂`. -/ -lemma submodule.sup_orthogonal_inf_of_is_complete {K₁ K₂ : submodule ℝ α} (h : K₁ ≤ K₂) - (hc : is_complete (K₁ : set α)) : K₁ ⊔ (K₁.orthogonal ⊓ K₂) = K₂ := -begin - ext x, - rw submodule.mem_sup, - rcases exists_norm_eq_infi_of_complete_subspace K₁ hc x with ⟨v, hv, hvm⟩, - rw norm_eq_infi_iff_inner_eq_zero K₁ hv at hvm, - split, - { rintro ⟨y, hy, z, hz, rfl⟩, - exact K₂.add_mem (h hy) hz.2 }, - { exact λ hx, ⟨v, hv, x - v, ⟨(K₁.mem_orthogonal' _).2 hvm, K₂.sub_mem hx (h hv)⟩, - add_sub_cancel'_right _ _⟩ } -end - -/-- If `K` is complete, `K` and `K.orthogonal` span the whole -space. -/ -lemma submodule.sup_orthogonal_of_is_complete {K : submodule ℝ α} (h : is_complete (K : set α)) : - K ⊔ K.orthogonal = ⊤ := -begin - convert submodule.sup_orthogonal_inf_of_is_complete (le_top : K ≤ ⊤) h, - simp -end - -/-- If `K` is complete, `K` and `K.orthogonal` are complements of each -other. -/ -lemma submodule.is_compl_orthogonal_of_is_complete {K : submodule ℝ α} - (h : is_complete (K : set α)) : is_compl K K.orthogonal := -⟨K.orthogonal_disjoint, le_of_eq (submodule.sup_orthogonal_of_is_complete h).symm⟩ - -open finite_dimensional - -/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁` -containined in it, the dimensions of `K₁` and the intersection of its -orthogonal subspace with `K₂` add to that of `K₂`. -/ -lemma submodule.findim_add_inf_findim_orthogonal {K₁ K₂ : submodule ℝ α} - [finite_dimensional ℝ K₂] (h : K₁ ≤ K₂) : - findim ℝ K₁ + findim ℝ (K₁.orthogonal ⊓ K₂ : submodule ℝ α) = findim ℝ K₂ := -begin - haveI := submodule.finite_dimensional_of_le h, - have hd := submodule.dim_sup_add_dim_inf_eq K₁ (K₁.orthogonal ⊓ K₂), - rw [←inf_assoc, (submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, findim_bot, - submodule.sup_orthogonal_inf_of_is_complete h - (submodule.complete_of_finite_dimensional _)] at hd, - rw add_zero at hd, - exact hd.symm -end - -end orthogonal diff --git a/src/data/complex/is_R_or_C.lean b/src/data/complex/is_R_or_C.lean index 9d16ad754a52d..a759eb58f3319 100644 --- a/src/data/complex/is_R_or_C.lean +++ b/src/data/complex/is_R_or_C.lean @@ -24,7 +24,7 @@ immediately from the two instances of the class. /-- This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ. -/ -class is_R_or_C (K : Type*) [nondiscrete_normed_field K] [algebra ℝ K] := +class is_R_or_C (K : Type*) extends nondiscrete_normed_field K, normed_algebra ℝ K, complete_space K := (re : K →+ ℝ) (im : K →+ ℝ) (conj : K →+* K) @@ -48,8 +48,9 @@ class is_R_or_C (K : Type*) [nondiscrete_normed_field K] [algebra ℝ K] := namespace is_R_or_C -variables {K : Type*} [nondiscrete_normed_field K] [algebra ℝ K] [is_R_or_C K] -local notation `𝓚` := @is_R_or_C.of_real K _ _ _ +variables {K : Type*} [is_R_or_C K] +local notation `𝓚` := @is_R_or_C.of_real K _ +local postfix `†`:100 := @is_R_or_C.conj K _ lemma of_real_alg : ∀ x : ℝ, 𝓚 x = x • (1 : K) := λ x, by rw [←mul_one (𝓚 x), smul_coe_mul_ax] @@ -62,6 +63,8 @@ is_R_or_C.mul_re_ax @[simp] lemma mul_im : ∀ z w : K, im (z * w) = re z * im w + im z * re w := is_R_or_C.mul_im_ax +lemma inv_def {z : K} : z⁻¹ = conj z * of_real ((∥z∥^2)⁻¹) := is_R_or_C.inv_def_ax z + theorem ext_iff : ∀ {z w : K}, z = w ↔ re z = re w ∧ im z = im w := λ z w, { mp := by { rintro rfl, cc }, mpr := by { rintro ⟨h₁,h₂⟩, rw [←re_add_im z, ←re_add_im w, h₁, h₂] } } @@ -70,10 +73,14 @@ theorem ext : ∀ {z w : K}, re z = re w → im z = im w → z = w := by { simp_rw ext_iff, cc } -lemma zero_re : re (𝓚 0) = (0 : ℝ) := by simp only [of_real_re] +@[simp] lemma zero_re : re (𝓚 0) = (0 : ℝ) := by simp only [of_real_re] @[simp] lemma zero_im : im (𝓚 0) = 0 := by rw [of_real_im] lemma of_real_zero : 𝓚 0 = 0 := by rw [of_real_alg, zero_smul] +@[simp] lemma zero_re' : re (0 : K) = (0 : ℝ) := +by simp only [add_monoid_hom.map_zero] + + @[simp] lemma of_real_one : 𝓚 1 = 1 := by rw [of_real_alg, one_smul] @[simp] lemma one_re : re (1 : K) = 1 := by rw [←of_real_one, of_real_re] @[simp] lemma one_im : im (1 : K) = 0 := by rw [←of_real_one, of_real_im] @@ -93,8 +100,8 @@ by simp only [bit1, add_right_eq_self, add_monoid_hom.map_add, bit0_im, one_im] @[simp] theorem of_real_eq_zero {z : ℝ} : 𝓚 z = 0 ↔ z = 0 := by rw [←of_real_zero]; exact of_real_inj -@[simp] lemma of_real_add (r s : ℝ) : 𝓚 (r + s) = 𝓚 r + 𝓚 s := -by apply (@is_R_or_C.ext_iff K _ _ _ (𝓚 (r + s)) (𝓚 r + 𝓚 s)).mpr; simp +@[simp] lemma of_real_add ⦃r s : ℝ⦄ : 𝓚 (r + s) = 𝓚 r + 𝓚 s := +by apply (@is_R_or_C.ext_iff K _ (𝓚 (r + s)) (𝓚 r + 𝓚 s)).mpr; simp @[simp] lemma of_real_bit0 (r : ℝ) : 𝓚 (bit0 r : ℝ) = bit0 (𝓚 r) := ext_iff.2 $ by simp [bit0] @@ -109,8 +116,10 @@ begin linarith, end -@[simp] lemma of_real_neg (r : ℝ) : 𝓚 (-r : ℝ) = -(𝓚 r) := ext_iff.2 $ by simp -@[simp] lemma of_real_mul (r s : ℝ) : 𝓚 (r * s : ℝ) = (𝓚 r) * (𝓚 s) := ext_iff.2 $ by simp +@[simp] lemma of_real_neg (r : ℝ) : 𝓚 (-r) = -(𝓚 r) := ext_iff.2 $ by simp +@[simp] lemma of_real_mul (r s : ℝ) : 𝓚 (r * s) = (𝓚 r) * (𝓚 s) := ext_iff.2 $ by simp +lemma of_real_mul_re (r : ℝ) (z : K) : re ((𝓚 r) * z) = r * re z := +by simp only [mul_re, of_real_im, zero_mul, of_real_re, sub_zero] lemma smul_re (r : ℝ) (z : K) : re ((𝓚 r) * z) = r * (re z) := by simp only [of_real_im, zero_mul, of_real_re, sub_zero, mul_re] @@ -127,6 +136,9 @@ lemma smul_im' : ∀ (r : ℝ) (z : K), im (r • z) = r * (im z) := /-- The imaginary unit. -/ @[simp] lemma I_re : re (I : K) = 0 := I_re_ax @[simp] lemma I_im (z : K) : im z * im (I : K) = im z := mul_im_I_ax z +@[simp] lemma I_im' (z : K) : im (I : K) * im z = im z := +by rw [mul_comm, I_im _] + lemma I_mul_I : (I : K) = 0 ∨ (I : K) * I = -1 := I_mul_I_ax @[simp] lemma conj_re (z : K) : re (conj z) = re z := is_R_or_C.conj_re_ax z @@ -148,7 +160,7 @@ lemma conj_bijective : @function.bijective K K is_R_or_C.conj := conj_involutive lemma conj_inj (z w : K) : conj z = conj w ↔ z = w := conj_bijective.1.eq_iff @[simp] lemma conj_eq_zero {z : K} : conj z = 0 ↔ z = 0 := -by simpa using @conj_inj K _ _ _ z 0 +by simpa using @conj_inj K _ z 0 lemma eq_conj_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (𝓚 r) := begin @@ -166,6 +178,16 @@ begin { rintros ⟨r, rfl⟩, apply conj_of_real } end +/-- Conjugation as a ring equivalence. This is used to convert the inner product into a +sesquilinear product. -/ +def conj_to_ring_equiv : K ≃+* Kᵒᵖ := +{ to_fun := opposite.op ∘ conj, + inv_fun := conj ∘ opposite.unop, + left_inv := λ x, by simp only [conj_conj, function.comp_app, opposite.unop_op], + right_inv := λ x, by simp only [conj_conj, opposite.op_unop, function.comp_app], + map_mul' := λ x y, by simp [mul_comm], + map_add' := λ x y, by simp } + lemma eq_conj_iff_re {z : K} : conj z = z ↔ 𝓚 (re z) = z := eq_conj_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩ @@ -228,9 +250,15 @@ lemma norm_sq_sub (z w : K) : norm_sq (z - w) = norm_sq z + norm_sq w - 2 * re (z * conj w) := by simp [-mul_re, norm_sq_add, add_comm, add_left_comm, sub_eq_add_neg] -/-! ### Inversion -/ +lemma sqrt_norm_sq_eq_norm {z : K} : real.sqrt (norm_sq z) = ∥z∥ := +begin + have h₁ : (norm_sq z) = ∥z∥^2 := by rw [norm_sq_eq_def, norm_sq], + have h₂ : ∥z∥ = real.sqrt (∥z∥^2) := eq_comm.mp (real.sqrt_sqr (norm_nonneg z)), + rw [h₂], + exact congr_arg real.sqrt h₁ +end -lemma inv_def {z : K} : z⁻¹ = conj z * of_real ((∥z∥^2)⁻¹) := inv_def_ax z +/-! ### Inversion -/ @[simp] lemma inv_re (z : K) : re (z⁻¹) = re z / norm_sq z := by simp [inv_def, norm_sq_eq_def, norm_sq, division_def] @@ -256,10 +284,19 @@ lemma div_im (z w : K) : im (z / w) = im z * re w / norm_sq w - re z * im w / no by simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm] @[simp] lemma of_real_div (r s : ℝ) : 𝓚 (r / s : ℝ) = 𝓚 r / 𝓚 s := -(@is_R_or_C.of_real_hom K _ _ _).map_div r s +(@is_R_or_C.of_real_hom K _).map_div r s + +lemma div_re_of_real {z : K} {r : ℝ} : re (z / (𝓚 r)) = re z / r := +begin + by_cases h : r = 0, + { simp [h, of_real_zero] }, + { change r ≠ 0 at h, + rw [div_eq_mul_inv, ←of_real_inv, div_eq_mul_inv], + simp [norm_sq, norm_sq_of_real, div_mul_eq_div_mul_one_div, div_self h] } +end @[simp] lemma of_real_fpow (r : ℝ) (n : ℤ) : 𝓚 (r ^ n) = (𝓚 r) ^ n := -(@is_R_or_C.of_real_hom K _ _ _).map_fpow r n +(@is_R_or_C.of_real_hom K _).map_fpow r n lemma I_mul_I_of_nonzero : (I : K) ≠ 0 → (I : K) * I = -1 := by { have := I_mul_I_ax, tauto } @@ -285,6 +322,15 @@ end @[simp] lemma norm_sq_div (z w : K) : norm_sq (z / w) = norm_sq z / norm_sq w := by { rw [division_def, norm_sq_mul, norm_sq_inv], refl } +lemma norm_conj {z : K} : ∥conj z∥ = ∥z∥ := +by simp only [←sqrt_norm_sq_eq_norm, norm_sq_conj] + +lemma conj_inv {z : K} : conj (z⁻¹) = (conj z)⁻¹ := +by simp only [inv_def, norm_conj, ring_hom.map_mul, conj_of_real] + +lemma conj_div {z w : K} : conj (z / w) = (conj z) / (conj w) := +by rw [div_eq_inv_mul, div_eq_inv_mul, ring_hom.map_mul]; simp only [conj_inv] + /-! ### Cast lemmas -/ @[simp] theorem of_real_nat_cast (n : ℕ) : 𝓚 (n : ℝ) = n := @@ -306,7 +352,7 @@ by rw [← of_real_int_cast, of_real_re] by rw [← of_real_int_cast, of_real_im] @[simp] theorem of_real_rat_cast (n : ℚ) : 𝓚 (n : ℝ) = n := -(@is_R_or_C.of_real_hom K _ _ _).map_rat_cast n +(@is_R_or_C.of_real_hom K _).map_rat_cast n @[simp] lemma rat_cast_re (q : ℚ) : re (q : K) = q := by rw [← of_real_rat_cast, of_real_re] @@ -335,7 +381,7 @@ by rw [add_conj]; simp; rw [mul_div_cancel_left (𝓚 (re z)) two_ne_zero] @[pp_nodot] noncomputable def abs (z : K) : ℝ := (norm_sq z).sqrt local notation `abs'` := _root_.abs -local notation `absK` := @abs K _ _ _ +local notation `absK` := @abs K _ @[simp] lemma abs_of_real (r : ℝ) : absK (𝓚 r) = abs' r := by simp [abs, norm_sq, norm_sq_of_real, real.sqrt_mul_self_eq_abs] @@ -437,6 +483,21 @@ by rw [← of_real_nat_cast, abs_of_nonneg (nat.cast_nonneg n)] lemma norm_sq_eq_abs (x : K) : norm_sq x = abs x ^ 2 := by rw [abs, pow_two, real.mul_self_sqrt (norm_sq_nonneg _)] +lemma re_eq_abs_of_mul_conj (x : K) : re (x * (conj x)) = abs (x * (conj x)) := +by rw [mul_conj, of_real_re, abs_of_real, norm_sq_eq_abs, pow_two, _root_.abs_mul, abs_abs] + +lemma abs_sqr_re_add_conj (x : K) : (abs (x + x†))^2 = (re (x + x†))^2 := +by simp [pow_two, ←norm_sq_eq_abs, norm_sq] + +lemma abs_sqr_re_add_conj' (x : K) : (abs (x† + x))^2 = (re (x† + x))^2 := +by simp [pow_two, ←norm_sq_eq_abs, norm_sq] + +lemma conj_mul_eq_norm_sq_left (x : K) : x† * x = 𝓚 (norm_sq x) := +begin + rw ext_iff, + refine ⟨by simp [of_real_re, mul_re, conj_re, conj_im, norm_sq],_⟩, + simp [of_real_im, mul_im, conj_im, conj_re, mul_comm], +end /-! ### Cauchy sequences -/ @@ -528,21 +589,21 @@ namespace is_R_or_C section cleanup_lemmas -local notation `reR` := @is_R_or_C.re ℝ _ _ _ -local notation `imR` := @is_R_or_C.im ℝ _ _ _ -local notation `conjR` := @is_R_or_C.conj ℝ _ _ _ -local notation `IR` := @is_R_or_C.I ℝ _ _ _ -local notation `of_realR` := @is_R_or_C.of_real ℝ _ _ _ -local notation `absR` := @is_R_or_C.abs ℝ _ _ _ -local notation `norm_sqR` := @is_R_or_C.norm_sq ℝ _ _ _ - -local notation `reC` := @is_R_or_C.re ℂ _ _ _ -local notation `imC` := @is_R_or_C.im ℂ _ _ _ -local notation `conjC` := @is_R_or_C.conj ℂ _ _ _ -local notation `IC` := @is_R_or_C.I ℂ _ _ _ -local notation `of_realC` := @is_R_or_C.of_real ℂ _ _ _ -local notation `absC` := @is_R_or_C.abs ℂ _ _ _ -local notation `norm_sqC` := @is_R_or_C.norm_sq ℂ _ _ _ +local notation `reR` := @is_R_or_C.re ℝ _ +local notation `imR` := @is_R_or_C.im ℝ _ +local notation `conjR` := @is_R_or_C.conj ℝ _ +local notation `IR` := @is_R_or_C.I ℝ _ +local notation `of_realR` := @is_R_or_C.of_real ℝ _ +local notation `absR` := @is_R_or_C.abs ℝ _ +local notation `norm_sqR` := @is_R_or_C.norm_sq ℝ _ + +local notation `reC` := @is_R_or_C.re ℂ _ +local notation `imC` := @is_R_or_C.im ℂ _ +local notation `conjC` := @is_R_or_C.conj ℂ _ +local notation `IC` := @is_R_or_C.I ℂ _ +local notation `of_realC` := @is_R_or_C.of_real ℂ _ +local notation `absC` := @is_R_or_C.abs ℂ _ +local notation `norm_sqC` := @is_R_or_C.norm_sq ℂ _ @[simp] lemma re_to_real {x : ℝ} : reR x = x := rfl @[simp] lemma im_to_real {x : ℝ} : imR x = 0 := rfl diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean index df653d98ba4c2..f53f6cc5e0ed8 100644 --- a/src/geometry/euclidean/basic.lean +++ b/src/geometry/euclidean/basic.lean @@ -3,7 +3,8 @@ Copyright (c) 2020 Joseph Myers. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Joseph Myers. -/ -import analysis.normed_space.real_inner_product +import analysis.normed_space.inner_product +import algebra.quadratic_discriminant import analysis.normed_space.add_torsor import data.matrix.notation import linear_algebra.affine_space.combination @@ -13,6 +14,7 @@ noncomputable theory open_locale big_operators open_locale classical open_locale real +open_locale real_inner_product_space /-! # Euclidean spaces @@ -21,7 +23,7 @@ This file makes some definitions and proves very basic geometrical results about real inner product spaces and Euclidean affine spaces. Results about real inner product spaces that involve the norm and inner product but not angles generally go in -`analysis.normed_space.real_inner_product`. Results with longer +`analysis.normed_space.inner_product`. Results with longer proofs or more geometrical content generally go in separate files. ## Main definitions @@ -41,7 +43,7 @@ proofs or more geometrical content generally go in separate files. ## Implementation notes To declare `P` as the type of points in a Euclidean affine space with -`V` as the type of vectors, use `[inner_product_space V] [metric_space P] +`V` as the type of vectors, use `[inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]`. This works better with `out_param` to make `V` implicit in most cases than having a separate type alias for Euclidean affine spaces. @@ -66,7 +68,7 @@ conveniently be developed in terms of vectors and then used to deduce corresponding results for Euclidean affine spaces. -/ -variables {V : Type*} [inner_product_space V] +variables {V : Type*} [inner_product_space ℝ V] /-- The undirected angle between two vectors. If either vector is 0, this is π/2. -/ @@ -74,14 +76,14 @@ def angle (x y : V) : ℝ := real.arccos (inner x y / (∥x∥ * ∥y∥)) /-- The cosine of the angle between two vectors. -/ lemma cos_angle (x y : V) : real.cos (angle x y) = inner x y / (∥x∥ * ∥y∥) := -real.cos_arccos (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).1 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).2 +real.cos_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2 /-- The angle between two vectors does not depend on their order. -/ lemma angle_comm (x y : V) : angle x y = angle y x := begin unfold angle, - rw [inner_comm, mul_comm] + rw [real_inner_comm, mul_comm] end /-- The angle between the negation of two vectors. -/ @@ -128,7 +130,7 @@ end @[simp] lemma angle_self {x : V} (hx : x ≠ 0) : angle x x = 0 := begin unfold angle, - rw [←inner_self_eq_norm_square, div_self (λ h, hx (inner_self_eq_zero.1 h)), + rw [←real_inner_self_eq_norm_square, div_self (λ h, hx (inner_self_eq_zero.1 h)), real.arccos_one] end @@ -187,12 +189,12 @@ lemma sin_angle_mul_norm_mul_norm (x y : V) : real.sin (angle x y) * (∥x∥ * real.sqrt (inner x x * inner y y - inner x y * inner x y) := begin unfold angle, - rw [real.sin_arccos (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).1 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).2, + rw [real.sin_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2, ←real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)), ←real.sqrt_mul' _ (mul_self_nonneg _), pow_two, - real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)), inner_self_eq_norm_square, - inner_self_eq_norm_square], + real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)), real_inner_self_eq_norm_square, + real_inner_self_eq_norm_square], by_cases h : (∥x∥ * ∥y∥) = 0, { rw [(show ∥x∥ * ∥x∥ * (∥y∥ * ∥y∥) = (∥x∥ * ∥y∥) * (∥x∥ * ∥y∥), by ring), h, mul_zero, mul_zero, zero_sub], @@ -210,11 +212,11 @@ nonzero and one is a positive multiple of the other. -/ lemma angle_eq_zero_iff (x y : V) : angle x y = 0 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x) := begin unfold angle, - rw [←inner_div_norm_mul_norm_eq_one_iff, ←real.arccos_one], + rw [←real_inner_div_norm_mul_norm_eq_one_iff, ←real.arccos_one], split, { intro h, - exact real.arccos_inj (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).1 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).2 + exact real.arccos_inj (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2 (by norm_num) (by norm_num) h }, @@ -227,11 +229,11 @@ and one is a negative multiple of the other. -/ lemma angle_eq_pi_iff (x y : V) : angle x y = π ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r < 0 ∧ y = r • x) := begin unfold angle, - rw [←inner_div_norm_mul_norm_eq_neg_one_iff, ←real.arccos_neg_one], + rw [←real_inner_div_norm_mul_norm_eq_neg_one_iff, ←real.arccos_neg_one], split, { intro h, - exact real.arccos_inj (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).1 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).2 + exact real.arccos_inj (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2 (by norm_num) (by norm_num) h }, @@ -252,7 +254,7 @@ end /-- Two vectors have inner product 0 if and only if the angle between them is π/2. -/ -lemma inner_eq_zero_iff_angle_eq_pi_div_two (x y : V) : inner x y = 0 ↔ angle x y = π / 2 := +lemma inner_eq_zero_iff_angle_eq_pi_div_two (x y : V) : ⟪x, y⟫ = 0 ↔ angle x y = π / 2 := begin split, { intro h, @@ -262,8 +264,8 @@ begin unfold angle at h, rw ←real.arccos_zero at h, have h2 : inner x y / (∥x∥ * ∥y∥) = 0 := - real.arccos_inj (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).1 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x y)).2 + real.arccos_inj (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2 (by norm_num) (by norm_num) h, @@ -287,8 +289,9 @@ Euclidean affine spaces. -/ open inner_product_geometry -variables {V : Type*} {P : Type*} [inner_product_space V] [metric_space P] +variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] +local notation `⟪`x`, `y`⟫` := @inner ℝ V _ x y include V /-- The undirected angle at `p2` between the line segments to `p1` and @@ -412,16 +415,16 @@ applies to `c₂`. Then the vector between `c₁` and `c₂` is orthogonal to that between `p₁` and `p₂`. (In two dimensions, this says that the diagonals of a kite are orthogonal.) -/ lemma inner_vsub_vsub_of_dist_eq_of_dist_eq {c₁ c₂ p₁ p₂ : P} (hc₁ : dist p₁ c₁ = dist p₂ c₁) - (hc₂ : dist p₁ c₂ = dist p₂ c₂) : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0 := + (hc₂ : dist p₁ c₂ = dist p₂ c₂) : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 := begin - have h : inner ((c₂ -ᵥ c₁) + (c₂ -ᵥ c₁)) (p₂ -ᵥ p₁) = 0, + have h : ⟪(c₂ -ᵥ c₁) + (c₂ -ᵥ c₁), p₂ -ᵥ p₁⟫ = 0, { conv_lhs { congr, congr, rw ←vsub_sub_vsub_cancel_right c₂ c₁ p₁, skip, rw ←vsub_sub_vsub_cancel_right c₂ c₁ p₂ }, rw [←add_sub_comm, inner_sub_left], conv_lhs { congr, rw ←vsub_sub_vsub_cancel_right p₂ p₁ c₂, skip, rw ←vsub_sub_vsub_cancel_right p₂ p₁ c₁ }, rw [dist_comm p₁, dist_comm p₂, dist_eq_norm_vsub V _ p₁, - dist_eq_norm_vsub V _ p₂, ←inner_add_sub_eq_zero_iff] at hc₁ hc₂, + dist_eq_norm_vsub V _ p₂, ←real_inner_add_sub_eq_zero_iff] at hc₁ hc₂, simp_rw [←neg_vsub_eq_vsub_rev c₁, ←neg_vsub_eq_vsub_rev c₂, sub_neg_eq_add, neg_add_eq_sub, hc₁, hc₂, sub_zero] }, simpa [inner_add_left, ←mul_two, (by norm_num : (2 : ℝ) ≠ 0)] using h @@ -432,23 +435,23 @@ multiple of a fixed vector added to a point) and another point, expressed as a quadratic. -/ lemma dist_smul_vadd_square (r : ℝ) (v : V) (p₁ p₂ : P) : dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ = - inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂) := + ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ := begin - rw [dist_eq_norm_vsub V _ p₂, ←inner_self_eq_norm_square, vadd_vsub_assoc, inner_add_add_self, - inner_smul_left, inner_smul_left, inner_smul_right], + rw [dist_eq_norm_vsub V _ p₂, ←real_inner_self_eq_norm_square, vadd_vsub_assoc, real_inner_add_add_self, + real_inner_smul_left, real_inner_smul_left, real_inner_smul_right], ring end /-- The condition for two points on a line to be equidistant from another point. -/ lemma dist_smul_vadd_eq_dist {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) : - dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ (r = 0 ∨ r = -2 * inner v (p₁ -ᵥ p₂) / inner v v) := + dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ (r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫) := begin conv_lhs { rw [←mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_square, ←sub_eq_zero_iff_eq, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, - ←inner_self_eq_norm_square, sub_self] }, - have hvi : inner v v ≠ 0, by simpa using hv, - have hd : discrim (inner v v) (2 * inner v (p₁ -ᵥ p₂)) 0 = + ←real_inner_self_eq_norm_square, sub_self] }, + have hvi : ⟪v, v⟫ ≠ 0, by simpa using hv, + have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = (2 * inner v (p₁ -ᵥ p₂)) * (2 * inner v (p₁ -ᵥ p₂)), { rw discrim, ring }, rw [quadratic_eq_zero_iff hvi hd, add_left_neg, zero_div, neg_mul_eq_neg_mul, @@ -469,7 +472,7 @@ lemma eq_of_dist_eq_of_dist_eq_of_mem_of_findim_eq_two {s : affine_subspace ℝ (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂) (hp₂c₂ : dist p₂ c₂ = r₂) (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂ := begin - have ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0 := + have ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 := inner_vsub_vsub_of_dist_eq_of_dist_eq (by cc) (by cc), let b : fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁], have hb : linear_independent ℝ b, @@ -479,7 +482,7 @@ begin { intros i j hij, fin_cases i; fin_cases j; try { exact false.elim (hij rfl) }, { exact ho }, - { rw inner_comm, exact ho } } }, + { rw real_inner_comm, exact ho } } }, have hbs : submodule.span ℝ (set.range b) = s.direction, { refine eq_of_le_of_findim_eq _ _, { rw [submodule.span_le, set.range_subset_iff], @@ -501,7 +504,7 @@ begin rcases hv' with ⟨t₂, rfl⟩, exact ⟨t₁, t₂, hv⟩ }, rcases hv (p -ᵥ p₁) (vsub_mem_direction hps hp₁s) with ⟨t₁, t₂, hpt⟩, - have hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0 := + have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 := inner_vsub_vsub_of_dist_eq_of_dist_eq (by cc) (by cc), simp only [hpt, inner_add_right, inner_smul_right, ho, mul_zero, add_zero, mul_eq_zero, inner_self_eq_zero, vsub_eq_zero_iff_eq, hc.symm, or_false] at hop, @@ -543,7 +546,7 @@ def orthogonal_projection_fn {s : affine_subspace ℝ P} (hn : (s : set P).nonem classical.some $ inter_eq_singleton_of_nonempty_of_is_compl hn (mk'_nonempty p s.direction.orthogonal) - ((direction_mk' p s.direction.orthogonal).symm ▸ submodule.is_compl_orthogonal_of_is_complete hc) + ((direction_mk' p s.direction.orthogonal).symm ▸ submodule.is_compl_orthogonal_of_is_complete_real hc) /-- The intersection of the subspace and the orthogonal subspace through the given point is the `orthogonal_projection_fn` of that @@ -556,7 +559,7 @@ lemma inter_eq_singleton_orthogonal_projection_fn {s : affine_subspace ℝ P} classical.some_spec $ inter_eq_singleton_of_nonempty_of_is_compl hn (mk'_nonempty p s.direction.orthogonal) - ((direction_mk' p s.direction.orthogonal).symm ▸ submodule.is_compl_orthogonal_of_is_complete hc) + ((direction_mk' p s.direction.orthogonal).symm ▸ submodule.is_compl_orthogonal_of_is_complete_real hc) /-- The `orthogonal_projection_fn` lies in the given subspace. This lemma is only intended for use in setting up the bundled version and @@ -794,7 +797,7 @@ lemma dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_proje begin rw [metric_space.dist_comm p2 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V _ p2, ← vsub_add_vsub_cancel p1 (orthogonal_projection s p2) p2, - norm_add_square_eq_norm_square_add_norm_square_iff_inner_eq_zero], + norm_add_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero], rw orthogonal_projection_def, split_ifs, { rw orthogonal_projection_of_nonempty_of_complete_eq, @@ -817,7 +820,7 @@ calc dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 : by { rw [dist_eq_norm_vsub V (r1 • v +ᵥ p1), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul], abel } ... = ∥p1 -ᵥ p2∥ * ∥p1 -ᵥ p2∥ + ∥(r1 - r2) • v∥ * ∥(r1 - r2) • v∥ - : norm_add_square_eq_norm_square_add_norm_square + : norm_add_square_eq_norm_square_add_norm_square_real (submodule.inner_right_of_mem_orthogonal (vsub_mem_direction hp1 hp2) (submodule.smul_mem _ _ hv)) ... = ∥(p1 -ᵥ p2 : V)∥ * ∥(p1 -ᵥ p2 : V)∥ + abs (r1 - r2) * abs (r1 - r2) * ∥v∥ * ∥v∥ @@ -847,30 +850,29 @@ def reflection (s : affine_subspace ℝ P) : P ≃ᵢ P := ((orthogonal_projection s p₁ -ᵥ p₁) +ᵥ orthogonal_projection s p₁), dist_eq_norm_vsub V p₁, ←inner_self_eq_norm_square, ←inner_self_eq_norm_square], by_cases h : (s : set P).nonempty ∧ is_complete (s.direction : set V), - { calc inner + { calc + ⟪(orthogonal_projection s p₁ -ᵥ p₁ +ᵥ orthogonal_projection s p₁ -ᵥ + (orthogonal_projection s p₂ -ᵥ p₂ +ᵥ orthogonal_projection s p₂)), (orthogonal_projection s p₁ -ᵥ p₁ +ᵥ orthogonal_projection s p₁ -ᵥ - (orthogonal_projection s p₂ -ᵥ p₂ +ᵥ orthogonal_projection s p₂)) - (orthogonal_projection s p₁ -ᵥ p₁ +ᵥ orthogonal_projection s p₁ -ᵥ - (orthogonal_projection s p₂ -ᵥ p₂ +ᵥ orthogonal_projection s p₂)) - = inner - ((_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂)) + + (orthogonal_projection s p₂ -ᵥ p₂ +ᵥ orthogonal_projection s p₂))⟫ + = ⟪(_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂)) + _root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) - - (p₁ -ᵥ p₂)) - (_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) + + (p₁ -ᵥ p₂), + _root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) + _root_.orthogonal_projection s.direction (p₁ -ᵥ p₂) - - (p₁ -ᵥ p₂)) + (p₁ -ᵥ p₂)⟫ : by rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc, ←vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub, ←add_sub_assoc, ←affine_map.linear_map_vsub, orthogonal_projection_linear h.1] ... = -4 * inner (p₁ -ᵥ p₂ - (_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂))) (_root_.orthogonal_projection s.direction (p₁ -ᵥ p₂)) + - inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂) + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ : by { simp [inner_sub_left, inner_sub_right, inner_add_left, inner_add_right, - inner_comm (p₁ -ᵥ p₂)], + real_inner_comm (p₁ -ᵥ p₂)], ring } - ... = -4 * 0 + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂) + ... = -4 * 0 + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ : by rw orthogonal_projection_inner_eq_zero s.direction _ _ (_root_.orthogonal_projection_mem h.2 _) - ... = inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂) : by simp }, + ... = ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ : by simp }, { simp [orthogonal_projection_def, h] } end } diff --git a/src/geometry/euclidean/circumcenter.lean b/src/geometry/euclidean/circumcenter.lean index a56354f92eb91..0ef2aa17c6f42 100644 --- a/src/geometry/euclidean/circumcenter.lean +++ b/src/geometry/euclidean/circumcenter.lean @@ -11,6 +11,7 @@ noncomputable theory open_locale big_operators open_locale classical open_locale real +open_locale real_inner_product_space /-! # Circumcenter and circumradius @@ -36,7 +37,7 @@ namespace euclidean_geometry open inner_product_geometry -variables {V : Type*} {P : Type*} [inner_product_space V] [metric_space P] +variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] include V @@ -265,7 +266,7 @@ namespace simplex open finset affine_subspace euclidean_geometry -variables {V : Type*} {P : Type*} [inner_product_space V] [metric_space P] +variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] include V @@ -662,7 +663,7 @@ namespace euclidean_geometry open affine affine_subspace finite_dimensional -variables {V : Type*} {P : Type*} [inner_product_space V] [metric_space P] +variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] include V @@ -841,14 +842,13 @@ begin dist_square_eq_dist_orthogonal_projection_square_add_dist_orthogonal_projection_square p₂ h], simp [h₂', dist_comm p₂] }, rw [←hd₂, hp₁, hp₂, dist_eq_norm_vsub V _ s.circumcenter, - dist_eq_norm_vsub V _ s.circumcenter, vadd_vsub, vadd_vsub, ←inner_self_eq_norm_square, - ←inner_self_eq_norm_square, inner_smul_left, inner_smul_left, inner_smul_right, - inner_smul_right, ←mul_assoc, ←mul_assoc] at hd₁, + dist_eq_norm_vsub V _ s.circumcenter, vadd_vsub, vadd_vsub, ←real_inner_self_eq_norm_square, + ←real_inner_self_eq_norm_square, real_inner_smul_left, real_inner_smul_left, real_inner_smul_right, + real_inner_smul_right, ←mul_assoc, ←mul_assoc] at hd₁, by_cases hp : p = orthogonal_projection span_s p, { rw [hp₁, hp₂, ←hp], simp }, - { have hz : inner (p -ᵥ orthogonal_projection span_s p) - (p -ᵥ orthogonal_projection span_s p) ≠ 0, + { have hz : ⟪p -ᵥ orthogonal_projection span_s p, p -ᵥ orthogonal_projection span_s p⟫ ≠ 0, { simpa using hp }, rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁, rw [hp₁, hp₂], diff --git a/src/geometry/euclidean/monge_point.lean b/src/geometry/euclidean/monge_point.lean index 82c6767443884..f08c3ce60e0a3 100644 --- a/src/geometry/euclidean/monge_point.lean +++ b/src/geometry/euclidean/monge_point.lean @@ -9,6 +9,7 @@ noncomputable theory open_locale big_operators open_locale classical open_locale real +open_locale real_inner_product_space /-! # Monge point and orthocenter @@ -51,7 +52,7 @@ namespace simplex open finset affine_subspace euclidean_geometry points_with_circumcenter_index -variables {V : Type*} {P : Type*} [inner_product_space V] [metric_space P] +variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] include V @@ -206,8 +207,8 @@ n-dimensional face, is orthogonal to the difference of the two vertices not in that face. -/ lemma inner_monge_point_vsub_face_centroid_vsub {n : ℕ} (s : simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) : - inner (s.monge_point -ᵥ ({i₁, i₂}ᶜ : finset (fin (n + 3))).centroid ℝ s.points) - (s.points i₁ -ᵥ s.points i₂) = 0 := + ⟪s.monge_point -ᵥ ({i₁, i₂}ᶜ : finset (fin (n + 3))).centroid ℝ s.points, + s.points i₁ -ᵥ s.points i₂⟫ = 0 := begin simp_rw [monge_point_vsub_face_centroid_eq_weighted_vsub_of_points_with_circumcenter s h, point_eq_affine_combination_of_points_with_circumcenter, @@ -437,9 +438,8 @@ namespace triangle open euclidean_geometry finset simplex affine_subspace finite_dimensional -variables {V : Type*} {P : Type*} [inner_product_space V] [metric_space P] +variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] - include V /-- The orthocenter of a triangle is the intersection of its diff --git a/src/geometry/euclidean/triangle.lean b/src/geometry/euclidean/triangle.lean index 206f9f51dc9d7..97964d71482ec 100644 --- a/src/geometry/euclidean/triangle.lean +++ b/src/geometry/euclidean/triangle.lean @@ -10,6 +10,7 @@ noncomputable theory open_locale big_operators open_locale classical open_locale real +open_locale real_inner_product_space /-! # Triangles @@ -48,13 +49,13 @@ most conveniently be developed in terms of vectors and then used to deduce corresponding results for Euclidean affine spaces. -/ -variables {V : Type*} [inner_product_space V] +variables {V : Type*} [inner_product_space ℝ V] /-- Pythagorean theorem, if-and-only-if vector angle form. -/ lemma norm_add_square_eq_norm_square_add_norm_square_iff_angle_eq_pi_div_two (x y : V) : ∥x + y∥ * ∥x + y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ angle x y = π / 2 := begin - rw norm_add_square_eq_norm_square_add_norm_square_iff_inner_eq_zero, + rw norm_add_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero, exact inner_eq_zero_iff_angle_eq_pi_div_two x y end @@ -67,7 +68,7 @@ lemma norm_add_square_eq_norm_square_add_norm_square' (x y : V) (h : angle x y = lemma norm_sub_square_eq_norm_square_add_norm_square_iff_angle_eq_pi_div_two (x y : V) : ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ ↔ angle x y = π / 2 := begin - rw norm_sub_square_eq_norm_square_add_norm_square_iff_inner_eq_zero, + rw norm_sub_square_eq_norm_square_add_norm_square_iff_real_inner_eq_zero, exact inner_eq_zero_iff_angle_eq_pi_div_two x y end @@ -82,8 +83,8 @@ lemma norm_sub_square_eq_norm_square_add_norm_square_sub_two_mul_norm_mul_norm_m ∥x - y∥ * ∥x - y∥ = ∥x∥ * ∥x∥ + ∥y∥ * ∥y∥ - 2 * ∥x∥ * ∥y∥ * real.cos (angle x y) := by rw [(show 2 * ∥x∥ * ∥y∥ * real.cos (angle x y) = 2 * (real.cos (angle x y) * (∥x∥ * ∥y∥)), by ring), - cos_angle_mul_norm_mul_norm, ←inner_self_eq_norm_square, - ←inner_self_eq_norm_square, ←inner_self_eq_norm_square, inner_sub_sub_self, + cos_angle_mul_norm_mul_norm, ←real_inner_self_eq_norm_square, + ←real_inner_self_eq_norm_square, ←real_inner_self_eq_norm_square, real_inner_sub_sub_self, sub_add_eq_add_sub] /-- Pons asinorum, vector angle form. -/ @@ -95,8 +96,8 @@ begin (angle_nonneg _ _) (angle_le_pi _ _) _, rw [cos_angle, cos_angle, h, ←neg_sub, norm_neg, neg_sub, - inner_sub_right, inner_sub_right, inner_self_eq_norm_square, inner_self_eq_norm_square, h, - inner_comm x y] + inner_sub_right, inner_sub_right, real_inner_self_eq_norm_square, real_inner_self_eq_norm_square, h, + real_inner_comm x y] end /-- Converse of pons asinorum, vector angle form. -/ @@ -104,10 +105,10 @@ lemma norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi {x y : V} (h : angle x (x - y) = angle y (y - x)) (hpi : angle x y ≠ π) : ∥x∥ = ∥y∥ := begin replace h := real.arccos_inj - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x (x - y))).1 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one x (x - y))).2 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one y (y - x))).1 - (abs_le.mp (abs_inner_div_norm_mul_norm_le_one y (y - x))).2 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x (x - y))).1 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x (x - y))).2 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one y (y - x))).1 + (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one y (y - x))).2 h, by_cases hxy : x = y, { rw hxy }, @@ -115,8 +116,8 @@ begin mul_inv_rev', mul_inv_rev', ←mul_assoc, ←mul_assoc] at h, replace h := mul_right_cancel' (inv_ne_zero (λ hz, hxy (eq_of_sub_eq_zero (norm_eq_zero.1 hz)))) h, - rw [inner_sub_right, inner_sub_right, inner_comm y x, inner_self_eq_norm_square, - inner_self_eq_norm_square, mul_sub_right_distrib, mul_sub_right_distrib, + rw [inner_sub_right, inner_sub_right, real_inner_comm x y, real_inner_self_eq_norm_square, + real_inner_self_eq_norm_square, mul_sub_right_distrib, mul_sub_right_distrib, mul_self_mul_inv, mul_self_mul_inv, sub_eq_sub_iff_sub_eq_sub, ←mul_sub_left_distrib] at h, by_cases hx0 : x = 0, @@ -130,7 +131,7 @@ begin symmetry, by_contradiction hyx, replace h := (mul_left_cancel' (sub_ne_zero_of_ne hyx) h).symm, - rw [inner_div_norm_mul_norm_eq_neg_one_iff, ←angle_eq_pi_iff] at h, + rw [real_inner_div_norm_mul_norm_eq_neg_one_iff, ←angle_eq_pi_iff] at h, exact hpi h } } } end @@ -154,19 +155,19 @@ begin ∥x∥ * ∥y∥ * ∥x - y∥ * ∥x - y∥ = (real.sin (angle x (x - y)) * (∥x∥ * ∥x - y∥)) * (real.sin (angle y (y - x)) * (∥y∥ * ∥x - y∥)), { ring }, - have H2 : inner x x * (inner x x - inner x y - (inner x y - inner y y)) - + have H2 : ⟪x, x⟫ * (inner x x - inner x y - (inner x y - inner y y)) - (inner x x - inner x y) * (inner x x - inner x y) = inner x x * inner y y - inner x y * inner x y, { ring }, - have H3 : inner y y * (inner y y - inner x y - (inner x y - inner x x)) - + have H3 : ⟪y, y⟫ * (inner y y - inner x y - (inner x y - inner x x)) - (inner y y - inner x y) * (inner y y - inner x y) = inner x x * inner y y - inner x y * inner x y, { ring }, rw [mul_sub_right_distrib, mul_sub_right_distrib, mul_sub_right_distrib, mul_sub_right_distrib, H1, sin_angle_mul_norm_mul_norm, norm_sub_rev x y, sin_angle_mul_norm_mul_norm, norm_sub_rev y x, inner_sub_left, inner_sub_left, - inner_sub_right, inner_sub_right, inner_sub_right, inner_sub_right, inner_comm y x, H2, - H3, real.mul_self_sqrt (sub_nonneg_of_le (inner_mul_inner_self_le x y)), - inner_self_eq_norm_square, inner_self_eq_norm_square, - inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two], + inner_sub_right, inner_sub_right, inner_sub_right, inner_sub_right, real_inner_comm x y, H2, + H3, real.mul_self_sqrt (sub_nonneg_of_le (real_inner_mul_inner_self_le x y)), + real_inner_self_eq_norm_square, real_inner_self_eq_norm_square, + real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two], field_simp [hxn, hyn, hxyn], ring } end @@ -187,25 +188,25 @@ begin apply mul_right_cancel' hyn, apply mul_right_cancel' hxyn, apply mul_right_cancel' hxyn, - have H1 : real.sin (angle x (x - y)) * (inner y (y - x) / (∥y∥ * ∥y - x∥)) * ∥x∥ * ∥y∥ * ∥x - y∥ = + have H1 : real.sin (angle x (x - y)) * (⟪y, y - x⟫ / (∥y∥ * ∥y - x∥)) * ∥x∥ * ∥y∥ * ∥x - y∥ = real.sin (angle x (x - y)) * (∥x∥ * ∥x - y∥) * - (inner y (y - x) / (∥y∥ * ∥y - x∥)) * ∥y∥, { ring }, - have H2 : inner x (x - y) / (∥x∥ * ∥y - x∥) * real.sin (angle y (y - x)) * ∥x∥ * ∥y∥ * ∥y - x∥ = - inner x (x - y) / (∥x∥ * ∥y - x∥) * + (⟪y, y - x⟫ / (∥y∥ * ∥y - x∥)) * ∥y∥, { ring }, + have H2 : ⟪x, x - y⟫ / (∥x∥ * ∥y - x∥) * real.sin (angle y (y - x)) * ∥x∥ * ∥y∥ * ∥y - x∥ = + ⟪x, x - y⟫ / (∥x∥ * ∥y - x∥) * (real.sin (angle y (y - x)) * (∥y∥ * ∥y - x∥)) * ∥x∥, { ring }, - have H3 : inner x x * (inner x x - inner x y - (inner x y - inner y y)) - - (inner x x - inner x y) * (inner x x - inner x y) = - inner x x * inner y y - inner x y * inner x y, { ring }, - have H4 : inner y y * (inner y y - inner x y - (inner x y - inner x x)) - - (inner y y - inner x y) * (inner y y - inner x y) = - inner x x * inner y y - inner x y * inner x y, { ring }, + have H3 : ⟪x, x⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - + (⟪x, x⟫ - ⟪x, y⟫) * (⟪x, x⟫ - ⟪x, y⟫) = + ⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫, { ring }, + have H4 : ⟪y, y⟫ * (⟪y, y⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪x, x⟫)) - + (⟪y, y⟫ - ⟪x, y⟫) * (⟪y, y⟫ - ⟪x, y⟫) = + ⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫, { ring }, rw [right_distrib, right_distrib, right_distrib, right_distrib, H1, sin_angle_mul_norm_mul_norm, norm_sub_rev x y, H2, sin_angle_mul_norm_mul_norm, norm_sub_rev y x, mul_assoc (real.sin (angle x y)), sin_angle_mul_norm_mul_norm, inner_sub_left, inner_sub_left, inner_sub_right, inner_sub_right, inner_sub_right, - inner_sub_right, inner_comm y x, H3, H4, inner_self_eq_norm_square, - inner_self_eq_norm_square, - inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two], + inner_sub_right, real_inner_comm x y, H3, H4, real_inner_self_eq_norm_square, + real_inner_self_eq_norm_square, + real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two], field_simp [hxn, hyn, hxyn], ring } end @@ -292,7 +293,7 @@ open inner_product_geometry open_locale euclidean_geometry -variables {V : Type*} {P : Type*} [inner_product_space V] [metric_space P] +variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] include V diff --git a/src/geometry/manifold/instances/real.lean b/src/geometry/manifold/instances/real.lean index 40610d6f437f6..6b68fbfc673c4 100644 --- a/src/geometry/manifold/instances/real.lean +++ b/src/geometry/manifold/instances/real.lean @@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel -/ import geometry.manifold.algebra.smooth_functions import linear_algebra.finite_dimensional -import analysis.normed_space.real_inner_product +import analysis.normed_space.inner_product /-! # Constructing examples of manifolds over ℝ @@ -15,18 +15,18 @@ or with boundary or with corners. As a concrete example, we construct explicitly boundary structure on the real interval `[x, y]`. More specifically, we introduce -* `model_with_corners ℝ (euclidean_space (fin n)) (euclidean_half_space n)` for the model space used +* `model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_half_space n)` for the model space used to define `n`-dimensional real manifolds with boundary -* `model_with_corners ℝ (euclidean_space (fin n)) (euclidean_quadrant n)` for the model space used +* `model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_quadrant n)` for the model space used to define `n`-dimensional real manifolds with corners ## Notations In the locale `manifold`, we introduce the notations -* `𝓡 n` for the identity model with corners on `euclidean_space (fin n)` -* `𝓡∂ n` for `model_with_corners ℝ (euclidean_space (fin n)) (euclidean_half_space n)`. +* `𝓡 n` for the identity model with corners on `euclidean_space ℝ (fin n)` +* `𝓡∂ n` for `model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_half_space n)`. -For instance, if a manifold `M` is boundaryless, smooth and modelled on `euclidean_space (fin m)`, +For instance, if a manifold `M` is boundaryless, smooth and modelled on `euclidean_space ℝ (fin m)`, and `N` is smooth with boundary modelled on `euclidean_half_space n`, and `f : M → N` is a smooth map, then the derivative of `f` can be written simply as `mfderiv (𝓡 m) (𝓡∂ n) f` (as to why the model with corners can not be implicit, see the discussion in `smooth_manifold_with_corners.lean`). @@ -46,13 +46,13 @@ The half-space in `ℝ^n`, used to model manifolds with boundary. We only define `1 ≤ n`, as the definition only makes sense in this case. -/ def euclidean_half_space (n : ℕ) [has_zero (fin n)] : Type := -{x : euclidean_space (fin n) // 0 ≤ x 0} +{x : euclidean_space ℝ (fin n) // 0 ≤ x 0} /-- The quadrant in `ℝ^n`, used to model manifolds with corners, made of all vectors with nonnegative coordinates. -/ -def euclidean_quadrant (n : ℕ) : Type := {x : euclidean_space (fin n) // ∀i:fin n, 0 ≤ x i} +def euclidean_quadrant (n : ℕ) : Type := {x : euclidean_space ℝ (fin n) // ∀i:fin n, 0 ≤ x i} section /- Register class instances for euclidean half-space and quadrant, that can not be noticed @@ -76,11 +76,11 @@ by simp end /-- -Definition of the model with corners `(euclidean_space (fin n), euclidean_half_space n)`, used as a +Definition of the model with corners `(euclidean_space ℝ (fin n), euclidean_half_space n)`, used as a model for manifolds with boundary. In the locale `manifold`, use the shortcut `𝓡∂ n`. -/ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] : - model_with_corners ℝ (euclidean_space (fin n)) (euclidean_half_space n) := + model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_half_space n) := { to_fun := λx, x.val, inv_fun := λx, ⟨λi, if h : i = 0 then max (x i) 0 else x i, by simp [le_refl]⟩, source := univ, @@ -107,10 +107,10 @@ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] : `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/ rw range_half_space, apply unique_diff_on_convex, - show convex {y : euclidean_space (fin n) | 0 ≤ y 0}, + show convex {y : euclidean_space ℝ (fin n) | 0 ≤ y 0}, { assume x y hx hy a b ha hb hab, simpa only [add_zero] using add_le_add (mul_nonneg ha hx) (mul_nonneg hb hy) }, - show (interior {y : euclidean_space (fin n) | 0 ≤ y 0}).nonempty, + show (interior {y : euclidean_space ℝ (fin n) | 0 ≤ y 0}).nonempty, { use (λi, 1), rw mem_interior, refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _, @@ -137,10 +137,10 @@ def model_with_corners_euclidean_half_space (n : ℕ) [has_zero (fin n)] : end } /-- -Definition of the model with corners `(euclidean_space (fin n), euclidean_quadrant n)`, used as a +Definition of the model with corners `(euclidean_space ℝ (fin n), euclidean_quadrant n)`, used as a model for manifolds with corners -/ def model_with_corners_euclidean_quadrant (n : ℕ) : - model_with_corners ℝ (euclidean_space (fin n)) (euclidean_quadrant n) := + model_with_corners ℝ (euclidean_space ℝ (fin n)) (euclidean_quadrant n) := { to_fun := λx, x.val, inv_fun := λx, ⟨λi, max (x i) 0, λi, by simp only [le_refl, or_true, le_max_iff]⟩, source := univ, @@ -163,10 +163,10 @@ def model_with_corners_euclidean_quadrant (n : ℕ) : `unique_diff_on_convex`: it suffices to check that it is convex and with nonempty interior. -/ rw range_quadrant, apply unique_diff_on_convex, - show convex {y : euclidean_space (fin n) | ∀ (i : fin n), 0 ≤ y i}, + show convex {y : euclidean_space ℝ (fin n) | ∀ (i : fin n), 0 ≤ y i}, { assume x y hx hy a b ha hb hab i, simpa only [add_zero] using add_le_add (mul_nonneg ha (hx i)) (mul_nonneg hb (hy i)) }, - show (interior {y : euclidean_space (fin n) | ∀ (i : fin n), 0 ≤ y i}).nonempty, + show (interior {y : euclidean_space ℝ (fin n) | ∀ (i : fin n), 0 ≤ y i}).nonempty, { use (λi, 1), rw mem_interior, refine ⟨(pi (univ : set (fin n)) (λi, (Ioi 0 : set ℝ))), _, @@ -187,7 +187,7 @@ def model_with_corners_euclidean_quadrant (n : ℕ) : exact this.comp (continuous_apply i) end } -localized "notation `𝓡 `n := model_with_corners_self ℝ (euclidean_space (fin n))" in manifold +localized "notation `𝓡 `n := model_with_corners_self ℝ (euclidean_space ℝ (fin n))" in manifold localized "notation `𝓡∂ `n := model_with_corners_euclidean_half_space n" in manifold /-- @@ -224,7 +224,7 @@ def Icc_left_chart (x y : ℝ) [fact (x < y)] : end, open_target := begin have : is_open {z : ℝ | z < y - x} := is_open_Iio, - have : is_open {z : euclidean_space (fin 1) | z 0 < y - x} := + have : is_open {z : euclidean_space ℝ (fin 1) | z 0 < y - x} := @continuous_apply (fin 1) (λ _, ℝ) _ 0 _ this, exact continuous_subtype_val _ this end, @@ -240,7 +240,7 @@ def Icc_left_chart (x y : ℝ) [fact (x < y)] : apply continuous_subtype_mk, have A : continuous (λ z : ℝ, min (z + x) y) := (continuous_id.add continuous_const).min continuous_const, - have B : continuous (λz : euclidean_space (fin 1), z 0) := continuous_apply 0, + have B : continuous (λz : euclidean_space ℝ (fin 1), z 0) := continuous_apply 0, exact (A.comp B).comp continuous_subtype_val end } @@ -279,7 +279,7 @@ def Icc_right_chart (x y : ℝ) [fact (x < y)] : end, open_target := begin have : is_open {z : ℝ | z < y - x} := is_open_Iio, - have : is_open {z : euclidean_space (fin 1) | z 0 < y - x} := + have : is_open {z : euclidean_space ℝ (fin 1) | z 0 < y - x} := @continuous_apply (fin 1) (λ _, ℝ) _ 0 _ this, exact continuous_subtype_val _ this end, @@ -295,7 +295,7 @@ def Icc_right_chart (x y : ℝ) [fact (x < y)] : apply continuous_subtype_mk, have A : continuous (λ z : ℝ, max (y - z) x) := (continuous_const.sub continuous_id).max continuous_const, - have B : continuous (λz : euclidean_space (fin 1), z 0) := continuous_apply 0, + have B : continuous (λz : euclidean_space ℝ (fin 1), z 0) := continuous_apply 0, exact (A.comp B).comp continuous_subtype_val end } @@ -321,7 +321,7 @@ The manifold structure on `[x, y]` is smooth. instance Icc_smooth_manifold (x y : ℝ) [fact (x < y)] : smooth_manifold_with_corners (𝓡∂ 1) (Icc x y) := begin - have M : times_cont_diff_on ℝ ∞ (λz : euclidean_space (fin 1), - z + (λi, y - x)) univ, + have M : times_cont_diff_on ℝ ∞ (λz : euclidean_space ℝ (fin 1), - z + (λi, y - x)) univ, { rw times_cont_diff_on_univ, exact times_cont_diff_id.neg.add times_cont_diff_const }, apply smooth_manifold_with_corners_of_times_cont_diff_on, diff --git a/src/linear_algebra/sesquilinear_form.lean b/src/linear_algebra/sesquilinear_form.lean index 424d7d21623dc..e889d05091b0a 100644 --- a/src/linear_algebra/sesquilinear_form.lean +++ b/src/linear_algebra/sesquilinear_form.lean @@ -31,6 +31,8 @@ refer to the function field, ie. `S x y = S.sesq x y`. Sesquilinear form, -/ +open_locale big_operators + universes u v /-- A sesquilinear form over a module -/ @@ -113,6 +115,22 @@ S x y = 0 lemma ortho_zero (x : M) : is_ortho S (0 : M) x := zero_left x +lemma is_add_monoid_hom_left (S : sesq_form R M I) (x : M) : is_add_monoid_hom (λ z, S z x) := +{ map_add := λ z y, sesq_add_left S _ _ _, + map_zero := zero_left x } + +lemma is_add_monoid_hom_right (S : sesq_form R M I) (x : M) : is_add_monoid_hom (λ z, S x z) := +{ map_add := λ z y, sesq_add_right S _ _ _, + map_zero := zero_right x } + +lemma map_sum_left {α : Type*} (S : sesq_form R M I) (t : finset α) (g : α → M) (w : M) : + S (∑ i in t, g i) w = ∑ i in t, S (g i) w := +by haveI s_inst := is_add_monoid_hom_left S w; exact (finset.sum_hom t (λ z, S z w)).symm + +lemma map_sum_right {α : Type*} (S : sesq_form R M I) (t : finset α) (g : α → M) (w : M) : + S w (∑ i in t, g i) = ∑ i in t, S w (g i) := +by haveI s_inst := is_add_monoid_hom_right S w; exact (finset.sum_hom t (λ z, S w z)).symm + end general_ring section comm_ring diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean index a48d3f401264e..1de94ff55246f 100644 --- a/src/ring_theory/algebra.lean +++ b/src/ring_theory/algebra.lean @@ -1511,16 +1511,6 @@ instance (R : Type*) (S : Type*) (E : Type*) [I : add_comm_group E] : end module -variables (𝕜 : Type*) [field 𝕜] (𝕜' : Type*) [field 𝕜'] [algebra 𝕜 𝕜'] -variables (W : Type*) [add_comm_group W] [vector_space 𝕜' W] - -/-- -`V.restrict_scalars 𝕜` is the `𝕜`-subspace of the `𝕜`-vector space given by restriction of scalars, -corresponding to `V`, a `𝕜'`-subspace of the original `𝕜'`-vector space. --/ -def subspace.restrict_scalars (V : subspace 𝕜' W) : subspace 𝕜 (semimodule.restrict_scalars 𝕜 𝕜' W) := -{ ..submodule.restrict_scalars 𝕜 (V : submodule 𝕜' W) } - end restrict_scalars section extend_scalars