Euclidean challenge

Stream: maths

[Patrick Massot]

I have a Euclidean geometry challenge:

import analysis.inner_product_space.projection

open_locale real_inner_product_space
open submodule

variables {E : Type*} [inner_product_space ℝ E] [complete_space E]

-- ignore the next line which is fixing a pretty-printer bug
local notation (name := line_printing_only) `Δ` v:55 := submodule.span ℝ {v}
local notation `Δ` v:55 := submodule.span ℝ ({v} : set E)
-- ignore the next line which is fixing a pretty-printer bug
local notation (name := module_span_printing_only) `{.` x `}ᗮ` := (submodule.span ℝ {x})ᗮ
local notation `{.` x `}ᗮ` := (submodule.span ℝ ({x} : set E))ᗮ
local notation `pr[`x`]ᗮ` := orthogonal_projection (submodule.span ℝ {x})ᗮ

lemma foo {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ  ⊔ Δ (pr[v]ᗮ u) = {.v}ᗮ :=
sorry

Note that you can assume E is finite dimensional if this help.

[Patrick Massot]

I think this is true unconditionally but the relevant case is when u and v are non zero and not parallel.

[Anatole Dedecker]

import analysis.inner_product_space.projection

open_locale real_inner_product_space
open submodule

variables {E : Type*} [inner_product_space ℝ E] [complete_space E]

-- ignore the next line which is fixing a pretty-printer bug
local notation (name := line_printing_only) `Δ` v:55 := submodule.span ℝ {v}
local notation `Δ` v:55 := submodule.span ℝ ({v} : set E)
-- ignore the next line which is fixing a pretty-printer bug
local notation (name := module_span_printing_only) `{.` x `}ᗮ` := (submodule.span ℝ {x})ᗮ
local notation `{.` x `}ᗮ` := (submodule.span ℝ ({x} : set E))ᗮ
local notation `pr[`x`]ᗮ` := orthogonal_projection (submodule.span ℝ {x})ᗮ

lemma foobar {U : submodule ℝ E} {x : E} [complete_space (U : set E)] :
  (orthogonal_projection Uᗮ x : E) = x - orthogonal_projection U x :=
by rw [eq_sub_iff_add_eq, add_comm, ← eq_sum_orthogonal_projection_self_orthogonal_complement]

lemma bar {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ = {.pr[v]ᗮ u}ᗮ ⊓ {.v}ᗮ :=
begin
  refine le_antisymm (λ x hx, ⟨_, hx.2⟩) (λ x hx, ⟨_, hx.2⟩);
  refine mem_orthogonal_singleton_of_inner_left _ _,
  { rw [foobar, inner_sub_right, inner_left_of_mem_orthogonal_singleton _ hx.1,
        inner_left_of_mem_orthogonal (coe_mem _) hx.2, sub_zero] },
  { rw [eq_sum_orthogonal_projection_self_orthogonal_complement (Δ v) u,
        inner_add_right, inner_left_of_mem_orthogonal_singleton _ hx.1,
        inner_left_of_mem_orthogonal (coe_mem _) hx.2, zero_add] }
end

lemma foo {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ  ⊔ Δ (pr[v]ᗮ u) = {.v}ᗮ :=
begin
  rw [bar, sup_comm, sup_orthogonal_inf_of_complete_space],
  rw span_singleton_le_iff_mem,
  exact coe_mem _
end

[Anatole Dedecker]

I'm very happy to have found docs#sup_orthogonal_inf_of_complete_space by pure luck here, I would never have thought to look for it

[Anatole Dedecker]

The proof of bar is almost surely suboptimal, but I have to sleep now

[Patrick Massot]

Fantastic, thank you very much!

[Anatole Dedecker]

This is not particularly shorter, but morally this should be the proof of bar:

lemma bar {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ = {.pr[v]ᗮ u}ᗮ ⊓ {.v}ᗮ :=
begin
  rw [inf_orthogonal, inf_orthogonal],
  refine congr_arg _ (le_antisymm (sup_le _ le_sup_right) (sup_le _ le_sup_right));
  rw [span_singleton_le_iff_mem],
  { nth_rewrite 0 eq_sum_orthogonal_projection_self_orthogonal_complement (Δ v) u,
    exact add_mem (mem_sup_right $ coe_mem _) (mem_sup_left $ mem_span_singleton_self _) },
  { rw [foobar],
    refine sub_mem (mem_sup_left $ mem_span_singleton_self _) (mem_sup_right $ coe_mem _) }
end

[Floris van Doorn]

If someone is interested in another challenge, mixed with some calculus:

import analysis.inner_product_space.projection
import analysis.calculus.cont_diff

variables {E : Type*} [inner_product_space ℝ E] {x : E}

lemma cont_diff_subtypeL_comp_orthogonal_projection_span {x₀ : E} (hx₀ : x₀ ≠ 0) :
  cont_diff_at ℝ ⊤ (λ x : E, submodule.subtypeL (ℝ ∙ x) ∘L orthogonal_projection (ℝ ∙ x)) x₀ :=
sorry

Again, finite dimensionality assumptions are fine.

[Floris van Doorn]

Oh, I see that @Heather Macbeth already proved this in the sphere eversion project. Thanks!