TITLE: Bell's Theorem - Why does $\lambda$ have a probability?
QUESTION [4 upvotes]: I'm reviewing Bell's theorem. In his proof by contradiction, he assumes the world is deterministic and defines a vector $\lambda$ as the set of all hidden variables which play a role in determining the spin of each entangled electron. He then starts to speak about the "probability density function of $\lambda$", called $\rho (\lambda )$.
But if the world is deterministic, then $\lambda$ is nonprobabilistic; it is a delta function at precisely the values which the hidden variables take. What is the purpose of introducing a density function at all?

REPLY [3 votes]: Bell does not assume that the universe is deterministic. He assumes that it is described by a local hidden variable theory. These are not the same thing.
Bell explains this himself by giving an example of a successful hidden variable theory. To briefly recap his argument: take an ensemble of spin 1/2 particles, each in the state $(| \uparrow \rangle+|\downarrow \rangle)/\sqrt{2}$. A measurement of whether the spin of any given particle will be up or down is random and will never be described by a single-valued hidden variable.
However, this system can be described by a local hidden variable theory, if you allow the hidden variable to be distributed with some probability. Bell does exactly this. Specifically, he shows that for a hidden variable that is distributed with an even probability distribution along the hemisphere (on a Bloch sphere) where $\vec{\lambda} \cdot \vec{p}>0$, $\vec{p}$ being the vector describing the spin state of the particle, there is a theory in which this hidden variable correctly reproduces the probability distribution of measurement results for any measurement axis one could choose. In his paper, Bell then goes on to prove that there is no similar theory for more than one particle.
Now, one could imagine that this probability distribution over $\lambda$ is due to a fundamental randomness as in regular quantum mechanics. One could also suppose that it is due to ignorance about the initial conditions of some deterministic system, like the probability distributions that one makes for the outcomes of a coin flip. Bell's inequality is general enough to cover both cases, as long as this hidden variable is local (in the sense that Bell uses this term). The lack of assumptions about $\lambda$ is one reason that this result is so important.


TITLE: What are all the possible cases among three planes.
QUESTION [0 upvotes]: Can someone help me to understand geometrically the system of equations in $3$ equations and $3$ unknowns in terms of all possible combinations of $\operatorname{Rank}(A)$ and $\operatorname{Rank}(A|B)$ each explained both analytically and geometrically?Most of the books only mention geometrically the cases but do not categorize them in terms of matrix rank.

REPLY [1 votes]: In summary, either

$\operatorname{Rank}(A|b) = \operatorname{Rank}(A)$, in which case
$Ax = b$ has solutions, or
$\operatorname{Rank}(A|b) = \operatorname{Rank}(A) + 1$, in which
case $Ax = b$ has no solution.

If $Ax = b$ has solutions,

If $\operatorname{Rank}(A) = 0$, then $A = 0, b= 0$, and all vectors $x$ are solutions.
If $\operatorname{Rank}(A) = 1$, then the set of all solutions is an affine plane (a plane that need not pass through the origin).
if $\operatorname{Rank}(A) = 2$, then the set of all solutions is an affine line.
if $\operatorname{Rank}(A) = 3$, then the solution is unique (and $\operatorname{Rank}(A|b)$ is necessarily $3$ as well, so it doesn't need checked).

Let $A$ be an $m\times n$ matrix and consider
$$A = \begin{bmatrix}A_1 & A_2 & \ldots & A_n\end{bmatrix}$$
where each $A_i$ is the $i$-th column of $A$, an $m$-dimensional column vector.
If $$x = \begin{bmatrix}x_1\\x_2\\\vdots\\x_n\end{bmatrix}$$
then
$$Ax = A_1x_1 + A_2x_2 + ... + A_nx_n$$
which is a linear combination of the columns $A_1, ..., A_n$. The column space of $A$ is the set of all such linear combinations - which is therefore the space  $\{Ax\mid x \in \Bbb R^n\}$. The Rank of $A$ is just the dimension of that space.
Therefore, when $m=n=3$,

If $\operatorname{Rank}(A) = 0$, then $A$ maps all $\Bbb R^3$ to $0$. I.e., $A = 0$. By the Rank-Nullity theorem, $\operatorname{Null}(A) = 3$.
If $\operatorname{Rank}(A) = 1$, then $A$ maps all $\Bbb R^3$ onto a line passing through $0$. At least one of the $A_i \ne 0$, and the other $A_j = c_jA_i$ for some constant $c_j$. $\operatorname{Null}(A) = 2$.
If $\operatorname{Rank}(A) = 2$, then $A$ maps all $\Bbb R^3$ onto a plane passing through $0$. At least one of the $A_i$ can be expressed as a linear combination of the other two. The other vectors are not multiples of each other. $\operatorname{Null}(A) = 1$.
If $\operatorname{Rank}(A) = 3$, then $A$ maps $\Bbb R^3$ onto all of itself. The three columns $A_i$ are linearly independent. $\operatorname{Null}(0) = 0$.

Note that if $x$ and $x'$ both satisfy $Ax = b$ and $Ax' = b$, then $$A(x - x') = Ax - Ax' = b - b = 0$$
Conversely, if $Ax = b$ and $A(x - x') = 0$, then $Ax' = b$. Therefore, if you know one solution to the equation $Ax = b$, all the other solutions differ from it by a vector from the null space of $A$ (the space of all vectors $v$ with $Av = 0$).
Now look at the augmented matrix $$A|b = \begin{bmatrix}A_1 & A_2 & \ldots & A_n& b\end{bmatrix}$$
As noted above, the rank of this matrix is the dimension of the column space of all linear combinations
$$c_1A_1 + c_2A_2 + ... + c_nA_n + c_0b$$
Adding in $b$ does not change whether any set of the $A_i$ are linearly dependent or not. So the rank of $A|b$ cannot be any less than the rank of $A$ itself. So there are two cases:

$b$ is not linearly independent of the $A_i$. Then $\operatorname{Rank}(A|b) = \operatorname{Rank}(A)$. And there exist scalars $x_i$ such that $$b = x_1A_1 + x_2A_2 + ... +x_nA_n$$. But that means $Ax = b$, where $x = \begin{bmatrix}x_1 & x_2 & ... & x_n\end{bmatrix}^T$. So $Ax = b$ has a solution.
$b$ is linearly independent of the $A_i$, Then $\operatorname{Rank}(A|b) = \operatorname{Rank}(A) + 1$ If $Ax = b$ for some $x$, then $$A_1x_1 + A_2x_2 + ... + A_nx_n - b = 0$$ which would mean $b$ is not linearly dependent.

Addendum:
To relate the planes of each equation to the rank of $A$, we need to look at the row space instead of the column space. The matrix $A$ can also be expressed as
$$A = \begin{bmatrix} {A^1}^T\\{A^2}^T\\{A^3}^T\end{bmatrix}$$ where each $A^i$ is a transposed row of $A$ (where I am indexing by superscripts to distinguish them from the column vectors above). If $b = \begin{bmatrix} b_1 & b_2 & b_3\end{bmatrix}^T$, then the three equations are
$${A^1}^Tx = b_1\\{A^2}^Tx = b_2\\{A^3}^Tx = b_3$$
Now for any non-zero column vector $V$, the equation $V^Tx = c$ is the equation of the unique plane normal to $V$ and passing though the point $c\frac V{\|V\|^2}$
The row space of a $A$ is the space of all possible linear combinations of the $A^i$. The dimension of the row space is always the same as the column space - i.e., it is the rank of $A$. So,

If $\operatorname{Rank}(A) = 0$, then $A = 0$ and there is a solution if and only if $b = 0$, in which case the solution is all of space. (There are no planes in this case, because all three row vectors are $0$ as well.)
If $\operatorname{Rank}(A) = 1$, then the three row vectors span a 1-dimensional space, so they must all be multiples of each other. Since they all point in the same direction, their normal planes are parallel. A solution can only exist if all three planes all pass through the same point, and being parallel, this requires them to be the same plane. This requires that the ratio of $b_i$ to $b_j$ be the same as $A^i$ to $A^j$ for all $i,j$. Since the planes are all the same, that common plane is the set of all solutions.
If $\operatorname{Rank}(A) = 2$, then the normal vectors $A^1, A^2, A^3$ all lie in some plane through the origin. If $N$ is a normal vector to that plane, then ${A^i}^TN = 0$ for all $i$. The three planes ${A^i}^Tx = b_i$ all extend in the direction $N$ (if $x$ is a point on the plane, then so will be $x + tN$ for any $t$). Either any two planes are parallel, or they intersect in a line parallel to $N$. These lines are all parallel, and so never intersect the third plane. This is the prism case you mentioned. Only when the three lines of intersection all turn out to be the same line is there a point that lies on all three planes. I.e., a solution to the equation. In this case, all points on the common line of intersection are solutions.
If $\operatorname{Rank}(A) = 3$, then the three normal vectors are linearly independent. No two planes are parallel, and the line of intersection of those two planes will not be parallel to the third plane, either. Therefore that line of intersection will intersect the third plane in some point $x$. That point $x$ is the unique solution to $Ax = b$.


TITLE: Expected Value of independent random variables with an ${\rm Exp}(\lambda)$ common distribution
QUESTION [0 upvotes]: Question is:

Jack is selling his house, and has decided to accept the first offer exceeding $k$. Assume that successive offers are independent random variables with common distribution $\mathrm{Exp}(\lambda)$.
a) Find the expected number of offers he will reject before he sells the house;
b) Find the expected value of the offer he will accept.

I have solved Part A as :
$p = e^{-\lambda r}$
$P(N=n) = (1-p)^{n-1}p$
$E(N) = \sum_{n=1}^\infty nP(N=n) = p \sum_{n=1}^\infty n(1-p)^{n-1}$
Eventually this will reduce down to $E(N) = \frac {1}{p} = e^{\lambda r}$
This should be correct.
Part B :
I am not sure how we go about finding the value of the actual offer that he will accept. I feel we have to find some conditional expectation but not sure. Any help would be great!

REPLY [1 votes]: The exponential distribution is memoryless: the conditional distribution of $X-k$ given $X>k$ coincides with the distribution of $X$ (you may check this property). That said, $$\mathrm{E}[X\mid X>k] = k + \mathrm{E}[X-k\mid X>k] =  k + \mathrm{E}[X].$$


text:
/-
Copyright (c) 2020 Joseph Myers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Myers, Manuel Candales
-/
import analysis.inner_product_space.projection
import analysis.special_functions.trigonometric.inverse
import algebra.quadratic_discriminant
import linear_algebra.affine_space.finite_dimensional
import analysis.calculus.conformal.normed_space

/-!
# Euclidean spaces

This file makes some definitions and proves very basic geometrical
results about real inner product spaces and Euclidean affine spaces.
Results about real inner product spaces that involve the norm and
inner product but not angles generally go in
`analysis.normed_space.inner_product`.  Results with longer
proofs or more geometrical content generally go in separate files.

## Main definitions

* `inner_product_geometry.angle` is the undirected angle between two
  vectors.

* `euclidean_geometry.angle`, with notation `∠`, is the undirected
  angle determined by three points.

* `euclidean_geometry.orthogonal_projection` is the orthogonal
  projection of a point onto an affine subspace.

* `euclidean_geometry.reflection` is the reflection of a point in an
  affine subspace.

## Implementation notes

To declare `P` as the type of points in a Euclidean affine space with
`V` as the type of vectors, use `[inner_product_space ℝ V] [metric_space P]
[normed_add_torsor V P]`.  This works better with `out_param` to make
`V` implicit in most cases than having a separate type alias for
Euclidean affine spaces.

Rather than requiring Euclidean affine spaces to be finite-dimensional
(as in the definition on Wikipedia), this is specified only for those
theorems that need it.

## References

* https://en.wikipedia.org/wiki/Euclidean_space

-/

noncomputable theory
open_locale big_operators
open_locale classical
open_locale real
open_locale real_inner_product_space

namespace inner_product_geometry
/-!
### Geometrical results on real inner product spaces

This section develops some geometrical definitions and results on real
inner product spaces, where those definitions and results can most
conveniently be developed in terms of vectors and then used to deduce
corresponding results for Euclidean affine spaces.
-/

variables {V : Type*} [inner_product_space ℝ V]

/-- The undirected angle between two vectors. If either vector is 0,
this is π/2. See `orientation.oangle` for the corresponding oriented angle
definition. -/
def angle (x y : V) : ℝ := real.arccos (inner x y / (∥x∥ * ∥y∥))

lemma continuous_at_angle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) :
  continuous_at (λ y : V × V, angle y.1 y.2) x :=
real.continuous_arccos.continuous_at.comp $ continuous_inner.continuous_at.div
  ((continuous_norm.comp continuous_fst).mul (continuous_norm.comp continuous_snd)).continuous_at
  (by simp [hx1, hx2])

lemma angle_smul_smul {c : ℝ} (hc : c ≠ 0) (x y : V) :
  angle (c • x) (c • y) = angle x y :=
have c * c ≠ 0, from mul_ne_zero hc hc,
by rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, real.norm_eq_abs,
  mul_mul_mul_comm _ (∥x∥), abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]

@[simp] lemma _root_.linear_isometry.angle_map {E F : Type*}
  [inner_product_space ℝ E] [inner_product_space ℝ F] (f : E →ₗᵢ[ℝ] F) (u v : E) :
  angle (f u) (f v) = angle u v :=
by rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]

lemma is_conformal_map.preserves_angle {E F : Type*}
  [inner_product_space ℝ E] [inner_product_space ℝ F]
  {f' : E →L[ℝ] F} (h : is_conformal_map f') (u v : E) :
  angle (f' u) (f' v) = angle u v :=
begin
  obtain ⟨c, hc, li, rfl⟩ := h,
  exact (angle_smul_smul hc _ _).trans (li.angle_map _ _)
end

/-- If a real differentiable map `f` is conformal at a point `x`,
    then it preserves the angles at that point. -/
lemma conformal_at.preserves_angle {E F : Type*}
  [inner_product_space ℝ E] [inner_product_space ℝ F]
  {f : E → F} {x : E} {f' : E →L[ℝ] F}
  (h : has_fderiv_at f f' x) (H : conformal_at f x) (u v : E) :
  angle (f' u) (f' v) = angle u v :=
let ⟨f₁, h₁, c⟩ := H in h₁.unique h ▸ is_conformal_map.preserves_angle c u v

/-- The cosine of the angle between two vectors. -/
lemma cos_angle (x y : V) : real.cos (angle x y) = inner x y / (∥x∥ * ∥y∥) :=
real.cos_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1
                (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2

/-- The angle between two vectors does not depend on their order. -/
lemma angle_comm (x y : V) : angle x y = angle y x :=
begin
  unfold angle,
  rw [real_inner_comm, mul_comm]
end

/-- The angle between the negation of two vectors. -/
@[simp] lemma angle_neg_neg (x y : V) : angle (-x) (-y) = angle x y :=
begin
  unfold angle,
  rw [inner_neg_neg, norm_neg, norm_neg]
end

/-- The angle between two vectors is nonnegative. -/
lemma angle_nonneg (x y : V) : 0 ≤ angle x y :=
real.arccos_nonneg _

/-- The angle between two vectors is at most π. -/
lemma angle_le_pi (x y : V) : angle x y ≤ π :=
real.arccos_le_pi _

/-- The angle between a vector and the negation of another vector. -/
lemma angle_neg_right (x y : V) : angle x (-y) = π - angle x y :=
begin
  unfold angle,
  rw [←real.arccos_neg, norm_neg, inner_neg_right, neg_div]
end

/-- The angle between the negation of a vector and another vector. -/
lemma angle_neg_left (x y : V) : angle (-x) y = π - angle x y :=
by rw [←angle_neg_neg, neg_neg, angle_neg_right]

/-- The angle between the zero vector and a vector. -/
@[simp] lemma angle_zero_left (x : V) : angle 0 x = π / 2 :=
begin
  unfold angle,
  rw [inner_zero_left, zero_div, real.arccos_zero]
end

/-- The angle between a vector and the zero vector. -/
@[simp] lemma angle_zero_right (x : V) : angle x 0 = π / 2 :=
begin
  unfold angle,
  rw [inner_zero_right, zero_div, real.arccos_zero]
end

/-- The angle between a nonzero vector and itself. -/
@[simp] lemma angle_self {x : V} (hx : x ≠ 0) : angle x x = 0 :=
begin
  unfold angle,
  rw [←real_inner_self_eq_norm_mul_norm, div_self (λ h, hx (inner_self_eq_zero.1 h)),
      real.arccos_one]
end

/-- The angle between a nonzero vector and its negation. -/
@[simp] lemma angle_self_neg_of_nonzero {x : V} (hx : x ≠ 0) : angle x (-x) = π :=
by rw [angle_neg_right, angle_self hx, sub_zero]

/-- The angle between the negation of a nonzero vector and that
vector. -/
@[simp] lemma angle_neg_self_of_nonzero {x : V} (hx : x ≠ 0) : angle (-x) x = π :=
by rw [angle_comm, angle_self_neg_of_nonzero hx]

/-- The angle between a vector and a positive multiple of a vector. -/
@[simp] lemma angle_smul_right_of_pos (x y : V) {r : ℝ} (hr : 0 < r) :
  angle x (r • y) = angle x y :=
begin
  unfold angle,
  rw [inner_smul_right, norm_smul, real.norm_eq_abs, abs_of_nonneg (le_of_lt hr), ←mul_assoc,
      mul_comm _ r, mul_assoc, mul_div_mul_left _ _ (ne_of_gt hr)]
end

/-- The angle between a positive multiple of a vector and a vector. -/
@[simp] lemma angle_smul_left_of_pos (x y : V) {r : ℝ} (hr : 0 < r) :
  angle (r • x) y = angle x y :=
by rw [angle_comm, angle_smul_right_of_pos y x hr, angle_comm]

/-- The angle between a vector and a negative multiple of a vector. -/
@[simp] lemma angle_smul_right_of_neg (x y : V) {r : ℝ} (hr : r < 0) :
  angle x (r • y) = angle x (-y) :=
by rw [←neg_neg r, neg_smul, angle_neg_right, angle_smul_right_of_pos x y (neg_pos_of_neg hr),
       angle_neg_right]

/-- The angle between a negative multiple of a vector and a vector. -/
@[simp] lemma angle_smul_left_of_neg (x y : V) {r : ℝ} (hr : r < 0) :
  angle (r • x) y = angle (-x) y :=
by rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]

/-- The cosine of the angle between two vectors, multiplied by the
product of their norms. -/
lemma cos_angle_mul_norm_mul_norm (x y : V) : real.cos (angle x y) * (∥x∥ * ∥y∥) = inner x y :=
begin
  rw [cos_angle, div_mul_cancel_of_imp],
  simp [or_imp_distrib] { contextual := tt },
end

/-- The sine of the angle between two vectors, multiplied by the
product of their norms. -/
lemma sin_angle_mul_norm_mul_norm (x y : V) : real.sin (angle x y) * (∥x∥ * ∥y∥) =
    real.sqrt (inner x x * inner y y - inner x y * inner x y) :=
begin
  unfold angle,
  rw [real.sin_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1
                      (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2,
      ←real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)),
      ←real.sqrt_mul' _ (mul_self_nonneg _), sq,
      real.sqrt_mul_self (mul_nonneg (norm_nonneg x) (norm_nonneg y)),
      real_inner_self_eq_norm_mul_norm,
      real_inner_self_eq_norm_mul_norm],
  by_cases h : (∥x∥ * ∥y∥) = 0,
  { rw [(show ∥x∥ * ∥x∥ * (∥y∥ * ∥y∥) = (∥x∥ * ∥y∥) * (∥x∥ * ∥y∥), by ring), h, mul_zero, mul_zero,
        zero_sub],
    cases eq_zero_or_eq_zero_of_mul_eq_zero h with hx hy,
    { rw norm_eq_zero at hx,
      rw [hx, inner_zero_left, zero_mul, neg_zero] },
    { rw norm_eq_zero at hy,
      rw [hy, inner_zero_right, zero_mul, neg_zero] } },
  { field_simp [h], ring_nf }
end

/-- The angle between two vectors is zero if and only if they are
nonzero and one is a positive multiple of the other. -/
lemma angle_eq_zero_iff {x y : V} : angle x y = 0 ↔ (x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x) :=
begin
  rw [angle, ← real_inner_div_norm_mul_norm_eq_one_iff, real.arccos_eq_zero, has_le.le.le_iff_eq,
    eq_comm],
  exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2
end

/-- The angle between two vectors is π if and only if they are nonzero
and one is a negative multiple of the other. -/
lemma angle_eq_pi_iff {x y : V} : angle x y = π ↔ (x ≠ 0 ∧ ∃ (r : ℝ), r < 0 ∧ y = r • x) :=
begin
  rw [angle, ← real_inner_div_norm_mul_norm_eq_neg_one_iff, real.arccos_eq_pi, has_le.le.le_iff_eq],
  exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1
end

/-- If the angle between two vectors is π, the angles between those
vectors and a third vector add to π. -/
lemma angle_add_angle_eq_pi_of_angle_eq_pi {x y : V} (z : V) (h : angle x y = π) :
  angle x z + angle y z = π :=
begin
  rcases angle_eq_pi_iff.1 h with ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩,
  rw [angle_smul_left_of_neg x z hr, angle_neg_left, add_sub_cancel'_right]
end

/-- Two vectors have inner product 0 if and only if the angle between
them is π/2. -/
lemma inner_eq_zero_iff_angle_eq_pi_div_two (x y : V) : ⟪x, y⟫ = 0 ↔ angle x y = π / 2 :=
iff.symm $ by simp [angle, or_imp_distrib] { contextual := tt }

/-- If the angle between two vectors is π, the inner product equals the negative product
of the norms. -/
lemma inner_eq_neg_mul_norm_of_angle_eq_pi {x y : V} (h : angle x y = π) : ⟪x, y⟫ = - (∥x∥ * ∥y∥) :=
by simp [← cos_angle_mul_norm_mul_norm, h]

/-- If the angle between two vectors is 0, the inner product equals the product of the norms. -/
lemma inner_eq_mul_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) : ⟪x, y⟫ = ∥x∥ * ∥y∥ :=
by simp [← cos_angle_mul_norm_mul_norm, h]

/-- The inner product of two non-zero vectors equals the negative product of their norms
if and only if the angle between the two vectors is π. -/
lemma inner_eq_neg_mul_norm_iff_angle_eq_pi {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
  ⟪x, y⟫ = - (∥x∥ * ∥y∥) ↔ angle x y = π :=
begin
  refine ⟨λ h, _, inner_eq_neg_mul_norm_of_angle_eq_pi⟩,
  have h₁ : (∥x∥ * ∥y∥) ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne',
  rw [angle, h, neg_div, div_self h₁, real.arccos_neg_one],
end

/-- The inner product of two non-zero vectors equals the product of their norms
if and only if the angle between the two vectors is 0. -/
lemma inner_eq_mul_norm_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
  ⟪x, y⟫ = ∥x∥ * ∥y∥ ↔ angle x y = 0 :=
begin
  refine ⟨λ h, _, inner_eq_mul_norm_of_angle_eq_zero⟩,
  have h₁ : (∥x∥ * ∥y∥) ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne',
  rw [angle, h, div_self h₁, real.arccos_one],
end

/-- If the angle between two vectors is π, the norm of their difference equals
the sum of their norms. -/
lemma norm_sub_eq_add_norm_of_angle_eq_pi {x y : V} (h : angle x y = π) : ∥x - y∥ = ∥x∥ + ∥y∥ :=
begin
  rw ← sq_eq_sq (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
  rw [norm_sub_pow_two_real, inner_eq_neg_mul_norm_of_angle_eq_pi h],
  ring,
end

/-- If the angle between two vectors is 0, the norm of their sum equals
the sum of their norms. -/
lemma norm_add_eq_add_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) : ∥x + y∥ = ∥x∥ + ∥y∥ :=
begin
  rw ← sq_eq_sq (norm_nonneg (x + y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
  rw [norm_add_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h],
  ring,
end

/-- If the angle between two vectors is 0, the norm of their difference equals
the absolute value of the difference of their norms. -/
lemma norm_sub_eq_abs_sub_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) :
  ∥x - y∥ = |∥x∥ - ∥y∥| :=
begin
  rw [← sq_eq_sq (norm_nonneg (x - y)) (abs_nonneg (∥x∥ - ∥y∥)),
      norm_sub_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h, sq_abs (∥x∥ - ∥y∥)],
  ring,
end

/-- The norm of the difference of two non-zero vectors equals the sum of their norms
if and only the angle between the two vectors is π. -/
lemma norm_sub_eq_add_norm_iff_angle_eq_pi {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
  ∥x - y∥ = ∥x∥ + ∥y∥ ↔ angle x y = π :=
begin
  refine ⟨λ h, _, norm_sub_eq_add_norm_of_angle_eq_pi⟩,
  rw ← inner_eq_neg_mul_norm_iff_angle_eq_pi hx hy,
  obtain ⟨hxy₁, hxy₂⟩ := ⟨norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg y)⟩,
  rw [← sq_eq_sq hxy₁ hxy₂, norm_sub_pow_two_real] at h,
  calc inner x y = (∥x∥ ^ 2 + ∥y∥ ^ 2 - (∥x∥ + ∥y∥) ^ 2) / 2 : by linarith
  ...            = -(∥x∥ * ∥y∥) : by ring,
end

/-- The norm of the sum of two non-zero vectors equals the sum of their norms
if and only the angle between the two vectors is 0. -/
lemma norm_add_eq_add_norm_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
  ∥x + y∥ = ∥x∥ + ∥y∥ ↔ angle x y = 0 :=
begin
  refine ⟨λ h, _, norm_add_eq_add_norm_of_angle_eq_zero⟩,
  rw ← inner_eq_mul_norm_iff_angle_eq_zero hx hy,
  obtain ⟨hxy₁, hxy₂⟩ := ⟨norm_nonneg (x + y), add_nonneg (norm_nonneg x) (norm_nonneg y)⟩,
  rw [← sq_eq_sq hxy₁ hxy₂, norm_add_pow_two_real] at h,
  calc inner x y = ((∥x∥ + ∥y∥) ^ 2 - ∥x∥ ^ 2 - ∥y∥ ^ 2)/ 2 : by linarith
  ...            = ∥x∥ * ∥y∥ : by ring,
end

/-- The norm of the difference of two non-zero vectors equals the absolute value
of the difference of their norms if and only the angle between the two vectors is 0. -/
lemma norm_sub_eq_abs_sub_norm_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
  ∥x - y∥ = |∥x∥ - ∥y∥| ↔ angle x y = 0 :=
begin
  refine ⟨λ h, _, norm_sub_eq_abs_sub_norm_of_angle_eq_zero⟩,
  rw ← inner_eq_mul_norm_iff_angle_eq_zero hx hy,
  have h1 : ∥x - y∥ ^ 2 = (∥x∥ - ∥y∥) ^ 2, { rw h, exact sq_abs (∥x∥ - ∥y∥) },
  rw norm_sub_pow_two_real at h1,
  calc inner x y = ((∥x∥ + ∥y∥) ^ 2 - ∥x∥ ^ 2 - ∥y∥ ^ 2)/ 2 : by linarith
  ...            = ∥x∥ * ∥y∥ : by ring,
end

/-- The norm of the sum of two vectors equals the norm of their difference if and only if
the angle between them is π/2. -/
lemma norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (x y : V) :
  ∥x + y∥ = ∥x - y∥ ↔ angle x y = π / 2 :=
begin
  rw [← sq_eq_sq (norm_nonneg (x + y)) (norm_nonneg (x - y)),
      ← inner_eq_zero_iff_angle_eq_pi_div_two x y, norm_add_pow_two_real, norm_sub_pow_two_real],
  split; intro h; linarith,
end

end inner_product_geometry

namespace euclidean_geometry
/-!
### Geometrical results on Euclidean affine spaces

This section develops some geometrical definitions and results on
Euclidean affine spaces.
-/
open inner_product_geometry

variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
    [normed_add_torsor V P]
local notation `⟪`x`, `y`⟫` := @inner ℝ V _ x y
include V

/-- The undirected angle at `p2` between the line segments to `p1` and
`p3`. If either of those points equals `p2`, this is π/2. Use
`open_locale euclidean_geometry` to access the `∠ p1 p2 p3`
notation. -/
def angle (p1 p2 p3 : P) : ℝ := angle (p1 -ᵥ p2 : V) (p3 -ᵥ p2)

localized "notation `∠` := euclidean_geometry.angle" in euclidean_geometry

lemma continuous_at_angle {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.2 ≠ x.2.1) :
  continuous_at (λ y : P × P × P, ∠ y.1 y.2.1 y.2.2) x :=
begin
  let f : P × P × P → V × V := λ y, (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1),
  have hf1 : (f x).1 ≠ 0, by simp [hx12],
  have hf2 : (f x).2 ≠ 0, by simp [hx32],
  exact (inner_product_geometry.continuous_at_angle hf1 hf2).comp
    ((continuous_fst.vsub continuous_snd.fst).prod_mk
      (continuous_snd.snd.vsub continuous_snd.fst)).continuous_at
end

/-- The angle at a point does not depend on the order of the other two
points. -/
lemma angle_comm (p1 p2 p3 : P) : ∠ p1 p2 p3 = ∠ p3 p2 p1 :=
angle_comm _ _

/-- The angle at a point is nonnegative. -/
lemma angle_nonneg (p1 p2 p3 : P) : 0 ≤ ∠ p1 p2 p3 :=
angle_nonneg _ _

/-- The angle at a point is at most π. -/
lemma angle_le_pi (p1 p2 p3 : P) : ∠ p1 p2 p3 ≤ π :=
angle_le_pi _ _

/-- The angle ∠AAB at a point. -/
lemma angle_eq_left (p1 p2 : P) : ∠ p1 p1 p2 = π / 2 :=
begin
  unfold angle,
  rw vsub_self,
  exact angle_zero_left _
end

/-- The angle ∠ABB at a point. -/
lemma angle_eq_right (p1 p2 : P) : ∠ p1 p2 p2 = π / 2 :=
by rw [angle_comm, angle_eq_left]

/-- The angle ∠ABA at a point. -/
lemma angle_eq_of_ne {p1 p2 : P} (h : p1 ≠ p2) : ∠ p1 p2 p1 = 0 :=
angle_self (λ he, h (vsub_eq_zero_iff_eq.1 he))

/-- If the angle ∠ABC at a point is π, the angle ∠BAC is 0. -/
lemma angle_eq_zero_of_angle_eq_pi_left {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = π) :
  ∠ p2 p1 p3 = 0 :=
begin
  unfold angle at h,
  rw angle_eq_pi_iff at h,
  rcases h with ⟨hp1p2, ⟨r, ⟨hr, hpr⟩⟩⟩,
  unfold angle,
  rw angle_eq_zero_iff,
  rw [←neg_vsub_eq_vsub_rev, neg_ne_zero] at hp1p2,
  use [hp1p2, -r + 1, add_pos (neg_pos_of_neg hr) zero_lt_one],
  rw [add_smul, ←neg_vsub_eq_vsub_rev p1 p2, smul_neg],
  simp [←hpr]
end

/-- If the angle ∠ABC at a point is π, the angle ∠BCA is 0. -/
lemma angle_eq_zero_of_angle_eq_pi_right {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = π) :
  ∠ p2 p3 p1 = 0 :=
begin
  rw angle_comm at h,
  exact angle_eq_zero_of_angle_eq_pi_left h
end

/-- If ∠BCD = π, then ∠ABC = ∠ABD. -/
lemma angle_eq_angle_of_angle_eq_pi (p1 : P) {p2 p3 p4 : P} (h : ∠ p2 p3 p4 = π) :
  ∠ p1 p2 p3 = ∠ p1 p2 p4 :=
begin
  unfold angle at *,
  rcases angle_eq_pi_iff.1 h with ⟨hp2p3, ⟨r, ⟨hr, hpr⟩⟩⟩,
  rw [eq_comm],
  convert angle_smul_right_of_pos (p1 -ᵥ p2) (p3 -ᵥ p2) (add_pos (neg_pos_of_neg hr) zero_lt_one),
  rw [add_smul, ← neg_vsub_eq_vsub_rev p2 p3, smul_neg, neg_smul, ← hpr],
  simp
end

/-- If ∠BCD = π, then ∠ACB + ∠ACD = π. -/
lemma angle_add_angle_eq_pi_of_angle_eq_pi (p1 : P) {p2 p3 p4 : P} (h : ∠ p2 p3 p4 = π) :
  ∠ p1 p3 p2 + ∠ p1 p3 p4 = π :=
begin
  unfold angle at h,
  rw [angle_comm p1 p3 p2, angle_comm p1 p3 p4],
  unfold angle,
  exact angle_add_angle_eq_pi_of_angle_eq_pi _ h
end

/-- Vertical Angles Theorem: angles opposite each other, formed by two intersecting straight
lines, are equal. -/
lemma angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi {p1 p2 p3 p4 p5 : P}
  (hapc : ∠ p1 p5 p3 = π) (hbpd : ∠ p2 p5 p4 = π) : ∠ p1 p5 p2 = ∠ p3 p5 p4 :=
by linarith [angle_add_angle_eq_pi_of_angle_eq_pi p1 hbpd, angle_comm p4 p5 p1,
             angle_add_angle_eq_pi_of_angle_eq_pi p4 hapc, angle_comm p4 p5 p3]

/-- If ∠ABC = π then dist A B ≠ 0. -/
lemma left_dist_ne_zero_of_angle_eq_pi {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = π) : dist p1 p2 ≠ 0 :=
begin
  by_contra heq,
  rw [dist_eq_zero] at heq,
  rw [heq, angle_eq_left] at h,
  exact real.pi_ne_zero (by linarith),
end

/-- If ∠ABC = π then dist C B ≠ 0. -/
lemma right_dist_ne_zero_of_angle_eq_pi {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = π) : dist p3 p2 ≠ 0 :=
left_dist_ne_zero_of_angle_eq_pi $ (angle_comm _ _ _).trans h

/-- If ∠ABC = π, then (dist A C) = (dist A B) + (dist B C). -/
lemma dist_eq_add_dist_of_angle_eq_pi {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = π) :
  dist p1 p3 = dist p1 p2 + dist p3 p2 :=
begin
  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right],
  exact norm_sub_eq_add_norm_of_angle_eq_pi h,
end

/-- If A ≠ B and C ≠ B then ∠ABC = π if and only if (dist A C) = (dist A B) + (dist B C). -/
lemma dist_eq_add_dist_iff_angle_eq_pi {p1 p2 p3 : P} (hp1p2 : p1 ≠ p2) (hp3p2 : p3 ≠ p2) :
  dist p1 p3 = dist p1 p2 + dist p3 p2 ↔ ∠ p1 p2 p3 = π :=
begin
  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right],
  exact norm_sub_eq_add_norm_iff_angle_eq_pi
    ((λ he, hp1p2 (vsub_eq_zero_iff_eq.1 he))) (λ he, hp3p2 (vsub_eq_zero_iff_eq.1 he)),
end

/-- If ∠ABC = 0, then (dist A C) = abs ((dist A B) - (dist B C)). -/
lemma dist_eq_abs_sub_dist_of_angle_eq_zero {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = 0) :
  (dist p1 p3) = |(dist p1 p2) - (dist p3 p2)| :=
begin
  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right],
  exact norm_sub_eq_abs_sub_norm_of_angle_eq_zero h,
end

/-- If A ≠ B and C ≠ B then ∠ABC = 0 if and only if (dist A C) = abs ((dist A B) - (dist B C)). -/
lemma dist_eq_abs_sub_dist_iff_angle_eq_zero {p1 p2 p3 : P} (hp1p2 : p1 ≠ p2) (hp3p2 : p3 ≠ p2) :
  (dist p1 p3) = |(dist p1 p2) - (dist p3 p2)| ↔ ∠ p1 p2 p3 = 0 :=
begin
  rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right],
  exact norm_sub_eq_abs_sub_norm_iff_angle_eq_zero
    ((λ he, hp1p2 (vsub_eq_zero_iff_eq.1 he))) (λ he, hp3p2 (vsub_eq_zero_iff_eq.1 he)),
end

/-- The midpoint of the segment AB is the same distance from A as it is from B. -/
lemma dist_left_midpoint_eq_dist_right_midpoint (p1 p2 : P) :
  dist p1 (midpoint ℝ p1 p2) = dist p2 (midpoint ℝ p1 p2) :=
by rw [dist_left_midpoint p1 p2, dist_right_midpoint p1 p2]

/-- If M is the midpoint of the segment AB, then ∠AMB = π. -/
lemma angle_midpoint_eq_pi (p1 p2 : P) (hp1p2 : p1 ≠ p2) : ∠ p1 (midpoint ℝ p1 p2) p2 = π :=
have p2 -ᵥ midpoint ℝ p1 p2 = -(p1 -ᵥ midpoint ℝ p1 p2), by { rw neg_vsub_eq_vsub_rev, simp },
by simp [angle, this, hp1p2, -zero_lt_one]

/-- If M is the midpoint of the segment AB and C is the same distance from A as it is from B
then ∠CMA = π / 2. -/
lemma angle_left_midpoint_eq_pi_div_two_of_dist_eq {p1 p2 p3 : P} (h : dist p3 p1 = dist p3 p2) :
  ∠ p3 (midpoint ℝ p1 p2) p1 = π / 2 :=
begin
  let m : P := midpoint ℝ p1 p2,
  have h1 : p3 -ᵥ p1 = (p3 -ᵥ m) - (p1 -ᵥ m) := (vsub_sub_vsub_cancel_right p3 p1 m).symm,
  have h2 : p3 -ᵥ p2 = (p3 -ᵥ m) + (p1 -ᵥ m),
  { rw [left_vsub_midpoint, ← midpoint_vsub_right, vsub_add_vsub_cancel] },
  rw [dist_eq_norm_vsub V p3 p1, dist_eq_norm_vsub V p3 p2, h1, h2] at h,
  exact (norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (p3 -ᵥ m) (p1 -ᵥ m)).mp h.symm,
end

/-- If M is the midpoint of the segment AB and C is the same distance from A as it is from B
then ∠CMB = π / 2. -/
lemma angle_right_midpoint_eq_pi_div_two_of_dist_eq {p1 p2 p3 : P} (h : dist p3 p1 = dist p3 p2) :
  ∠ p3 (midpoint ℝ p1 p2) p2 = π / 2 :=
by rw [midpoint_comm p1 p2, angle_left_midpoint_eq_pi_div_two_of_dist_eq h.symm]

/-- The inner product of two vectors given with `weighted_vsub`, in
terms of the pairwise distances. -/
lemma inner_weighted_vsub {ι₁ : Type*} {s₁ : finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P)
    (h₁ : ∑ i in s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P)
    (h₂ : ∑ i in s₂, w₂ i = 0) :
  inner (s₁.weighted_vsub p₁ w₁) (s₂.weighted_vsub p₂ w₂) =
    (-∑ i₁ in s₁, ∑ i₂ in s₂,
      w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2 :=
begin
  rw [finset.weighted_vsub_apply, finset.weighted_vsub_apply,
      inner_sum_smul_sum_smul_of_sum_eq_zero _ h₁ _ h₂],
  simp_rw [vsub_sub_vsub_cancel_right],
  rcongr i₁ i₂; rw dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)
end

/-- The distance between two points given with `affine_combination`,
in terms of the pairwise distances between the points in that
combination. -/
lemma dist_affine_combination {ι : Type*} {s : finset ι} {w₁ w₂ : ι → ℝ} (p : ι → P)
    (h₁ : ∑ i in s, w₁ i = 1) (h₂ : ∑ i in s, w₂ i = 1) :
  by have a₁ := s.affine_combination p w₁; have a₂ := s.affine_combination p w₂; exact
  dist a₁ a₂ * dist a₁ a₂ = (-∑ i₁ in s, ∑ i₂ in s,
      (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2 :=
begin
  rw [dist_eq_norm_vsub V (s.affine_combination p w₁) (s.affine_combination p w₂),
      ←inner_self_eq_norm_mul_norm, finset.affine_combination_vsub],
  have h : ∑ i in s, (w₁ - w₂) i = 0,
  { simp_rw [pi.sub_apply, finset.sum_sub_distrib, h₁, h₂, sub_self] },
  exact inner_weighted_vsub p h p h
end

/-- Suppose that `c₁` is equidistant from `p₁` and `p₂`, and the same
applies to `c₂`.  Then the vector between `c₁` and `c₂` is orthogonal
to that between `p₁` and `p₂`.  (In two dimensions, this says that the
diagonals of a kite are orthogonal.) -/
lemma inner_vsub_vsub_of_dist_eq_of_dist_eq {c₁ c₂ p₁ p₂ : P} (hc₁ : dist p₁ c₁ = dist p₂ c₁)
  (hc₂ : dist p₁ c₂ = dist p₂ c₂) : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
begin
  have h : ⟪(c₂ -ᵥ c₁) + (c₂ -ᵥ c₁), p₂ -ᵥ p₁⟫ = 0,
  { conv_lhs { congr, congr, rw ←vsub_sub_vsub_cancel_right c₂ c₁ p₁,
               skip, rw ←vsub_sub_vsub_cancel_right c₂ c₁ p₂ },
    rw [sub_add_sub_comm, inner_sub_left],
    conv_lhs { congr, rw ←vsub_sub_vsub_cancel_right p₂ p₁ c₂,
               skip, rw ←vsub_sub_vsub_cancel_right p₂ p₁ c₁ },
    rw [dist_comm p₁, dist_comm p₂, dist_eq_norm_vsub V _ p₁,
        dist_eq_norm_vsub V _ p₂, ←real_inner_add_sub_eq_zero_iff] at hc₁ hc₂,
    simp_rw [←neg_vsub_eq_vsub_rev c₁, ←neg_vsub_eq_vsub_rev c₂, sub_neg_eq_add,
             neg_add_eq_sub, hc₁, hc₂, sub_zero] },
  simpa [inner_add_left, ←mul_two, (by norm_num : (2 : ℝ) ≠ 0)] using h
end

/-- The squared distance between points on a line (expressed as a
multiple of a fixed vector added to a point) and another point,
expressed as a quadratic. -/
lemma dist_smul_vadd_sq (r : ℝ) (v : V) (p₁ p₂ : P) :
  dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ :=
begin
  rw [dist_eq_norm_vsub V _ p₂, ←real_inner_self_eq_norm_mul_norm, vadd_vsub_assoc,
    real_inner_add_add_self, real_inner_smul_left, real_inner_smul_left, real_inner_smul_right],
  ring
end

/-- The condition for two points on a line to be equidistant from
another point. -/
lemma dist_smul_vadd_eq_dist {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) :
  dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ (r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫) :=
begin
  conv_lhs { rw [←mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq,
                 ←sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂,
                 ←real_inner_self_eq_norm_mul_norm, sub_self] },
  have hvi : ⟪v, v⟫ ≠ 0, by simpa using hv,
  have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 =
    (2 * inner v (p₁ -ᵥ p₂)) * (2 * inner v (p₁ -ᵥ p₂)),
  { rw discrim, ring },
  rw [quadratic_eq_zero_iff hvi hd, add_left_neg, zero_div, neg_mul_eq_neg_mul,
      ←mul_sub_right_distrib, sub_eq_add_neg, ←mul_two, mul_assoc, mul_div_assoc,
      mul_div_mul_left, mul_div_assoc],
  norm_num
end

open affine_subspace finite_dimensional

/-- Distances `r₁` `r₂` of `p` from two different points `c₁` `c₂` determine at
most two points `p₁` `p₂` in a two-dimensional subspace containing those points
(two circles intersect in at most two points). -/
lemma eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two {s : affine_subspace ℝ P}
  [finite_dimensional ℝ s.direction] (hd : finrank ℝ s.direction = 2) {c₁ c₂ p₁ p₂ p : P}
  (hc₁s : c₁ ∈ s) (hc₂s : c₂ ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s) (hps : p ∈ s) {r₁ r₂ : ℝ}
  (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁) (hp₂c₁ : dist p₂ c₁ = r₁)
  (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂) (hp₂c₂ : dist p₂ c₂ = r₂)
  (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂ :=
begin
  have ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
    inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hp₂c₁.symm) (hp₁c₂.trans hp₂c₂.symm),
  have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 :=
    inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hpc₁.symm) (hp₁c₂.trans hpc₂.symm),
  let b : fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁],
  have hb : linear_independent ℝ b,
  { refine linear_independent_of_ne_zero_of_inner_eq_zero _ _,
    { intro i,
      fin_cases i; simp [b, hc.symm, hp.symm], },
    { intros i j hij,
      fin_cases i; fin_cases j; try { exact false.elim (hij rfl) },
      { exact ho },
      { rw real_inner_comm, exact ho } } },
  have hbs : submodule.span ℝ (set.range b) = s.direction,
  { refine eq_of_le_of_finrank_eq _ _,
    { rw [submodule.span_le, set.range_subset_iff],
      intro i,
      fin_cases i,
      { exact vsub_mem_direction hc₂s hc₁s },
      { exact vsub_mem_direction hp₂s hp₁s } },
    { rw [finrank_span_eq_card hb, fintype.card_fin, hd] } },
  have hv : ∀ v ∈ s.direction, ∃ t₁ t₂ : ℝ, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁),
  { intros v hv,
    have hr : set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁},
    { have hu : (finset.univ : finset (fin 2)) = {0, 1}, by dec_trivial,
      rw [←fintype.coe_image_univ, hu],
      simp,
      refl },
    rw [←hbs, hr, submodule.mem_span_insert] at hv,
    rcases hv with ⟨t₁, v', hv', hv⟩,
    rw submodule.mem_span_singleton at hv',
    rcases hv' with ⟨t₂, rfl⟩,
    exact ⟨t₁, t₂, hv⟩ },
  rcases hv (p -ᵥ p₁) (vsub_mem_direction hps hp₁s) with ⟨t₁, t₂, hpt⟩,
  simp only [hpt, inner_add_right, inner_smul_right, ho, mul_zero, add_zero, mul_eq_zero,
             inner_self_eq_zero, vsub_eq_zero_iff_eq, hc.symm, or_false] at hop,
  rw [hop, zero_smul, zero_add, ←eq_vadd_iff_vsub_eq] at hpt,
  subst hpt,
  have hp' : (p₂ -ᵥ p₁ : V) ≠ 0, { simp [hp.symm] },
  have hp₂ : dist ((1 : ℝ) • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁, { simp [hp₂c₁] },
  rw [←hp₁c₁, dist_smul_vadd_eq_dist _ _ hp'] at hpc₁ hp₂,
  simp only [one_ne_zero, false_or] at hp₂,
  rw hp₂.symm at hpc₁,
  cases hpc₁; simp [hpc₁]
end

/-- Distances `r₁` `r₂` of `p` from two different points `c₁` `c₂` determine at
most two points `p₁` `p₂` in two-dimensional space (two circles intersect in at
most two points). -/
lemma eq_of_dist_eq_of_dist_eq_of_finrank_eq_two [finite_dimensional ℝ V] (hd : finrank ℝ V = 2)
  {c₁ c₂ p₁ p₂ p : P} {r₁ r₂ : ℝ} (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁)
  (hp₂c₁ : dist p₂ c₁ = r₁) (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂)
  (hp₂c₂ : dist p₂ c₂ = r₂) (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂ :=
begin
  have hd' : finrank ℝ (⊤ : affine_subspace ℝ P).direction = 2,
  { rw [direction_top, finrank_top],
    exact hd },
  exact eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two hd'
    (mem_top ℝ V _) (mem_top ℝ V _) (mem_top ℝ V _) (mem_top ℝ V _) (mem_top ℝ V _)
    hc hp hp₁c₁ hp₂c₁ hpc₁ hp₁c₂ hp₂c₂ hpc₂
end

variables {V}

/-- The orthogonal projection of a point onto a nonempty affine
subspace, whose direction is complete, as an unbundled function.  This
definition is only intended for use in setting up the bundled version
`orthogonal_projection` and should not be used once that is
defined. -/
def orthogonal_projection_fn (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction]
  (p : P) : P :=
classical.some $ inter_eq_singleton_of_nonempty_of_is_compl
  (nonempty_subtype.mp ‹_›)
  (mk'_nonempty p s.directionᗮ)
  begin
    rw direction_mk' p s.directionᗮ,
    exact submodule.is_compl_orthogonal_of_complete_space,
  end

/-- The intersection of the subspace and the orthogonal subspace
through the given point is the `orthogonal_projection_fn` of that
point onto the subspace.  This lemma is only intended for use in
setting up the bundled version and should not be used once that is
defined. -/
lemma inter_eq_singleton_orthogonal_projection_fn {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] (p : P) :
  (s : set P) ∩ (mk' p s.directionᗮ) = {orthogonal_projection_fn s p} :=
classical.some_spec $ inter_eq_singleton_of_nonempty_of_is_compl
  (nonempty_subtype.mp ‹_›)
  (mk'_nonempty p s.directionᗮ)
  begin
    rw direction_mk' p s.directionᗮ,
    exact submodule.is_compl_orthogonal_of_complete_space
  end

/-- The `orthogonal_projection_fn` lies in the given subspace.  This
lemma is only intended for use in setting up the bundled version and
should not be used once that is defined. -/
lemma orthogonal_projection_fn_mem {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] (p : P) : orthogonal_projection_fn s p ∈ s :=
begin
  rw [←mem_coe, ←set.singleton_subset_iff, ←inter_eq_singleton_orthogonal_projection_fn],
  exact set.inter_subset_left _ _
end

/-- The `orthogonal_projection_fn` lies in the orthogonal
subspace.  This lemma is only intended for use in setting up the
bundled version and should not be used once that is defined. -/
lemma orthogonal_projection_fn_mem_orthogonal {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] (p : P) :
  orthogonal_projection_fn s p ∈ mk' p s.directionᗮ :=
begin
  rw [←mem_coe, ←set.singleton_subset_iff, ←inter_eq_singleton_orthogonal_projection_fn],
  exact set.inter_subset_right _ _
end

/-- Subtracting `p` from its `orthogonal_projection_fn` produces a
result in the orthogonal direction.  This lemma is only intended for
use in setting up the bundled version and should not be used once that
is defined. -/
lemma orthogonal_projection_fn_vsub_mem_direction_orthogonal {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] (p : P) :
  orthogonal_projection_fn s p -ᵥ p ∈ s.directionᗮ :=
direction_mk' p s.directionᗮ ▸
  vsub_mem_direction (orthogonal_projection_fn_mem_orthogonal p) (self_mem_mk' _ _)

/-- The orthogonal projection of a point onto a nonempty affine
subspace, whose direction is complete. The corresponding linear map
(mapping a vector to the difference between the projections of two
points whose difference is that vector) is the `orthogonal_projection`
for real inner product spaces, onto the direction of the affine
subspace being projected onto. -/
def orthogonal_projection (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
  P →ᵃ[ℝ] s :=
{ to_fun := λ p, ⟨orthogonal_projection_fn s p, orthogonal_projection_fn_mem p⟩,
  linear := orthogonal_projection s.direction,
  map_vadd' := λ p v, begin
    have hs : ((orthogonal_projection s.direction) v : V) +ᵥ orthogonal_projection_fn s p ∈ s :=
      vadd_mem_of_mem_direction (orthogonal_projection s.direction v).2
                                (orthogonal_projection_fn_mem p),
    have ho : ((orthogonal_projection s.direction) v : V) +ᵥ orthogonal_projection_fn s p ∈
      mk' (v +ᵥ p) s.directionᗮ,
    { rw [←vsub_right_mem_direction_iff_mem (self_mem_mk' _ _) _, direction_mk',
          vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc],
      refine submodule.add_mem _ (orthogonal_projection_fn_vsub_mem_direction_orthogonal p) _,
      rw submodule.mem_orthogonal',
      intros w hw,
      rw [←neg_sub, inner_neg_left, orthogonal_projection_inner_eq_zero _ w hw, neg_zero], },
    have hm : ((orthogonal_projection s.direction) v : V) +ᵥ orthogonal_projection_fn s p ∈
      ({orthogonal_projection_fn s (v +ᵥ p)} : set P),
    { rw ←inter_eq_singleton_orthogonal_projection_fn (v +ᵥ p),
      exact set.mem_inter hs ho },
    rw set.mem_singleton_iff at hm,
    ext,
    exact hm.symm
  end }

@[simp] lemma orthogonal_projection_fn_eq {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] (p : P) :
  orthogonal_projection_fn s p = orthogonal_projection s p :=
rfl

/-- The linear map corresponding to `orthogonal_projection`. -/
@[simp] lemma orthogonal_projection_linear {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] :
  (orthogonal_projection s).linear = _root_.orthogonal_projection s.direction :=
rfl

/-- The intersection of the subspace and the orthogonal subspace
through the given point is the `orthogonal_projection` of that point
onto the subspace. -/
lemma inter_eq_singleton_orthogonal_projection {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] (p : P) :
  (s : set P) ∩ (mk' p s.directionᗮ) = {orthogonal_projection s p} :=
begin
  rw ←orthogonal_projection_fn_eq,
  exact inter_eq_singleton_orthogonal_projection_fn p
end

/-- The `orthogonal_projection` lies in the given subspace. -/
lemma orthogonal_projection_mem {s : affine_subspace ℝ P} [nonempty s] [complete_space s.direction]
  (p : P) : ↑(orthogonal_projection s p) ∈ s :=
(orthogonal_projection s p).2

/-- The `orthogonal_projection` lies in the orthogonal subspace. -/
lemma orthogonal_projection_mem_orthogonal (s : affine_subspace ℝ P) [nonempty s]
  [complete_space s.direction] (p : P) :
  ↑(orthogonal_projection s p) ∈ mk' p s.directionᗮ :=
orthogonal_projection_fn_mem_orthogonal p

/-- Subtracting a point in the given subspace from the
`orthogonal_projection` produces a result in the direction of the
given subspace. -/
lemma orthogonal_projection_vsub_mem_direction {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :
  ↑(orthogonal_projection s p2 -ᵥ ⟨p1, hp1⟩ : s.direction) ∈ s.direction :=
(orthogonal_projection s p2 -ᵥ ⟨p1, hp1⟩ : s.direction).2

/-- Subtracting the `orthogonal_projection` from a point in the given
subspace produces a result in the direction of the given subspace. -/
lemma vsub_orthogonal_projection_mem_direction {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :
  ↑((⟨p1, hp1⟩ : s) -ᵥ orthogonal_projection s p2 : s.direction) ∈ s.direction :=
((⟨p1, hp1⟩ : s) -ᵥ orthogonal_projection s p2 : s.direction).2

/-- A point equals its orthogonal projection if and only if it lies in
the subspace. -/
lemma orthogonal_projection_eq_self_iff {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p : P} :
  ↑(orthogonal_projection s p) = p ↔ p ∈ s :=
begin
  split,
  { exact λ h, h ▸ orthogonal_projection_mem p },
  { intro h,
    have hp : p ∈ ((s : set P) ∩ mk' p s.directionᗮ) := ⟨h, self_mem_mk' p _⟩,
    rw [inter_eq_singleton_orthogonal_projection p] at hp,
    symmetry,
    exact hp }
end

@[simp] lemma orthogonal_projection_mem_subspace_eq_self {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] (p : s) :
  orthogonal_projection s p = p :=
begin
  ext,
  rw orthogonal_projection_eq_self_iff,
  exact p.2
end

/-- Orthogonal projection is idempotent. -/
@[simp] lemma orthogonal_projection_orthogonal_projection (s : affine_subspace ℝ P) [nonempty s]
  [complete_space s.direction] (p : P) :
  orthogonal_projection s (orthogonal_projection s p) = orthogonal_projection s p :=
begin
  ext,
  rw orthogonal_projection_eq_self_iff,
  exact orthogonal_projection_mem p,
end

lemma eq_orthogonal_projection_of_eq_subspace {s s' : affine_subspace ℝ P} [nonempty s]
  [nonempty s'] [complete_space s.direction] [complete_space s'.direction] (h : s = s') (p : P) :
  (orthogonal_projection s p : P) = (orthogonal_projection s' p : P) :=
begin
  change orthogonal_projection_fn s p = orthogonal_projection_fn s' p,
  congr,
  exact h
end

/-- The distance to a point's orthogonal projection is 0 iff it lies in the subspace. -/
lemma dist_orthogonal_projection_eq_zero_iff {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p : P} :
  dist p (orthogonal_projection s p) = 0 ↔ p ∈ s :=
by rw [dist_comm, dist_eq_zero, orthogonal_projection_eq_self_iff]

/-- The distance between a point and its orthogonal projection is
nonzero if it does not lie in the subspace. -/
lemma dist_orthogonal_projection_ne_zero_of_not_mem {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p : P} (hp : p ∉ s) :
  dist p (orthogonal_projection s p) ≠ 0 :=
mt dist_orthogonal_projection_eq_zero_iff.mp hp

/-- Subtracting `p` from its `orthogonal_projection` produces a result
in the orthogonal direction. -/
lemma orthogonal_projection_vsub_mem_direction_orthogonal (s : affine_subspace ℝ P) [nonempty s]
  [complete_space s.direction] (p : P) :
  (orthogonal_projection s p : P) -ᵥ p ∈ s.directionᗮ :=
orthogonal_projection_fn_vsub_mem_direction_orthogonal p

/-- Subtracting the `orthogonal_projection` from `p` produces a result
in the orthogonal direction. -/
lemma vsub_orthogonal_projection_mem_direction_orthogonal (s : affine_subspace ℝ P) [nonempty s]
  [complete_space s.direction] (p : P) :
  p -ᵥ orthogonal_projection s p ∈ s.directionᗮ :=
direction_mk' p s.directionᗮ ▸
  vsub_mem_direction (self_mem_mk' _ _) (orthogonal_projection_mem_orthogonal s p)

/-- Subtracting the `orthogonal_projection` from `p` produces a result in the kernel of the linear
part of the orthogonal projection. -/
lemma orthogonal_projection_vsub_orthogonal_projection (s : affine_subspace ℝ P) [nonempty s]
  [complete_space s.direction] (p : P) :
  _root_.orthogonal_projection s.direction (p -ᵥ orthogonal_projection s p) = 0 :=
begin
  apply orthogonal_projection_mem_subspace_orthogonal_complement_eq_zero,
  intros c hc,
  rw [← neg_vsub_eq_vsub_rev, inner_neg_right,
    (orthogonal_projection_vsub_mem_direction_orthogonal s p c hc), neg_zero]
end

/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector was
in the orthogonal direction. -/
lemma orthogonal_projection_vadd_eq_self {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p : P} (hp : p ∈ s) {v : V}
  (hv : v ∈ s.directionᗮ) :
  orthogonal_projection s (v +ᵥ p) = ⟨p, hp⟩ :=
begin
  have h := vsub_orthogonal_projection_mem_direction_orthogonal s (v +ᵥ p),
  rw [vadd_vsub_assoc, submodule.add_mem_iff_right _ hv] at h,
  refine (eq_of_vsub_eq_zero _).symm,
  ext,
  refine submodule.disjoint_def.1 s.direction.orthogonal_disjoint _ _ h,
  exact (_ : s.direction).2
end

/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector is a
multiple of the result of subtracting a point's orthogonal projection
from that point. -/
lemma orthogonal_projection_vadd_smul_vsub_orthogonal_projection {s : affine_subspace ℝ P}
  [nonempty s] [complete_space s.direction] {p1 : P} (p2 : P) (r : ℝ) (hp : p1 ∈ s) :
  orthogonal_projection s (r • (p2 -ᵥ orthogonal_projection s p2 : V) +ᵥ p1) = ⟨p1, hp⟩ :=
orthogonal_projection_vadd_eq_self hp
  (submodule.smul_mem _ _ (vsub_orthogonal_projection_mem_direction_orthogonal s _))

/-- The square of the distance from a point in `s` to `p2` equals the
sum of the squares of the distances of the two points to the
`orthogonal_projection`. -/
lemma dist_sq_eq_dist_orthogonal_projection_sq_add_dist_orthogonal_projection_sq
  {s : affine_subspace ℝ P} [nonempty s] [complete_space s.direction] {p1 : P}
  (p2 : P) (hp1 : p1 ∈ s) :
  dist p1 p2 * dist p1 p2 =
    dist p1 (orthogonal_projection s p2) * dist p1 (orthogonal_projection s p2) +
    dist p2 (orthogonal_projection s p2) * dist p2 (orthogonal_projection s p2) :=
begin
  rw [dist_comm p2 _, dist_eq_norm_vsub V p1 _, dist_eq_norm_vsub V p1 _,
    dist_eq_norm_vsub V _ p2, ← vsub_add_vsub_cancel p1 (orthogonal_projection s p2) p2,
    norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero],
  exact submodule.inner_right_of_mem_orthogonal
    (vsub_orthogonal_projection_mem_direction p2 hp1)
    (orthogonal_projection_vsub_mem_direction_orthogonal s p2),
end

/-- The square of the distance between two points constructed by
adding multiples of the same orthogonal vector to points in the same
subspace. -/
lemma dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd {s : affine_subspace ℝ P}
    {p1 p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) (r1 r2 : ℝ) {v : V}
    (hv : v ∈ s.directionᗮ) :
  dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) =
    dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (∥v∥ * ∥v∥) :=
calc dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2)
    = ∥(p1 -ᵥ p2) + (r1 - r2) • v∥ * ∥(p1 -ᵥ p2) + (r1 - r2) • v∥
  : by rw [dist_eq_norm_vsub V (r1 • v +ᵥ p1), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul,
      add_comm, add_sub_assoc]
... = ∥p1 -ᵥ p2∥ * ∥p1 -ᵥ p2∥ + ∥(r1 - r2) • v∥ * ∥(r1 - r2) • v∥
  : norm_add_sq_eq_norm_sq_add_norm_sq_real
      (submodule.inner_right_of_mem_orthogonal (vsub_mem_direction hp1 hp2)
        (submodule.smul_mem _ _ hv))
... = ∥(p1 -ᵥ p2 : V)∥ * ∥(p1 -ᵥ p2 : V)∥ + |r1 - r2| * |r1 - r2| * ∥v∥ * ∥v∥
  : by { rw [norm_smul, real.norm_eq_abs], ring }
... = dist p1 p2 * dist p1 p2 + (r1 - r2) * (r1 - r2) * (∥v∥ * ∥v∥)
  : by { rw [dist_eq_norm_vsub V p1, abs_mul_abs_self, mul_assoc] }

/-- Reflection in an affine subspace, which is expected to be nonempty
and complete.  The word "reflection" is sometimes understood to mean
specifically reflection in a codimension-one subspace, and sometimes
more generally to cover operations such as reflection in a point.  The
definition here, of reflection in an affine subspace, is a more
general sense of the word that includes both those common cases. -/
def reflection (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
  P ≃ᵃⁱ[ℝ] P :=
affine_isometry_equiv.mk'
  (λ p, (↑(orthogonal_projection s p) -ᵥ p) +ᵥ orthogonal_projection s p)
  (_root_.reflection s.direction)
  ↑(classical.arbitrary s)
  begin
    intros p,
    let v := p -ᵥ ↑(classical.arbitrary s),
    let a : V := _root_.orthogonal_projection s.direction v,
    let b : P := ↑(classical.arbitrary s),
    have key : a +ᵥ b -ᵥ (v +ᵥ b) +ᵥ (a +ᵥ b) = a + a - v +ᵥ (b -ᵥ b +ᵥ b),
    { rw [← add_vadd, vsub_vadd_eq_vsub_sub, vsub_vadd, vadd_vsub],
      congr' 1,
      abel },
    have : p = v +ᵥ ↑(classical.arbitrary s) := (vsub_vadd p ↑(classical.arbitrary s)).symm,
    simpa only [coe_vadd, reflection_apply, affine_map.map_vadd, orthogonal_projection_linear,
      orthogonal_projection_mem_subspace_eq_self, vadd_vsub, continuous_linear_map.coe_coe,
      continuous_linear_equiv.coe_coe, this] using key,
  end

/-- The result of reflecting. -/
lemma reflection_apply (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] (p : P) :
  reflection s p = (↑(orthogonal_projection s p) -ᵥ p) +ᵥ orthogonal_projection s p :=
rfl

lemma eq_reflection_of_eq_subspace {s s' : affine_subspace ℝ P} [nonempty s]
  [nonempty s'] [complete_space s.direction] [complete_space s'.direction] (h : s = s') (p : P) :
  (reflection s p : P) = (reflection s' p : P) :=
by unfreezingI { subst h }

/-- Reflecting twice in the same subspace. -/
@[simp] lemma reflection_reflection (s : affine_subspace ℝ P) [nonempty s]
  [complete_space s.direction] (p : P) :
  reflection s (reflection s p) = p :=
begin
  have : ∀ a : s, ∀ b : V, (_root_.orthogonal_projection s.direction) b = 0
    → reflection s (reflection s (b +ᵥ a)) = b +ᵥ a,
  { intros a b h,
    have : (a:P) -ᵥ (b +ᵥ a) = - b,
    { rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub] },
    simp [reflection, h, this] },
  rw ← vsub_vadd p (orthogonal_projection s p),
  exact this (orthogonal_projection s p) _ (orthogonal_projection_vsub_orthogonal_projection s p),
end

/-- Reflection is its own inverse. -/
@[simp] lemma reflection_symm (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
  (reflection s).symm = reflection s :=
by { ext, rw ← (reflection s).injective.eq_iff, simp }

/-- Reflection is involutive. -/
lemma reflection_involutive (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction] :
  function.involutive (reflection s) :=
reflection_reflection s

/-- A point is its own reflection if and only if it is in the
subspace. -/
lemma reflection_eq_self_iff {s : affine_subspace ℝ P} [nonempty s] [complete_space s.direction]
  (p : P) : reflection s p = p ↔ p ∈ s :=
begin
  rw [←orthogonal_projection_eq_self_iff, reflection_apply],
  split,
  { intro h,
    rw [←@vsub_eq_zero_iff_eq V, vadd_vsub_assoc,
        ←two_smul ℝ (↑(orthogonal_projection s p) -ᵥ p), smul_eq_zero] at h,
    norm_num at h,
    exact h },
  { intro h,
    simp [h] }
end

/-- Reflecting a point in two subspaces produces the same result if
and only if the point has the same orthogonal projection in each of
those subspaces. -/
lemma reflection_eq_iff_orthogonal_projection_eq (s₁ s₂ : affine_subspace ℝ P)
  [nonempty s₁] [nonempty s₂] [complete_space s₁.direction] [complete_space s₂.direction] (p : P) :
  reflection s₁ p = reflection s₂ p ↔
    (orthogonal_projection s₁ p : P) = orthogonal_projection s₂ p :=
begin
  rw [reflection_apply, reflection_apply],
  split,
  { intro h,
    rw [←@vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm,
        add_sub_assoc, vsub_sub_vsub_cancel_right,
        ←two_smul ℝ ((orthogonal_projection s₁ p : P) -ᵥ orthogonal_projection s₂ p),
        smul_eq_zero] at h,
    norm_num at h,
    exact h },
  { intro h,
    rw h }
end

/-- The distance between `p₁` and the reflection of `p₂` equals that
between the reflection of `p₁` and `p₂`. -/
lemma dist_reflection (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction]
  (p₁ p₂ : P) :
  dist p₁ (reflection s p₂) = dist (reflection s p₁) p₂ :=
begin
  conv_lhs { rw ←reflection_reflection s p₁ },
  exact (reflection s).dist_map _ _
end

/-- A point in the subspace is equidistant from another point and its
reflection. -/
lemma dist_reflection_eq_of_mem (s : affine_subspace ℝ P) [nonempty s] [complete_space s.direction]
  {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ : P) :
  dist p₁ (reflection s p₂) = dist p₁ p₂ :=
begin
  rw ←reflection_eq_self_iff p₁ at hp₁,
  convert (reflection s).dist_map p₁ p₂,
  rw hp₁
end

/-- The reflection of a point in a subspace is contained in any larger
subspace containing both the point and the subspace reflected in. -/
lemma reflection_mem_of_le_of_mem {s₁ s₂ : affine_subspace ℝ P} [nonempty s₁]
  [complete_space s₁.direction] (hle : s₁ ≤ s₂) {p : P}
  (hp : p ∈ s₂) : reflection s₁ p ∈ s₂ :=
begin
  rw [reflection_apply],
  have ho : ↑(orthogonal_projection s₁ p) ∈ s₂ := hle (orthogonal_projection_mem p),
  exact vadd_mem_of_mem_direction (vsub_mem_direction ho hp) ho
end

/-- Reflecting an orthogonal vector plus a point in the subspace
produces the negation of that vector plus the point. -/
lemma reflection_orthogonal_vadd {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p : P} (hp : p ∈ s) {v : V}
  (hv : v ∈ s.directionᗮ) : reflection s (v +ᵥ p) = -v +ᵥ p :=
begin
  rw [reflection_apply, orthogonal_projection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub],
  simp
end

/-- Reflecting a vector plus a point in the subspace produces the
negation of that vector plus the point if the vector is a multiple of
the result of subtracting a point's orthogonal projection from that
point. -/
lemma reflection_vadd_smul_vsub_orthogonal_projection {s : affine_subspace ℝ P} [nonempty s]
  [complete_space s.direction] {p₁ : P} (p₂ : P) (r : ℝ) (hp₁ : p₁ ∈ s) :
  reflection s (r • (p₂ -ᵥ orthogonal_projection s p₂) +ᵥ p₁) =
    -(r • (p₂ -ᵥ orthogonal_projection s p₂)) +ᵥ p₁ :=
reflection_orthogonal_vadd hp₁
  (submodule.smul_mem _ _ (vsub_orthogonal_projection_mem_direction_orthogonal s _))

omit V

/-- A set of points is cospherical if they are equidistant from some
point.  In two dimensions, this is the same thing as being
concyclic. -/
def cospherical (ps : set P) : Prop :=
∃ (center : P) (radius : ℝ), ∀ p ∈ ps, dist p center = radius

/-- The definition of `cospherical`. -/
lemma cospherical_def (ps : set P) :
  cospherical ps ↔ ∃ (center : P) (radius : ℝ), ∀ p ∈ ps, dist p center = radius :=
iff.rfl

/-- A subset of a cospherical set is cospherical. -/
lemma cospherical_subset {ps₁ ps₂ : set P} (hs : ps₁ ⊆ ps₂) (hc : cospherical ps₂) :
  cospherical ps₁ :=
begin
  rcases hc with ⟨c, r, hcr⟩,
  exact ⟨c, r, λ p hp, hcr p (hs hp)⟩
end

include V

/-- The empty set is cospherical. -/
lemma cospherical_empty : cospherical (∅ : set P) :=
begin
  use add_torsor.nonempty.some,
  simp,
end

omit V

/-- A single point is cospherical. -/
lemma cospherical_singleton (p : P) : cospherical ({p} : set P) :=
begin
  use p,
  simp
end

include V

/-- Two points are cospherical. -/
lemma cospherical_pair (p₁ p₂ : P) : cospherical ({p₁, p₂} : set P) :=
begin
  use [(2⁻¹ : ℝ) • (p₂ -ᵥ p₁) +ᵥ p₁, (2⁻¹ : ℝ) * (dist p₂ p₁)],
  intro p,
  rw [set.mem_insert_iff, set.mem_singleton_iff],
  rintro ⟨_|_⟩,
  { rw [dist_eq_norm_vsub V p₁, vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, norm_neg, norm_smul,
        dist_eq_norm_vsub V p₂],
    simp },
  { rw [H, dist_eq_norm_vsub V p₂, vsub_vadd_eq_vsub_sub, dist_eq_norm_vsub V p₂],
    conv_lhs { congr, congr, rw ←one_smul ℝ (p₂ -ᵥ p₁ : V) },
    rw [←sub_smul, norm_smul],
    norm_num }
end

/-- Any three points in a cospherical set are affinely independent. -/
lemma cospherical.affine_independent {s : set P} (hs : cospherical s) {p : fin 3 → P}
  (hps : set.range p ⊆ s) (hpi : function.injective p) :
  affine_independent ℝ p :=
begin
  rw affine_independent_iff_not_collinear,
  intro hc,
  rw collinear_iff_of_mem ℝ (set.mem_range_self (0 : fin 3)) at hc,
  rcases hc with ⟨v, hv⟩,
  rw set.forall_range_iff at hv,
  have hv0 : v ≠ 0,
  { intro h,
    have he : p 1 = p 0, by simpa [h] using hv 1,
    exact (dec_trivial : (1 : fin 3) ≠ 0) (hpi he) },
  rcases hs with ⟨c, r, hs⟩,
  have hs' := λ i, hs (p i) (set.mem_of_mem_of_subset (set.mem_range_self _) hps),
  choose f hf using hv,
  have hsd : ∀ i, dist ((f i • v) +ᵥ p 0) c = r,
  { intro i,
    rw ←hf,
    exact hs' i },
  have hf0 : f 0 = 0,
  { have hf0' := hf 0,
    rw [eq_comm, ←@vsub_eq_zero_iff_eq V, vadd_vsub, smul_eq_zero] at hf0',
    simpa [hv0] using hf0' },
  have hfi : function.injective f,
  { intros i j h,
    have hi := hf i,
    rw [h, ←hf j] at hi,
    exact hpi hi },
  simp_rw [←hsd 0, hf0, zero_smul, zero_vadd, dist_smul_vadd_eq_dist (p 0) c hv0] at hsd,
  have hfn0 : ∀ i, i ≠ 0 → f i ≠ 0 := λ i, (hfi.ne_iff' hf0).2,
  have hfn0' : ∀ i, i ≠ 0 → f i = (-2) * ⟪v, (p 0 -ᵥ c)⟫ / ⟪v, v⟫,
  { intros i hi,
    have hsdi := hsd i,
    simpa [hfn0, hi] using hsdi },
  have hf12 : f 1 = f 2, { rw [hfn0' 1 dec_trivial, hfn0' 2 dec_trivial] },
  exact (dec_trivial : (1 : fin 3) ≠ 2) (hfi hf12)
end

end euclidean_geometry

subset_name: curated


TITLE: Finding the matrix of a specific scalar product
QUESTION [1 upvotes]: Let $V$ be the vector space over $\mathbb{R}$ whose basis is $(\sin(t),\cos(t))$. Let the scalar product be defined by $$\langle f,g \rangle =\int_{-\pi}^{\pi} f(t)g(t)\,\mathrm dt$$ What is the matrix of this scalar product with respect to the given basis?

$$\langle f,g \rangle = \int_\limits{-\pi}^{\pi} f(t)g(t)\,\mathrm dt = \int_\limits{-\pi}^{\pi}(\sin (t)+\cos(t))(\sin (t)+\cos(t))\,\mathrm dt = 2\pi$$
From a previous exercise with polynomials, I acquired this method. However I do not get a matrix but a number. Am I doing anything wrong? I do not know why people consider it a duplicate, if I am not getting the same result using the same method.
Thanks in advance.

REPLY [2 votes]: It seems like you have not understood what the matrix of a scalar product with respect to a given basis is (even if there were some answers on your previous question), so let me make a general (not truly general but more general) remark on this. Given any $\mathbb{R}$-vector space $V$, say of dimension $n$, with scalar product \begin{align*}⟨ \; , \; ⟩ \colon V \times V &\longrightarrow \mathbb{R}, \\ (v,w) &\longmapsto ⟨v,w⟩, \end{align*} and basis $\mathcal{B}=(v_1, \dots , v_n)$, the matrix of the given scalar product with respect to $\mathcal{B}$ is given by \begin{align*} M_{\mathcal{B}}(⟨ \; , \; ⟩) = (⟨v_i,v_j⟩)_{ij}. \end{align*} Here you can see what you have to compute and where to fill in to get the matrix you are searching for.


TITLE: Solution to second order partial differential equation
QUESTION [4 upvotes]: Suppose $Q$ is the solution to $Q_{tt}-Q_{xx} =0$.
Let $\bar{Q}$ be the solution to $Q_{tt}-Q_{xx}+k Q_t=0$
Is there any known relation between these two solution, given that in the limit of $k$ going to zero, both solution should approach each other?

REPLY [2 votes]: In order to avoid confusion two different notations $P(x,t)$ and $Q(x,t)$ will be used :
$P$ is the solution to $\quad P_{tt}-P_{xx} =0$.
$Q$ is the solution to $\quad Q_{tt}-Q_{xx}+k Q_t=0$
The general solution expressed on the form of integral is :
$$Q(x,t)=\int_{\forall \lambda} F(\lambda)e^{\lambda t +\frac12\left(k+\sqrt{k^2+4\lambda^2} \right)x }d\lambda +\int_{\forall \lambda} G(\lambda)e^{\lambda t +\frac12\left(k-\sqrt{k^2+4\lambda^2} \right)x }d\lambda $$
$F(\lambda)$ and $G(\lambda)$ are arbitrary functions to be determined according to some boundary conditions (not mentioned in the wording of the question).
In case of $k=0$ the general solution is the preceding equation which is reduced to :
$$P(x,t)=\int_{\forall \lambda} f(\lambda)e^{\lambda (t+x) }d\lambda + \int_{\forall \lambda} g(\lambda)e^{\lambda (t-x) }d\lambda$$
$f(\lambda)$ and $g(\lambda)$ are arbitrary functions to be determined according to some boundary conditions. There is no reason for $f=F$ and $g=G$.
Note that one can write equivalently
$$P(x,t)=\Phi(t+x)+\Gamma(t-x)$$
where $\Phi$ and $\Gamma$ are arbitrary functions.
The question raised by the OP is if whether or not a general relationship exist between $P(x,t)$ and $Q(x,t)$.
Since both $P(x,t)$ and $Q(x,t)$ depends from boundary conditions it is doubtful that such a relationship exists because they are an infinity of possible different boundary conditions.
Supposing that the question be less general, but raised for only a particular boundary condition common to the two PDEs, it is difficult to give a definitive answer without the particular boundary condition be specified.
APPROXIMATE SOLUTION for $k$ close to $0.$ :
$\lambda t +\frac12\left(k\pm\sqrt{k^2+4\lambda^2} \right)x \simeq\lambda t +\frac12\left(k\pm 2\lambda \right)x $
$$Q(x,t)\simeq\int_{\forall \lambda} F(\lambda)e^{\lambda t +\frac12\left(k+2\lambda \right)x }d\lambda +\int_{\forall \lambda} G(\lambda)e^{\lambda t +\frac12\left(k-2\lambda \right)x }d\lambda $$
$$Q(x,t)\simeq\int_{\forall \lambda} F(\lambda)e^{\lambda (t+x) +\frac{k}{2} x }d\lambda +\int_{\forall \lambda} G(\lambda)e^{\lambda (t-x) +\frac{k}{2}x }d\lambda $$
$$Q(x,t)\simeq e^{\frac{k}{2} x}\int_{\forall \lambda} F(\lambda)e^{\lambda (t+x) }d\lambda +e^{\frac{k}{2} x}\int_{\forall \lambda} G(\lambda)e^{\lambda (t-x)}d\lambda $$
$$Q(x,t)\simeq e^{\frac{k}{2} x}\big( \Phi(t+x)+\Gamma(t-x)\big)+\epsilon(x,t)\qquad k\:\:\text{small}$$
$$Q(x,t)\simeq e^{\frac{k}{2} x}P(x,t)+\epsilon(x,t)$$
The magnitude of the deviation $\epsilon(x,t)$ is proportional to $k^2$.


text:
\begin{document}

\title{Topological entropy of Bunimovich stadium billiards}

\author[M.~Misiurewicz]{Micha{\l}~Misiurewicz}

\address[Micha{\l}~Misiurewicz]
{Department of Mathematical Sciences\\ Indiana Univer\-sity-Purdue
University Indianapolis\\ 402 N. Blackford Street\\
Indianapolis, IN 46202\\ USA}
\email{mmisiure@math.iupui.edu}

\author[H.-K.~Zhang]{Hong-Kun~Zhang}

\address[Hong-Kun~Zhang]
{Department of Mathematics and Statistics\\ University of
Massachusetts\\ Amherst, MA 01003\\ USA}
\email{hongkun@math.umass.edu}

\subjclass[2010]{Primary 37D50, 37B40}

\keywords{Bunimovich stadium billiard, topological entropy}

\date{January 28, 2020}

\thanks{Research of Micha{\l} Misiurewicz was partially
supported by grant number 426602 from the Simons Foundation.}

\begin{abstract}
We estimate from below the topological entropy of the Bunimovich
stadium billiards. We do it for long billiard tables, and find the
limit of estimates as the length goes to infinity.
\end{abstract}

\maketitle

\section{Introduction}

In this paper, we consider Bunimovich stadium billiards. This was
the first type of billiards having convex (focusing) components of the
boundary $\partial \Omega$, yet enjoying the hyperbolic behavior
\cite{Bun74,Bun79}. Such boundary consists of two semicircles at the
ends, joined by segments of straight lines (see Figure~\ref{fig0}).
For those billiards, ergodicity, K-mixing and Bernoulli
property were proved in \cite{CT} for the natural measure.

\begin{figure}[h]
\begin{center}
\includegraphics[width=100truemm]{fig0.eps}
\caption{Bunimovich stadium.}\label{fig0}
\end{center}
\end{figure}

We consider billiard maps (not the flow) for two-dimensional billiard
tables. Thus, the phase space of a billiard is the product of the
boundary of the billiard table and the interval $[-\pi/2,\pi/2]$ of
angles of reflection. We will use the variables $(r,\varphi)$, where $r$
parametrizes the table boundary by the arc length, and $\varphi$ is the
angle of reflection. We mentioned the natural measure; it is
$c\cos\varphi\;dr\;d\varphi$, where $c$ is the normalizing constant. This
measure is invariant for the billiard map.

As we said, we want to study topological entropy of the billiard map.
This means that we should look at the billiard as a topological
dynamical system. However, existence of the natural measure resulted
in most authors looking at the billiard as a measure preserving
transformation. That is, all important properties of the billiard were
proved only almost everywhere, not everywhere. Additionally, the
billiard map is only piecewise continuous instead of continuous. Often
it is even not defined everywhere. All this creates problems already
at the level of definitions. We will discuss those problems in the
next section.

In view of this complicated situation, we will not try to produce a
comprehensive theory of the Bunimovich stadium billiards from the
topological point of view, but present the results on their
topological entropy that are independent of the approach. For this we
will find a subspace of the phase space that is compact and invariant,
and on which the billiard map is continuous. We will find the
topological entropy restricted to this subspace. This entropy is a
lower bound of the topological entropy of the full system, no matter
how this entropy is defined. Finally, we will find the limit of our
estimates as the length of the billiard table goes to infinity.

The reader who wants to learn more on other properties of the
Bunimovich stadium billiards, can find it in many papers, in
particular \cite{BC, BK, Bun74, Bun79, Ch, CM, HC}. While some of them
contain results about topological entropy of those billiards, none of
those results can be considered completely rigorous.

The paper is organized as follows. In Section~\ref{sec-teb} we discuss
the problems connected with defining topological entropy for
billiards. In Section~\ref{sec-sac} we produce symbolic systems
connected with the Bunimovich billiards. In Section~\ref{sec-cote} we
perform actual computations of the topological entropy.

\section{Topological entropy of billiards}\label{sec-teb}

Let $\cM=\partial\Omega\times[-\pi/2,\pi/2]$ be the phase space of a billiard
and let $\cF:\cM\to\cM$ be the billiard map. We assume that the
boundary of the billiard table is piecewise $C^2$ with finite number
of pieces. In such a situation the map $\cF$ is piecewise continuous
(in fact, piecewise smooth) with finitely many pieces. That is, $\cM$
is the union of finitely many open sets $\cM_i$ (of quite regular
shape) and a singular set $\cS$, which is the union of finitely many
smooth curves, and on which the map is often even not defined. The map
$\cF$ restricted to each $\cM_i$ is a diffeomorphism onto its image.

This situation is very similar as for piecewise continuous piecewise
monotone interval maps. For those maps, the usual way of investigating
them from the topological point of view is to use \emph{coding}. We
produce the \emph{symbolic system} associated with our map by taking
sequences of symbols (numbers enumerating pieces of continuity)
according to the number of the piece to which the $n$-th image of our
point belongs. On this symbolic space we have the shift to the left.
In particular, the topological entropy of this symbolic system was
shown to be equal to the usual Bowen's entropy of the underlying
interval map (see~\cite{MZ}).

Thus, it is a natural idea to do the same for billiards. Thus, for a
point $x\in\cM$, whose trajectory is disjoint from $\cS$, we take its
\emph{itinerary} (code) $\omega(x)=(\omega_n)$, where $\omega_n=i$ if
and only if
$\cF(x)\in\cM_i$. The problem is that the set of itineraries obtained
in such a way is usually not closed (in the product topology). Therefore
we have to take the closure of this set. Then the question one has to
deal with is whether there is no essential dynamics (for example,
invariant measures with positive entropy) on this extra set. A
rigorous approach for coding, including the definition of topological
entropy and a proof of a theorem analogous to the one from~\cite{MZ},
can be found in the recent paper of Baladi and Demers~\cite{BD} about
Sinai billiards.

The Sinai billiard maps are simpler for
coding than the Bunimovich stadium maps. There are finitely many
obstacles on the torus, so the pieces of the boundary, used for the
coding, are pairwise disjoint. This property is
not shared by the Bunimovich stadium billiards. The stadium billiard
is hyperbolic, but not uniformly. Moreover, here we have to
deal with the trajectories that are bouncing between the straight line
segments of the boundary. To complete the list of problems, the coding
with four pieces of the boundary seems to be not sufficient (as has
been noticed in~\cite{BK}).

The papers dealing with the topological entropy of Bunimovich stadium
billiards use different definitions. In~\cite{BK} and~\cite{HC},
topological entropy is explicitly definied as the exponential growth
rate of the number of
periodic orbits of a given period. In~\cite{Ch}, first coding is
performed in a different way, using rectangles defines by stable and
unstable manifolds. This coding uses an infinite alphabet. Then
various definitions of topological entropy for the obtained symbolic
system are used. In~\cite{BD}, topological entropy is defined as the
topological entropy of the corresponding symbolic system, that is, as
the exponential growth rate of the number of nonempty cylinders of a
given length in the symbolic system. As we
mentioned, it is shown that the result is the same as when one is
using the classical Bowen's definition for the original billiard map.
In~\cite{BC}, topological entropy is not formally defined, but it
seems that the authors think of the entropy of the symbolic system.

In this paper, we will be considering a subsystem of the full billiard
map. This subsystem is a continuous map of a compact space to itself,
and is conjugate to a subshift of finite type. Thus, whether we define
the topological entropy of the full system as the entropy of the
symbolic system or as the growth rate of the number of periodic orbit,
our estimates will be always lower bounds for the topological entropy.

\section{Subsystem and coding}\label{sec-sac}

We consider the Bunimovich stadium billiard table, with the radius of
the semicircles 1, and the lengths of straight segments $\ell>1$. The
phase space of this billiard map will be denoted by $\cM_\ell$, and
the map by $\cF_\ell$. The subspace of $\cM_\ell$ consisting of points
whose trajectories have no two consecutive collisions with the same
semicircle will be denoted by $\kl$. The subspace of $\kl$ consisting
of points whose trajectories have no $N+1$ consecutive collisions with
the straight segments will be denoted by $\kln$. We will show that if
$\ell>2N+2$, then the map $\cF_\ell$ restricted to $\kln$ has very
good properties.

In general, coding for $\cF_\ell$ needs at least six symbols. They
correspond to the four pieces of the boundary of the stadium, and
additionally on the semicircles we have to specify the orientation of
the trajectory
(whether $\varphi$ is positive or negative), see~\cite{BK}. However, in
$\kl$ this additional requirement is unnecessary, because there are no
multiple consecutive collisions with the same semicircle. This also
implies that in $\kl$ for a given $\ell$ the angle $\varphi$ is uniformly
bounded away from $\pm\pi/2$.

While in~\cite{BC} the statements about
generating partition are written in terms of measure preserving
transformations, the sets of measure zero that have to be removed are
specified. In $\kl$ the only set that needs to be removed is the set
of points whose trajectories are periodic of period 2, bouncing from
the two straight line segments. However, this set carries no
topological entropy, so we can ignore it. Thus, according
to~\cite{BC}, the symbolic system corresponding to $\cF_\ell$ on $\kl$
is a closed subshift $\Sigma_\ell$ of a subshift of finite type with 4
symbols. We say that there is a \emph{transition} from a state $i$ to
$j$ if it is possible that $\omega_n=i$ and $\omega_{n+1}=j$. In our
subshift here are some transitions that are forbidden: one cannot go
from a symbol corresponding to a semicircle to the same symbol. There
are of course also some transitions in many steps forbidden; they
depend on $\ell$.

For every element of $\Sigma_\ell$ there is a unique point of $\kl$
with that itinerary. However, the same point of $\kl$ may have more than one
itinerary, because there are four points on the boundary of the stadium
that belong to two pieces of the boundary each. Thus, the coding is
not one-to-one, but this is unavoidable if we want to obtain a compact
symbolic system. Another solution would be to remove codes of all
trajectories that pass through any of four special points, and at the
end take the closure of the symbolic space.

This problem disappears when we pass to $\kln$ with $\ell>2N+2$.
Namely, then the angle $\varphi$ at any point of $\kln$ whose first
coordinate is on the straight line piece, is larger than $\pi/4$ in
absolute value.

Let us look at the geometry of this situation. Let $C$ be the right
unit semicircle in $\IR^2$ (without endpoints), $A\in C$, and let
$L_1,L_2$ be half-lines emerging from $A$, reflecting from $C$ (like a
billiard flow trajectory) from inside at $A$ (see Figure~\ref{fig3}).
Assume that for $i=1,2$ the angles between $L_i$ and the horizontal
lines are less than $\pi/4$, and that $L_i$ intersects $C$ only at
$A$. Consider the argument $\arg(A)$ of $A$ (as in polar coordinates
on in the complex plane).

\begin{figure}[h]
\begin{center}
\includegraphics[width=40truemm]{fig3.eps}
\caption{Situation from Lemma~\ref{geom}.}\label{fig3}
\end{center}
\end{figure}

\begin{lemma}\label{geom}
In the above situation, $|\arg(A)|<\pi/4$. Moreover, neither $L_1$ nor
$L_2$ passes through an endpoint of $C$.
\end{lemma}

\begin{proof}
If $|\arg(A)|\ge\pi/4$, then both lines $L_1$ and $L_2$ are on the
same side of the origin, so the incidence and reflection angle cannot
be the same. Therefore, $|\arg(A)|<\pi/4$.

Suppose that $L_1$ passes through the lower endpoint of $C$ (the other
cases are similar). Then $\arg(A)<0$, so $L_2$ intersects the
semicircle also at the point with argument
\[
\arg(A)+(\arg(A)-(-\pi/2))=2\arg(A)+\pi/2,
\]
a contradiction.
\end{proof}

In view of the above lemma, the collision points on the semicircles
cannot be too close to the endpoints of the semicircles (including
endpoints themselves). Thus, the
correspondence between $\kln$ and its coding system $\Sigma_{\ell,N}$
is a bijection. Standard considerations of topologies in both systems
show that this bijection is a homeomorphism, say
$\xi_{\ell,N}:\kln\to\Sigma_{\ell,N}$. If $\sigma$ is the left shift
in the symbolic system, then by the construction we have
$\xi_{\ell,N}\circ\cF_\ell=\sigma\circ\xi_{\ell,N}$. In such a way we
get the following lemma.

\begin{lemma}\label{conj}
If $\ell>2N+2$ then the systems $(\kln,\cF_\ell)$ and
$(\Sigma_{\ell,N},\sigma)$ are topologically conjugate.
\end{lemma}

We can modify our codings, in order to simplify further proofs. The
first thing is to identify the symbols corresponding to two
semicircles. This can be done due to the symmetry, and will result in
producing symbolic systems $\Sigma'_\ell$ and $\Sigma'_{\ell,N}$,
which are 2-to-1 factors of $\Sigma_\ell$ and $\Sigma_{\ell,N}$
respectively. Since the operation of taking a 2-to-1 factor preserves
topological entropy, this will not affect our results.

With this simplification, $\Sigma'_\ell$ is a closed, shift-invariant
subset of the phase space of a subshift of finite type $\ws$. Subshift
of finite type $\ws$ looks as follows. There are three states, $0,A,B$
(where 0 corresponds to the semicircles), and the only forbidden
transitions are from $A$ to $A$ and from $B$ to $B$.

Then $\Sigma'_{\ell,N}$ is a closed, shift-invariant subset of
$\Sigma'_\ell$, where additionally $n$-step transitions involving only
states $A$ and $B$ are forbidden if $n>N$. However, it pays to recode
$\Sigma'_{\ell,N}$. Namely, we replace states $A$ and $B$ by
$1,2,\dots,N$ and $-1,-2,\dots,-N$ respectively. If
$(\omega_n)\in\Sigma'_{\ell,N}$, and $\omega_k=\omega_{k+m+1}=0$, while
$\omega_n\in\{A,B\}$ for $n=k+1,k+2,\dots,k+m$, then for the recoded
sequence $(\rho_n)$ we have $\rho_k=\rho_{k+m+1}=0$ and
$(\rho_{k+1},\rho_{k+2}\dots,\rho_{k+m})$ is equal to $(1,2,\dots,m)$
if $\omega_{k+1}=A$ and $(-1,-2,\dots,-m)$ if $\omega_{k+1}=B$.

Geometric meaning of the recoding is simple. We unfold the
stadium by using reflections from the straight parts (see
Figure~\ref{fig1}). We will label the levels of the semicircles by
integers.
\begin{figure}[h]
\begin{center}
\includegraphics[width=100truemm]{fig1.eps}
\caption{Unfolded stadium.}\label{fig1}
\end{center}
\end{figure}
Our new coding translates to this picture as follows. We start at a
semicircle, then go to a semicircle on the other side and $m$ levels
up or down, etc.

For symbolic systems, recoding in such a way amounts to the
topological conjugacy of the original and recoded systems (see~\cite{K}).
This means that the system $(\Sigma'_{\ell,N},\sigma)$ is
topologically conjugate to a subsystem of $\ws_N$, which is the
subshift of finite type defined as follows. The states are
$-N,-N+1,\dots,N-1,N$, and the transitions are: from 0 to every state,
from $i$ to $i+1$ and 0 if $1\le i\le N-1$, from $N$ to 0, from $-i$
to $-i-1$ and 0 if $1\le i\le N-1$, and from $-N$ to 0.

\begin{lemma}\label{level-c}
If $\ell>2N+2$ then $(\Sigma'_{\ell,N},\sigma)$ is topologically
conjugate to $(\ws_N,\sigma)$.
\end{lemma}

\begin{proof}
Both sets $\Sigma'_{\ell,N}$ and $\ws_N$ are closed and
$\Sigma'_{\ell,N}\subset\ws_N$. Therefore, it is enough to prove that
$\Sigma'_{\ell,N}$ is dense in $\ws_N$. For this we show that for
every sequence $(\rho_0,\rho_1,\dots,\rho_k)$ appearing as a block in
an element of $\ws_N$ there is a point $(r_0,\varphi_0)\in\kln$ for which
after coding and recoding a piece of trajectory of length $k+1$, we
get $(\rho_0,\rho_1,\dots,\rho_k)$. By taking a longer sequence, we
may assume that $\rho_0=\rho_k=0$.

Consider all candidates for such trajectories in the unfolded stadium,
when we do not care whether the incidence and reflection angles are
equal. That is, we consider all curves that are unions of straight
line segments from $x_0$ to $x_1$ to $x_2$ $\dots$ to $x_k$ in the
unfolded stadium, such that $x_0$ is in the left semicircle at level
0, $x_1$ is in the right semicircle at level $n_1$, $x_2$ is in the
left semicircle at level $n_1+n_2$, etc. Here $n_1,n_2,\dots$ are the
numbers of non-zero elements of the sequence
$(\rho_0,\rho_1,\dots,\rho_k)$ between a zero element and the next
zero element, where we also take into account the signs of those
non-zero elements. In other words, this curve is an approximate
trajectory (of the flow) in the unfolded stadium that would have the
recoded itinerary $(\rho_0,\rho_1,\dots,\rho_k)$. Additionally we require that
$x_0$ and $x_k$ are at the midpoints of their semicircles. The class
of such curves is a compact space with the natural topology, so there
is the longest curve in this class. We claim that this curve is a
piece of the flow trajectory corresponding to the trajectory we are
looking for.

If we look at the ellipse with foci at $x_i$ and $x_{i+2}$ to which
$x_{i+1}$ belongs, then $x_{i+1}$ has to be a point of tangency of
that elipse and the semicircle. Since for the ellipse the angles of
incidence and reflection are equal, the same is true for the
semicircle.

Now we have to prove three properties of our curve. The first one is that
any small movement of one of the points $x_1,\dots,x_{m-1}$ gives us a
shorter curve. The second one is that none of those points lies at an
endpoint of a semicircle. The third one is that none of the segments
of the curve intersects any semicircle at any other point.

The first property follows from the fact that any ellipse with foci on
the union of the left semicircles at levels $-N$ through $N$, which is
tangent to any right semicircle, is tangent from outside. This is
equivalent to the fact that the maximal curvature of such ellipse is
smaller than the curvature of the semicircles (which is 1). The
distance between the foci of our ellipse is not larger than $2(2N+1)$,
and the length of the large semi-axis is larger than $\ell$.
Elementary computations show that the maximal curvature of such
ellipse is smaller than $\frac{\ell}{\ell^2-(2N+1)^2}$. Thus, this
property is satisfied if $\ell^2-\ell>(2N+1)^2$. However, by the
assumption, $\ell^2-\ell=\ell(\ell-1)\ge(2N+2)(2N+1)>(2N+1)^2$.

The second property is clearly satisfied, because if $x_i$ lies at an
endpoint of a semicircle, then an infinitesimally small movement of
this point along the semicircle would result in both straight segments
of the curve that end/begin at $x_i$ to get longer.

The third property follows from the observation that if $\ell\ge 2N+2$
then the angles between the segments of our curve and the straight
parts of the billiard table boundary are smaller than $\pi/4$. Suppose
that the segment from $x_i$ to $x_{i+1}$ intersects the semicircle $C$
to which $x_{i+1}$ belongs at some other point $y$ (see
Figure~\ref{fig2}). Then $x_{i+1}$ and $y$ belong to the same half of
$C$. By the argument with the ellipses, at $x_{i+1}$ the incidence and
reflection angles of our curve are equal. Therefore, the segment from
$x_{i+1}$ to $x_{i+2}$ also intersects $C$ at some other point, so
$x_{i+1}$ should belong to the other half of $C$, a contradiction.
This completes the proof.
\end{proof}

\begin{figure}[h]
\begin{center}
\includegraphics[width=40truemm]{fig2.eps}
\caption{Two intersections.}\label{fig2}
\end{center}
\end{figure}

\begin{remark}\label{Markov}
By Lemmas~\ref{conj} and~\ref{level-c} (plus the way we obtained
$\Sigma'_{\ell,N}$ from $\Sigma_{\ell,N}$) it follows that if
$\ell>2N+2$ then the natural partition of $\kln$ into four sets is a
Markov partition.
\end{remark}

\section{Computation of topological entropy}\label{sec-cote}

In the preceding section we obtained some subshifts of finite type. Now
we have to compute their topological entropies. If the alphabet
of a subshift of finite type is $\{1,2,\dots,k\}$, then we
can write the \emph{transition matrix} $M=(m_{ij})_{i,j=1}^n$, where
$m_{ij}=1$ if there is a transition from $i$ to $j$ and $m_{ij}=0$
otherwise. Then the topological entropy of our subshift is the
logarithm of the spectral radius of $M$ (see~\cite{K, ALM}).

\begin{lemma}\label{ent-kl}
Topological entropy of the system $(\Sigma_\ell',\sigma)$ is
$\log(1+\sqrt2)$.
\end{lemma}

\begin{proof}
The transition matrix of $(\Sigma_\ell',\sigma)$ is
\[
\begin{bmatrix}
  1&1&1\\
  1&1&0\\
  1&0&1\\
\end{bmatrix}.
\]
The characteristic polynomial of this matrix is $(1-x)(x^2-2x-1)$, so
the entropy is $\log(1+\sqrt2)$.
\end{proof}

In the case of larger, but not too complicated, matrices, in order to
compute the spectral radius one can use the \emph{rome method}
(see~\cite{BGMY, ALM}). For the transition matrices of $\ws_N$ this
method is especially simple. Namely, if we look at the paths given by
transitions, we see that 0 is a rome: all paths lead to it. Then we
only have to identify the lengths of all paths from 0 to 0 that do not
go through 0 except at the beginning and the end. The spectral radius
of the transition matrix is then the largest zero of the function
$\sum x^{-p_i}-1$, where the sum is over all such paths and $p_i$ is
the length if the $i$-th path.

\begin{lemma}\label{ent-kln}
Topological entropy of the system $(\ws_N,\sigma)$ is the logarithm of
the largest root of the equation
\begin{equation}\label{eq0}
(x^2-2x-1)=-2x^{1-N}.
\end{equation}
\end{lemma}

\begin{proof}
The paths that we mentioned before the lemma, are: one path of length
1 (from 0 directly to itself), and two paths of length $2,3,\dots,N$
each. Therefore, our entropy is the logarithm of the largest zero of
the function $2(x^{-N}+\dots+x^{-3}+x^{-2})+x^{-1}-1$. We have
\[
x(1-x)\big(2(x^{-N}+\dots +x^{-3}+x^{-2})+x^{-1}-1\big)=
(x^2-2x-1)+2x^{1-N},
\]
so our entropy is the logarithm of the largest root of
equation~\eqref{eq0}.
\end{proof}

Now that we computed topological entropies of the subshifts of
finite type involved, we have to go back to the definition of the
topological entropy of billiards (and their subsystems). As we
mentioned earlier, the most popular definitions either employ the
symbolic systems or use the growth rate of the number of periodic
orbits of the given period. For subshifts of finite type that does not
make difference, because the exponential growth rate of the number of
periodic orbits of a given period is the same as the topological
entropy (if the systems are topologically mixing, which is the case
here). As the first step, we get the following result, that follows
immediately from Lemmas~\ref{conj}, \ref{level-c} and~\ref{ent-kln}.

\begin{theorem}\label{t-ent-kln}
If $\ell>2N+2$ then topological entropy of the system
$(\kln,\cF_\ell)$ is the logarithm of the largest root of the
equation~\eqref{eq0}.
\end{theorem}

Now, independently of which definition of the entropy $h(\fkl)$ of
$(\kl,\cF_\ell)$ we choose, we get the next theorem.

\begin{theorem}\label{main}
We have
\begin{equation}\label{eq1}
\liminf_{\ell\to\infty}h(\fkl)\ge 1+\sqrt2.
\end{equation}
\end{theorem}

\begin{proof}
On one hand, $\kln$ is a subset of $\kl$, so $h(\fkl)\ge h(\fkln)$ for
every $N$. Therefore, by Theorem~\ref{t-ent-kln},
\[
\liminf_{\ell\to\infty}h(\fkl)\ge\lim_{N\to\infty}\log y_N,
\]
where $y_N$ is the largest root of the equation~\eqref{eq0}. The
largest root of $x^2-2x-1=0$ is $1+\sqrt2$. In its neighborhood the
right-hand side of~\eqref{eq0} goes uniformly to 0 as $N\to\infty$.
Thus, $\lim_{N\to\infty}y_N=1+\sqrt2$, so we get~\eqref{eq1}.
\end{proof}

If we choose the definition of the entropy via the entropy of the
corresponding symbolic system, then, taking into account
Lemma~\ref{ent-kl}, we get a stronger theorem.

\begin{theorem}\label{main1}
We have
\begin{equation}\label{eq2}
\lim_{\ell\to\infty}h(\fkl)=1+\sqrt2.
\end{equation}
\end{theorem}

Of course, the same lower estimates hold for the whole billiard.

config: arxiv