[Merged by Bors] - feat(geometry/euclidean/basic): intersections of circles

[jsm28]

Add two versions of the statement that two circles in two-dimensional
space intersect in at most two points, along with some lemmas involved
in the proof (some of which can be interpreted in terms of
intersections of circles or spheres and lines).

---

[eric-wieser]

It would be neat to generalize this to show:

• If it exists, the intersection of two (n-1)-spheres in n dimensions is a n-2 sphere in an n-1 dimensional affine space
• There are at most two points on a 0-sphere

I think the first one can be stated something like

/-- A circular subspace -/
variables (P)
structure circle :=
(c : P)
(r : ℝ)
(direction : submodule ℝ V)
variables {P}

namespace circle

def subspace (c : circle P) : affine_subspace ℝ P := affine_subspace.mk' c.c c.direction

instance : has_mem P (circle P) := ⟨
  λ p c, dist p c.c = c.r ∧ p ∈ c.subspace
⟩

end circle

lemma mem_circle_inter
  {p : P}
  {c₁ c₂ : circle P}
  (hc : c₁.c ≠ c₂.c)
  (hc2 : c₁.subspace = c₂.subspace)
  (hpc₁ : p ∈ c₁)
  (hpc₂ : p ∈ c₂) :
    p ∈ let d := c₂.c -ᵥ c₁.c in 
      circle.mk
        (((inner d d + c₁.r*c₁.r - c₂.r*c₂.r) / inner d d) • d +ᵥ c₁.c)
        sorry -- too lazy to write this right now
        (c₁.direction ⊓ (submodule.span ℝ {d}).orthogonal) :=
begin
  sorry
end

[jsm28]

My inclination is that the most natural version of bundled spheres bundles center, radius and probably radius_pos to require being non-degenerate, but not a direction, so is a sphere in whatever dimension the ambient Euclidean space is, rather than in a subspace. Then you'd define sphere.power, define sphere.radical_subspace and show it contains exactly the points of equal power with respect to both spheres, and deduce that the intersection lies within the radical subspace because points in both spheres have power 0 with respect to both spheres (if the spheres are concentric, the definition of the radical subspace ought to give the empty subspace if the radii are different and the whole space if they are equal, for the above properties to hold). I'm less sure of the use of a version of bundled spheres that bundles a direction as well, versus providing the direction separately when relevant.

Anyway, I think the specific results about intersections of circles are useful in unbundled form in terms of equal distances, not just in a form with bundled spheres; that quite a lot would need to be done to get bundled spheres cleanly to a point where they are helpful for such unbundled results; and that much of the complexity is simply what you get when manipulating things in a particular concrete dimension such as dimension 2 so a proof based on bundled spheres wouldn't actually be much simpler.

[PatrickMassot]

I'm sorry about the delay. Start of academic year is always difficult, and this is Covid year...
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests