What is docs#euclidean.dist?

Stream: general

[Eric Wieser]

Is this true?

import analysis.inner_product_space.euclidean_dist

example : euclidean.dist (0 : ℝ × ℝ) (3, 4) = 5 :=
sorry

My impression is that's it's not necessarily even provable

[Floris van Doorn]

There is no condition that docs#to_euclidean is length-preserving, in general it isn't. In particular euclidean.dist (0 : ℝ) 1 can be any positive real number.

[Eric Wieser]

Should this really be a def and not an existential?

[Floris van Doorn]

I thought I wanted more information, but you should probably just avoid using it on inner product spaces. And use e.g. docs#cont_diff_bump_of_inner instead of docs#cont_diff_bump

[Eric Wieser]

I guess my complaint is that the name suggests that this is going to give some useful euclidean distance, not just a proof that you could have one

[Yaël Dillies]

In particular, people wanted to use it for euclidean geometry.

[Floris van Doorn]

It does something else: define some euclidean distance on finite-dimensional normed vector spaces.
If you want to do euclidean geometry, just use dist.

[Yaël Dillies]

Yes of course. My point is that this is a wrongly tentative name.

[Floris van Doorn]

I'm fine with a rename (pinging @Yury G. Kudryashov)

[Eric Wieser]

Here's the "proof" that it's unprovable:

import analysis.inner_product_space.euclidean_dist

example : euclidean.dist (0 : ℝ × ℝ) (3, 4) = 5 :=
begin
  have : ((3 : ℝ)^(2 : ℝ) + (4 : ℝ)^(2 : ℝ)) ^ (1/2 : ℝ) = 5,
  { rw [real.rpow_two, real.rpow_two],
    have : (0 : ℝ) ≤ 3 ^ 2 + 4 ^ 2 := by norm_num,
    apply real.rpow_left_inj_on (two_ne_zero) (real.rpow_nonneg_of_nonneg this _),
    { norm_num },
    { dsimp only,
      rw [←real.rpow_mul this, div_mul_cancel (1 : ℝ) (two_ne_zero), real.rpow_one],
      norm_num } },
  dunfold euclidean.dist,
  dsimp only [to_euclidean, continuous_linear_equiv.of_finrank_eq,
    linear_equiv.coe_to_continuous_linear_equiv', finite_dimensional.linear_equiv.of_finrank_eq,
    pi_Lp.dist],
  simp_rw [←this, map_zero, pi.zero_apply, dist_zero_left, real.norm_eq_abs,
    real.rpow_two, sq_abs, ←real.rpow_two],
  congr' 1,
  have hd : finite_dimensional.finrank ℝ (ℝ × ℝ) = 2 :=
    (module.free.finrank_prod _ _ _).trans (by simp),
  rw [←(fin.cast hd.symm).to_equiv.sum_comp, fin.sum_univ_succ, fin.sum_univ_succ,
    fin.sum_univ_zero, add_zero, fin.succ_zero_eq_one],
  dsimp,

  -- ⇑(classical.choice _) (3, 4) (⇑(fin.cast _) 0) ^ 2
  --   + ⇑(classical.choice _) (3, 4) (⇑(fin.cast _) 1) ^ 2 = 3 ^ 2 + 4 ^ 2
  sorry,

end

[Chris Hughes]

Just a comment in the docstring explaining that it doesn't necessarily preserve the dist on spaces that are already euclidean would be useful.

[Yury G. Kudryashov]

Feel free to rename the namespace as you wish.