Zulip Chat Archive

Stream: maths

Topic: Euclidean challenge


Patrick Massot (Sep 08 2022 at 20:58):

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 (Sep 08 2022 at 20:59):

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

Anatole Dedecker (Sep 08 2022 at 21:48):

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 (Sep 08 2022 at 21:49):

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 (Sep 08 2022 at 21:51):

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

Patrick Massot (Sep 09 2022 at 06:55):

Fantastic, thank you very much!

Anatole Dedecker (Sep 09 2022 at 09:03):

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 (Sep 09 2022 at 13:24):

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 (Sep 09 2022 at 16:14):

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


Last updated: Dec 20 2023 at 11:08 UTC