Signed distance between points

Stream: mathlib4

[Jovan Gerbscheid]

@Joseph Myers, What do you think of a signedDist in the global namespace, for two points p q : P in an affine space and a vector v : V, measuring the distance from p to q in the direction of v?

I think your recently added AffineSubspace.signedDist is the signed version of Metric.infDist, while signedDist would be the signed version of dist. Then AffineSubspace.signedDist could be renamed to AffineSubspace.signedInfDist.

[Jovan Gerbscheid]

This could be used in my formalization of IMO2020Q6.

And I think we also need it for stating results about the power of a point/the (signed) intersecting chords theorem

[Joseph Myers]

I'm not particularly concerned with the precise names, and having some form of signed distance between points (with lemmas linking it to signed distance between a single-point affine subspace and a point) makes sense. Note that AffineSubspace.signedDist is a bundled affine map. I think the one between points with a vector for the direction could be bundled affine in both points (that is, a bundled affine map with codomain a type of bundled affine maps).

[Joseph Myers]

The existing material in Mathlib.Geometry.Euclidean.Sphere.Power is indeed rather ad hoc and probably could do with being reworked in terms of an actual definition of power together with signed distance.

[Jovan Gerbscheid]

I noticed signedDist_apply_self uses ‖p -ᵥ orthogonalProjection s p‖ instead of dist p (orthogonalProjection s p), while abs_signedInfDist_eq_dist_of_mem_affineSpan_insert uses dist. Should they both use dist?

[Joseph Myers]

It probably makes sense to be more consistent there (though neither form is likely to be a good simp normal form - that is, dist_eq_norm_vsub wouldn't be a good simp lemma in either direction - since the most convenient form depends on the context).

[Jovan Gerbscheid]

I've made a PR for the renaming (#23646)

[Jovan Gerbscheid]

It would be nice to define signedInfDist in terms of signedDist. However this would require a way to compose signedDist : P →ᵃ[ℝ] P →ᵃ[ℝ] ℝ with AffineMap.id ℝ P : P →ᵃ[ℝ] P and s.subtype.comp (orthogonalProjection s) : P →ᵃ[ℝ] P, that is, create as an affine map the function fun x => signedDist x (orthogonalProjection s x)

[Jovan Gerbscheid]

Does mathlib have some sort of support for SKI combinator calculus to do this? (In this case it is just the S combinator)
edit: nevermind, you can't define the S combinator on general linear maps.

[Jovan Gerbscheid]

In #24245, I've defined signedDist (v : V) : P →ᵃ[ℝ] P →ᵃ[ℝ] ℝ between two points. I then used signedDist to rewrite the definition of signedInfDist.

[Joseph Myers]

I have an alternative redefinition of signedInfDist in #24338 as a bundled continuous affine map (depends on #23732 and #24295 to provide continuous affine map versions of the operations being composed to produce signedInfDist).

[Jovan Gerbscheid]

I propose that we merge the two approaches. That is, use my definition, but then as a bundled continuous affine map (though I haven't tried this yet)

[Jovan Gerbscheid]

But I don't quite get the point of the bunled continuous version. Isn't every affine linear map also continuous? (In a normed space)

[Joseph Myers]

https://en.wikipedia.org/wiki/Discontinuous_linear_map#General_existence_theorem

[Jovan Gerbscheid]

Thanks, that makes sense now. But I am still confused about the notation for the bundled maps and equivalences: P₁ ≃ᵃL[k] P₂ is a continuous affine equivalence, but P₁ →ᴬ[k] P₂ is a continuous affine map? Why don't they use the same letters?

[Joseph Myers]

I don't know the reasons behind notation in specific cases, but in general some irregularities in notation for bundled affine maps of various kinds may arise from bundled algebra maps having got there first with various uses of "a" and "A", and affine maps having to fit in with variants of notation that weren't already in use for algebra maps.

[Jovan Gerbscheid]

Hmm, surely we could at least have the map and equivalence of the same kind use the same letters?

[Jovan Gerbscheid]

I tried to define signedDist as a continuous affine map, but I ran into the lack of a ContinuousAffineMap.id. (you also observed this in #23732)

[Kevin Buzzard]

See #mathlib4 > RFC: notation for continuous maps in algebra @ 💬 for some discussion about my attempt to unify notation here

[Jovan Gerbscheid]

I looked through the current conventions around this, and I concluded that the notation for ContinuousAffineEquiv is a mistake and should be P₁ ≃ᴬ[k] P₂

[Jovan Gerbscheid]

I made a PR for fixing this: #24357

[Jovan Gerbscheid]

I have another question about ContinuousAffineMap and ContinuousAffineEquiv. They are defined as an AffineMap/AffineEquiv where the underlying (affine) function is continuous. Wouldn't it be better to instead require the underlying LinearMap/LinearEquiv to be Continuous? Then the underlying linear map would automatically be (bundled) continuous.

edit: The actual reason I wanted the above is that I want to be able to construct a ContinuousAffineMap by proving that the underlying linear map is continuous instead of proving that the affine map itself is continuous. But this should be possible to do with a constructor. I'll post about it in the AffineSubspace.mk thread since it is related.

[Joseph Myers]

In the common case, the topologies on the spaces of points and vectors are compatible and the affine map is continuous if and only if the linear map is continuous. It's true that some material that's meaningful in that case is only actually present in mathlib for the more restricted normed space case (Mathlib.Analysis.Normed.Affine.ContinuousAffineMap). If someone would like to make such material more general in mathlib, getting #22583 in might be a good start.

In the uncommon case where the topologies aren't compatible, it would seem counterintuitive for ContinuousAffineMap not actually to be continuous.