TITLE: Estimate $\int^1_0 e^{-x^2}\, dx$
QUESTION [2 upvotes]: Estimate $\int^1_0 e^{-x^2}\, dx$
This is in a section on Taylor series so I would assume that is how it should be solved.
I started by using the Taylor series formula for $e^x$ replacing $x$ with $x^2$. I ended up with this:
$1+(-x^2)+\frac{(-x^2)^2}{2!}+\frac{(-x^2)^3}{3!}+\frac{(-x^2)^4}{4!}+...$
It looks to me like from here I should get some Fundamental Theorem of Calculus going, but I'm not sure how. The integral evaluated at $0$ is just $1$, however the integral evaluated at $1$ is not so easy. Is there some summation formula that would apply here that I could use?

REPLY [2 votes]: Use the standard normal distribution table.
Consider $$\frac{1}{\sqrt{2π}}\int e^{-x^2/2}\,dx$$
Let $u=\frac{x}{\sqrt{2}}$. Then $\frac{du}{dx}=\frac{1}{\sqrt{2}}$.
Then $$\frac{1}{\sqrt{2π}}\int e^{-x^2/2}\,dx=\frac{1}{\sqrt{2π}}\int e^{-u^2}\,\sqrt{2}du=\frac{1}{\sqrt{π}}\int e^{-u^2}\,du$$
So
$$\frac{1}{\sqrt{π}}\int_{0}^1 e^{-u^2}\,du=\frac{1}{\sqrt{2π}}\int_{0}^\sqrt{2} e^{-x^2/2}\,dx$$
$$\int_{0}^1 e^{-u^2}\,du=\sqrt{π}*\frac{1}{\sqrt{2π}}\int_{0}^\sqrt{2} e^{-x^2/2}\,dx\approx\sqrt{π}*0.4207\approx0.7457$$


text:
/-
Copyright (c) 2019 Reid Barton. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Reid Barton, Johan Commelin
-/
import category_theory.adjunction.basic
import category_theory.limits.creates

/-!
# Adjunctions and limits

A left adjoint preserves colimits (`category_theory.adjunction.left_adjoint_preserves_colimits`),
and a right adjoint preserves limits (`category_theory.adjunction.right_adjoint_preserves_limits`).

Equivalences create and reflect (co)limits.
(`category_theory.adjunction.is_equivalence_creates_limits`,
`category_theory.adjunction.is_equivalence_creates_colimits`,
`category_theory.adjunction.is_equivalence_reflects_limits`,
`category_theory.adjunction.is_equivalence_reflects_colimits`,)

In `category_theory.adjunction.cocones_iso` we show that
when `F ⊣ G`,
the functor associating to each `Y` the cocones over `K ⋙ F` with cone point `Y`
is naturally isomorphic to
the functor associating to each `Y` the cocones over `K` with cone point `G.obj Y`.
-/

open opposite

namespace category_theory.adjunction
open category_theory
open category_theory.functor
open category_theory.limits

universes v u v₁ v₂ v₀ u₁ u₂

section arbitrary_universe

variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]

variables {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
include adj

section preservation_colimits
variables {J : Type u} [category.{v} J] (K : J ⥤ C)

/--
The right adjoint of `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)`.

Auxiliary definition for `functoriality_is_left_adjoint`.
-/
def functoriality_right_adjoint : cocone (K ⋙ F) ⥤ cocone K :=
(cocones.functoriality _ G) ⋙
  (cocones.precompose (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv))

local attribute [reducible] functoriality_right_adjoint

/--
The unit for the adjunction for `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)`.

Auxiliary definition for `functoriality_is_left_adjoint`.
-/
@[simps] def functoriality_unit :
  𝟭 (cocone K) ⟶ cocones.functoriality _ F ⋙ functoriality_right_adjoint adj K :=
{ app := λ c, { hom := adj.unit.app c.X } }

/--
The counit for the adjunction for `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)`.

Auxiliary definition for `functoriality_is_left_adjoint`.
-/
@[simps] def functoriality_counit :
  functoriality_right_adjoint adj K ⋙ cocones.functoriality _ F ⟶ 𝟭 (cocone (K ⋙ F)) :=
{ app := λ c, { hom := adj.counit.app c.X } }

/-- The functor `cocones.functoriality K F : cocone K ⥤ cocone (K ⋙ F)` is a left adjoint. -/
def functoriality_is_left_adjoint :
  is_left_adjoint (cocones.functoriality K F) :=
{ right := functoriality_right_adjoint adj K,
  adj := mk_of_unit_counit
  { unit := functoriality_unit adj K,
    counit := functoriality_counit adj K } }

/--
A left adjoint preserves colimits.

See <https://stacks.math.columbia.edu/tag/0038>.
-/
def left_adjoint_preserves_colimits : preserves_colimits_of_size.{v u} F :=
{ preserves_colimits_of_shape := λ J 𝒥,
  { preserves_colimit := λ F,
    by exactI
    { preserves := λ c hc, is_colimit.iso_unique_cocone_morphism.inv
        (λ s, @equiv.unique _ _ (is_colimit.iso_unique_cocone_morphism.hom hc _)
          (((adj.functoriality_is_left_adjoint _).adj).hom_equiv _ _)) } } }.

omit adj

@[priority 100] -- see Note [lower instance priority]
instance is_equivalence_preserves_colimits (E : C ⥤ D) [is_equivalence E] :
  preserves_colimits_of_size.{v u} E :=
left_adjoint_preserves_colimits E.adjunction

@[priority 100] -- see Note [lower instance priority]
instance is_equivalence_reflects_colimits (E : D ⥤ C) [is_equivalence E] :
  reflects_colimits_of_size.{v u} E :=
{ reflects_colimits_of_shape := λ J 𝒥, by exactI
  { reflects_colimit := λ K,
    { reflects := λ c t,
      begin
        have l := (is_colimit_of_preserves E.inv t).map_cocone_equiv E.as_equivalence.unit_iso.symm,
        refine (((is_colimit.precompose_inv_equiv K.right_unitor _).symm) l).of_iso_colimit _,
        tidy,
      end } } }

@[priority 100] -- see Note [lower instance priority]
instance is_equivalence_creates_colimits (H : D ⥤ C) [is_equivalence H] :
  creates_colimits_of_size.{v u} H :=
{ creates_colimits_of_shape := λ J 𝒥, by exactI
  { creates_colimit := λ F,
    { lifts := λ c t,
      { lifted_cocone := H.map_cocone_inv c,
        valid_lift := H.map_cocone_map_cocone_inv c } } } }

-- verify the preserve_colimits instance works as expected:
example (E : C ⥤ D) [is_equivalence E]
  (c : cocone K) (h : is_colimit c) : is_colimit (E.map_cocone c) :=
preserves_colimit.preserves h

lemma has_colimit_comp_equivalence (E : C ⥤ D) [is_equivalence E] [has_colimit K] :
  has_colimit (K ⋙ E) :=
has_colimit.mk
{ cocone := E.map_cocone (colimit.cocone K),
  is_colimit := preserves_colimit.preserves (colimit.is_colimit K) }

lemma has_colimit_of_comp_equivalence (E : C ⥤ D) [is_equivalence E] [has_colimit (K ⋙ E)] :
  has_colimit K :=
@has_colimit_of_iso _ _ _ _ (K ⋙ E ⋙ inv E) K
(@has_colimit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _)
((functor.right_unitor _).symm ≪≫ iso_whisker_left K (E.as_equivalence.unit_iso))

/-- Transport a `has_colimits_of_shape` instance across an equivalence. -/
lemma has_colimits_of_shape_of_equivalence (E : C ⥤ D) [is_equivalence E]
  [has_colimits_of_shape J D] : has_colimits_of_shape J C :=
⟨λ F, by exactI has_colimit_of_comp_equivalence F E⟩

/-- Transport a `has_colimits` instance across an equivalence. -/
lemma has_colimits_of_equivalence (E : C ⥤ D) [is_equivalence E] [has_colimits_of_size.{v u} D] :
  has_colimits_of_size.{v u} C :=
⟨λ J hJ, by { exactI has_colimits_of_shape_of_equivalence E }⟩

end preservation_colimits

section preservation_limits
variables {J : Type u} [category.{v} J] (K : J ⥤ D)

/--
The left adjoint of `cones.functoriality K G : cone K ⥤ cone (K ⋙ G)`.

Auxiliary definition for `functoriality_is_right_adjoint`.
-/
def functoriality_left_adjoint : cone (K ⋙ G) ⥤ cone K :=
(cones.functoriality _ F) ⋙ (cones.postcompose
    ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom))

local attribute [reducible] functoriality_left_adjoint

/--
The unit for the adjunction for`cones.functoriality K G : cone K ⥤ cone (K ⋙ G)`.

Auxiliary definition for `functoriality_is_right_adjoint`.
-/
@[simps] def functoriality_unit' :
  𝟭 (cone (K ⋙ G)) ⟶ functoriality_left_adjoint adj K ⋙ cones.functoriality _ G :=
{ app := λ c, { hom := adj.unit.app c.X, } }

/--
The counit for the adjunction for`cones.functoriality K G : cone K ⥤ cone (K ⋙ G)`.

Auxiliary definition for `functoriality_is_right_adjoint`.
-/
@[simps] def functoriality_counit' :
  cones.functoriality _ G ⋙ functoriality_left_adjoint adj K ⟶ 𝟭 (cone K) :=
{ app := λ c, { hom := adj.counit.app c.X, } }

/-- The functor `cones.functoriality K G : cone K ⥤ cone (K ⋙ G)` is a right adjoint. -/
def functoriality_is_right_adjoint :
  is_right_adjoint (cones.functoriality K G) :=
{ left := functoriality_left_adjoint adj K,
  adj := mk_of_unit_counit
  { unit := functoriality_unit' adj K,
    counit := functoriality_counit' adj K } }

/--
A right adjoint preserves limits.

See <https://stacks.math.columbia.edu/tag/0038>.
-/
def right_adjoint_preserves_limits : preserves_limits_of_size.{v u} G :=
{ preserves_limits_of_shape := λ J 𝒥,
  { preserves_limit := λ K,
    by exactI
    { preserves := λ c hc, is_limit.iso_unique_cone_morphism.inv
        (λ s, @equiv.unique _ _ (is_limit.iso_unique_cone_morphism.hom hc _)
          (((adj.functoriality_is_right_adjoint _).adj).hom_equiv _ _).symm) } } }.

omit adj

@[priority 100] -- see Note [lower instance priority]
instance is_equivalence_preserves_limits (E : D ⥤ C) [is_equivalence E] :
  preserves_limits_of_size.{v u} E :=
right_adjoint_preserves_limits E.inv.adjunction

@[priority 100] -- see Note [lower instance priority]
instance is_equivalence_reflects_limits (E : D ⥤ C) [is_equivalence E] :
  reflects_limits_of_size.{v u} E :=
{ reflects_limits_of_shape := λ J 𝒥, by exactI
  { reflects_limit := λ K,
    { reflects := λ c t,
      begin
        have := (is_limit_of_preserves E.inv t).map_cone_equiv E.as_equivalence.unit_iso.symm,
        refine (((is_limit.postcompose_hom_equiv K.left_unitor _).symm) this).of_iso_limit _,
        tidy,
      end } } }

@[priority 100] -- see Note [lower instance priority]
instance is_equivalence_creates_limits (H : D ⥤ C) [is_equivalence H] :
  creates_limits_of_size.{v u} H :=
{ creates_limits_of_shape := λ J 𝒥, by exactI
  { creates_limit := λ F,
    { lifts := λ c t,
      { lifted_cone := H.map_cone_inv c,
        valid_lift := H.map_cone_map_cone_inv c } } } }

-- verify the preserve_limits instance works as expected:
example (E : D ⥤ C) [is_equivalence E]
  (c : cone K) [h : is_limit c] : is_limit (E.map_cone c) :=
preserves_limit.preserves h

lemma has_limit_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit K] :
  has_limit (K ⋙ E) :=
has_limit.mk
{ cone := E.map_cone (limit.cone K),
  is_limit := preserves_limit.preserves (limit.is_limit K) }

lemma has_limit_of_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit (K ⋙ E)] :
  has_limit K :=
@has_limit_of_iso _ _ _ _ (K ⋙ E ⋙ inv E) K
(@has_limit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _)
((iso_whisker_left K E.as_equivalence.unit_iso.symm) ≪≫ (functor.right_unitor _))

/-- Transport a `has_limits_of_shape` instance across an equivalence. -/
lemma has_limits_of_shape_of_equivalence (E : D ⥤ C) [is_equivalence E] [has_limits_of_shape J C] :
  has_limits_of_shape J D :=
⟨λ F, by exactI has_limit_of_comp_equivalence F E⟩

/-- Transport a `has_limits` instance across an equivalence. -/
lemma has_limits_of_equivalence (E : D ⥤ C) [is_equivalence E] [has_limits_of_size.{v u} C] :
  has_limits_of_size.{v u} D :=
⟨λ J hJ, by exactI has_limits_of_shape_of_equivalence E⟩

end preservation_limits

/-- auxiliary construction for `cocones_iso` -/
@[simps]
def cocones_iso_component_hom {J : Type u} [category.{v} J] {K : J ⥤ C}
  (Y : D) (t : ((cocones J D).obj (op (K ⋙ F))).obj Y) :
  (G ⋙ (cocones J C).obj (op K)).obj Y :=
{ app := λ j, (adj.hom_equiv (K.obj j) Y) (t.app j),
  naturality' := λ j j' f, by { erw [← adj.hom_equiv_naturality_left, t.naturality], dsimp, simp } }

/-- auxiliary construction for `cocones_iso` -/
@[simps]
def cocones_iso_component_inv {J : Type u} [category.{v} J] {K : J ⥤ C}
  (Y : D) (t : (G ⋙ (cocones J C).obj (op K)).obj Y) :
  ((cocones J D).obj (op (K ⋙ F))).obj Y :=
{ app := λ j, (adj.hom_equiv (K.obj j) Y).symm (t.app j),
  naturality' := λ j j' f,
  begin
    erw [← adj.hom_equiv_naturality_left_symm, ← adj.hom_equiv_naturality_right_symm, t.naturality],
    dsimp, simp
  end }

/-- auxiliary construction for `cones_iso` -/
@[simps]
def cones_iso_component_hom {J : Type u} [category.{v} J] {K : J ⥤ D}
  (X : Cᵒᵖ) (t : (functor.op F ⋙ (cones J D).obj K).obj X) :
  ((cones J C).obj (K ⋙ G)).obj X :=
{ app := λ j, (adj.hom_equiv (unop X) (K.obj j)) (t.app j),
  naturality' := λ j j' f,
  begin
    erw [← adj.hom_equiv_naturality_right, ← t.naturality, category.id_comp, category.id_comp],
    refl
  end }

/-- auxiliary construction for `cones_iso` -/
@[simps]
def cones_iso_component_inv {J : Type u} [category.{v} J] {K : J ⥤ D}
  (X : Cᵒᵖ) (t : ((cones J C).obj (K ⋙ G)).obj X) :
  (functor.op F ⋙ (cones J D).obj K).obj X :=
{ app := λ j, (adj.hom_equiv (unop X) (K.obj j)).symm (t.app j),
  naturality' := λ j j' f,
  begin
    erw [← adj.hom_equiv_naturality_right_symm, ← t.naturality, category.id_comp, category.id_comp]
  end }

end arbitrary_universe

variables {C : Type u₁} [category.{v₀} C] {D : Type u₂} [category.{v₀} D]
{F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)

/--
When `F ⊣ G`,
the functor associating to each `Y` the cocones over `K ⋙ F` with cone point `Y`
is naturally isomorphic to
the functor associating to each `Y` the cocones over `K` with cone point `G.obj Y`.
-/
-- Note: this is natural in K, but we do not yet have the tools to formulate that.
def cocones_iso {J : Type u} [category.{v} J] {K : J ⥤ C} :
  (cocones J D).obj (op (K ⋙ F)) ≅ G ⋙ (cocones J C).obj (op K) :=
nat_iso.of_components (λ Y,
{ hom := cocones_iso_component_hom adj Y,
  inv := cocones_iso_component_inv adj Y, })
(by tidy)

-- Note: this is natural in K, but we do not yet have the tools to formulate that.
/--
When `F ⊣ G`,
the functor associating to each `X` the cones over `K` with cone point `F.op.obj X`
is naturally isomorphic to
the functor associating to each `X` the cones over `K ⋙ G` with cone point `X`.
-/
def cones_iso {J : Type u} [category.{v} J] {K : J ⥤ D} :
  F.op ⋙ (cones J D).obj K ≅ (cones J C).obj (K ⋙ G) :=
nat_iso.of_components (λ X,
{ hom := cones_iso_component_hom adj X,
  inv := cones_iso_component_inv adj X, } )
(by tidy)

end category_theory.adjunction

subset_name: curated


TITLE: Simplifying using algebraic operations
QUESTION [0 upvotes]: I came across this question while doing homework out of the Philips Exeter Academy Mathematics 1 textbook, and do not usderstand what to do.
Here is the question:
"In each of the following, use appropriate algebraic operations to remove the parentheses and combine like terms. Leave your answers in simple form.
(a) x(2x)+2(x+5)  (b) 2x(5x-2)+3(6x+7)  (c)  5m(3m-2n)+4n(3m-2n) "
I'm having ahard time understanding what the question means getting rid of the parentheses by using "algebraic operations", and I tried doing the multiplication, but I couldn't get rid of the parentheses successfully.
Could someone please walk me through and help me understand this problem?
Thanks

REPLY [0 votes]: HINTS
$x(2x)=x*(2*x)=x*2*x=2*x*x=2x^2$
Does this make sense? Can you see why it holds?
Now for combining like terms:
$2x^2+2x+3y^3-6y=2x(x+1)+3y(y^2-2)$
where we have the $"x"$s and $"y"$s neatly packaged in two instead of four terms.
This is just an example of applying the basic properties:
Commutative, Associative and Distributive.


TITLE: The Norm Map in (group) cohomology via classifying spaces
QUESTION [7 upvotes]: The well-known transfer map in group (co)homology can be defined with only homological algebra, or with algebraic topology via classifying spaces (group cohomology of $G$ is isomorphic to ordinary cohomology of $BG$).  Here I fix a group $G$ with finite-index subgroup $H$, and field $k=\mathbb{Z}_p$. Let $p:\tilde{Y}\rightarrow Y$ be a covering map, where $Y$ is a $K(G,1)$-manifold of top dimension $n$ and $\tilde{Y}$ is the cover which corresponds to $H$ (so that it is a $K(H,1)$-manifold); clearly $p$ is a $|G:H|$-sheeted covering map.  Now the transfer map $tr^G_H:H_n(G,k)\rightarrow H_n(H,k)$ agrees with the transfer map $H_n(Y;k)\rightarrow H_n(\tilde{Y};k)$, which in terms of chain complexes is induced by $\sigma\mapsto\sum_{\sigma'}\sigma'$ where $\sigma$ is an oriented $n$-cell of $Y$ and $\sigma'$ ranges over the oriented $n$-cells of $\tilde{Y}$ lying over $\sigma$.  In cohomology this is $f\mapsto[\sigma\mapsto \sum_{\sigma'}f(\sigma')]$ for cochains. Likewise, the restriction map runs in the opposite direction of the transfer and is induced from the map $BH=EG/H\rightarrow EG/G=BG$.
What is the corresponding classifying space construction in the setting of the norm map defined below?
Let $S_{G/H}$ be the group of permutations of $G/H$ (left coset representatives) and consider $H$ as a subgroup of $S_H$ through left multiplication.  The wreath product $S_{G/H}\int H$ is $H^{\oplus|G:H|}\rtimes S_{G/H}$, where $s^{-1}(\prod_{x\in G/H}h_x)s=\prod_{x\in G/H}h_{s(x)}$.  From this is the monomial representation $\Phi:G\rightarrow S_{G/H}\int H$ defined by $\Phi(g)=\pi(g)\prod_{x\in G/H}h_{g,t}$ where $gx=x_gh_{g,t}$ (for $x,x_g\in G/H$ and $h_{g,t}\in H$), and $x\mapsto x_g$ induces a permutation $\pi(g)\in S_{G/H}$ (so $\pi$ is the representation of $G$ as a group of permutations of its left coset space $G/H$).
Finally, for $\alpha\in H^*(H,k)$ of even degree, the norm map $\mathcal{N}^G_H:H^{even}(H,k)\rightarrow H^*(G,k)$ is defined by $\mathcal{N}^G_H(\alpha)=\Phi^*(1\int \alpha)$; for convenience I left out the cohomological construction of the element $1\int\alpha$ from $\alpha$.  If $\alpha\in H^n(H,k)$ then $\mathcal{N}^G_H(\alpha)\in H^{n|G:H|}(G,k)$.  This is a pretty hard construction for me to grasp, but ultimately it is extremely useful in group cohomology (in particular, it was defined by Leonard Evens and used to prove the finite generation result that $H^*(G,\mathbb{Z}_p)$ is Noetherian for any $p$ dividing $|G|$).
The reason this question arose is because $\mathcal{N}^G_H(1+\alpha)=1+tr^G_H(\alpha)+\cdots+\mathcal{N}^G_H(\alpha)$ for $\alpha\in H^n(H,k)$, where the intermediate terms are also transfers, i.e. the norm map is intertwined with the transfer map.  Even simpler, $\mathcal{N}^G_H(\alpha+\beta)=\mathcal{N}^G_H(\alpha)+tr^G_H(\mu)+\mathcal{N}^G_H(\beta)$ for some $\mu\in H^*(H,k)$, if $H$ is an index-$p$ normal subgroup ($\alpha,\beta$ are homogeneous elements of even degree).
[[Addendum]] I have actually just stumbled upon a piece of this desired construction, on pg73-75 of Adem & Milgram's Cohomology of Finite Groups. The map given here is $BG\rightarrow (BH)^{|G:H|}\times_{S_{G/H}}ES_{G/H}\simeq B(S_{G/H}\int H)$ and is induced from $\Phi$.  I assume from here we can functorially relate cohomology classes of $H$ to that of $S_{G/H}\int H$ and hence obtain $\mathcal{N}^G_H$.

REPLY [4 votes]: The easiest starting point for equivariant stable homotopy theory is probably the paper
with that title in The Handbook of Algebraic Topology, edited by I.M. James.  The paper
modern foundations for stable homotopy theory in the same volume is one of several possible
starting points for spectrum level stuff.


TITLE: Real rings with a zero divisor
QUESTION [1 upvotes]: Let $A$ be a commutative ring with identity. We say that $A$ is a real ring if every sum of squares of non-zero elements of $A$ is not zero. It is well-known that if $A$ is a real ring and an integral domain, then the quotient field of $A$ is an orderable field. My question:
Give an example of a real ring which is not integral domain.

REPLY [4 votes]: Just take a direct product of real rings, for example $\Bbb Z\times\Bbb Z$.


TITLE: A problem regarding the intersection of a cylinder and a line
QUESTION [1 upvotes]: Let $N,S$ be the poles of $S^2$. If $C$ is the cylinder with base $x^2+y^2=1$ we define $f:S^2\{N,C\}\to C$ by $f(p)=\vec{op}\cap C$ being $\vec{op}$ the ray from $(0,0,0)$ directed at $p$. Prove that $f$ is a diffeomorphism and show that $f$ transforms parallels in circumferences and meridians in straight lines.

My first idea was to find a better way to write $f$ because $\vec{op}\cap C$ doesn't look too handy. Working with the cartesian equation for the cylinder and  the parametric equations for the line seems that I have to find the intersection between $x^2+y^1=1$ and the line given by $\{x=tp_x,y=tp_y,z=tp_z\}$, follows that $t^2p_x^2+t^2p_y^2=1$ which implies $t=\frac{1}{\sqrt{p_x^2+p_y^2}}$ (I'm only considering the $+$ value of $t$ because I'm using the ray $\vec{op}$ so I only care about the upper intersection). Follows that $f$ could be defined by $f(p)=\left(\frac{p_x}{\sqrt{p_x^2+p_y^2}},\frac{p_y}{\sqrt{p_x^2+p_y^2}},\frac{p_z}{\sqrt{p_x^2+p_y^2}}\right)=\frac{1}{\sqrt{p_x^2+p_y^2}}p$
Then I calculated each partial derivative and I got
$$\nabla f(p)=\begin{pmatrix} \frac{p_y^2}{(p_x^2+p_y^2)^{3/2}} & \frac{p_xp_y}{(p_x^2+p_y^2)^{3/2}} & 0 \\ \frac{p_x^2}{(p_x^2+p_y^2)^2} & \frac{p_xp_y}{(p_x^2+p_y^2)^{3/2}} & 0\\ 0 & 0 & \frac{1}{(p_x^2+p_y^2)^{1/2}}\end{pmatrix}$$
And each ones of them looks continuous, but what further argument could I use?, would be enough to say thatgiven the domain of the function the denominator is never zero so each function is continuous in its domain?. And since each function can be differentiated again the $f$ is continuosly differentiable.
Now I have to prove the differentiable continuity of $f^{-1}$. Doing some calculations with the cylidner and the parametric equations above I got $$x^2=t^2p_x^2=1-y^2\; (1)\\y^2=t^2p_y^2=1-x^2 \;(2)\\z=tp_z\; (3)$$
But I couldn't find the expression for $p_x,p_y,p_z$ in terms of $x,y,z$ in order to find $f^{-1}$, and I couldn't think of a way to determine is the statement "$f$ transforms parallels in circumferences and meridians in straight lines" is true.

REPLY [2 votes]: My natural inclination is to appeal to symmetry about the $z$-axis (which is the content of the wording in the question that parallels map to parallels and meridians map to straight lines). If we use spherical coordinates $(\phi,\theta)$ on the sphere and cylindrical coordinates $(z,\theta)$ on the cylinder, then the mapping $f$ is given by
$$f(\phi,\theta)=(\cot\phi,\theta), \quad 0<\phi<\pi, 0\le\theta<2\pi,$$
as we see in this figure:

Now, once you know that these are smooth coordinate systems on the respective surfaces, then it follows easily that $f$ and $f^{-1}$ are smooth, since
$$f^{-1}(z,\theta) = (\operatorname{arccot} z,\theta)$$
and both $\cot$ and $\operatorname{arccot}$ are smooth functions.
As is often the case here, it's difficult to know what course you're in and what your acceptable toolbox might be, so feel free to ask questions.


TITLE: convergence in $L^1$ for a subsequence
QUESTION [2 upvotes]: If we have a sequence $(f_n)$, which is convergence in measure to $f$. If we can prove that a subsequence $(f_{n_k})$ converges to $f$ in $L^1$. Can we say that the original sequence converges to $f$ in $L^1$ as well? If not, what extra conditions do we need?
Thanks！

REPLY [1 votes]: I think I have found a counterexample.
Consider $f\equiv0$ and the sequence $f_n$ given by
\begin{equation*}
f_n(x) =\begin{cases}
1/n &\text{if $\vert x \vert \leq 1/n$}\\
0 &\text{if $\vert x \vert > 1/n$}
\end{cases}
\end{equation*}
if $n$ is odd, and
\begin{equation*}
f_n(x) =\begin{cases}
n^2 &\text{if $\vert x \vert \leq 1/n$}\\
0 &\text{if $\vert x \vert > 1/n$}
\end{cases}
\end{equation*}
if $n$ is even
We see that the sequence converges in measure to $f$, and also the subsequence $f_n$ with $n$ odd, converges to $f$ in $L^1$, however the subsequence $f_n$, with $n$ even, doesn't converge to $f$ in $L^1$, as we have
\begin{equation*}
\Vert f_n-f \Vert_1=\int_{-1/n}^{1/n}n^2dx=2n
\end{equation*}
An extra condition to secure that the sequence will converge in $L^1$ is if the difference between $f_n$ and $f$ is bounded a.e. However, I don't know if there are weaker extra conditions which secure convergence in $L^1$.


text:
(*******************************************************************************

  Project: IsaNet

  Author:  Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
           Tobias Klenze, ETH Zurich <tobias.klenze@inf.ethz.ch>
  Version: JCSPaper.1.0
  Isabelle Version: Isabelle2021-1

  Copyright (c) 2022 Christoph Sprenger
  Licence: Mozilla Public License 2.0 (MPL) / BSD-3-Clause (dual license)

*******************************************************************************)

chapter\<open>Verification Infrastructure\<close>
text\<open>Here we define event systems, the term algebra, and the Dolev--Yao adversary\<close>
section \<open>Event Systems\<close>

text \<open>This theory contains definitions of event systems, trace, traces, reachability, simulation,
and proves the soundness of simulation for proving trace inclusion. We also derive some related
simulation rules.\<close>

theory Event_Systems
  imports Main
begin

record ('e, 's) ES =
  init :: "'s \<Rightarrow> bool"
  trans :: "'s \<Rightarrow> 'e \<Rightarrow> 's \<Rightarrow> bool"   ("(4_: _\<midarrow>_\<rightarrow> _)" [50, 50, 50] 90)

(********************************************************************************)
subsection \<open>Reachable states and invariants\<close>
(********************************************************************************)

inductive
  reach :: "('e, 's) ES \<Rightarrow> 's \<Rightarrow> bool" for E
  where
    reach_init [simp, intro]:  "init E s \<Longrightarrow> reach E s"
  | reach_trans [intro]: "\<lbrakk> E: s \<midarrow>e\<rightarrow> s'; reach E s \<rbrakk> \<Longrightarrow> reach E s'"

thm reach.induct

text \<open>Abbreviation for stating that a predicate is an invariant of an event system.\<close>

definition Inv :: "('e, 's) ES \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" where
  "Inv E I \<longleftrightarrow> (\<forall>s. reach E s \<longrightarrow> I s)"

lemmas InvI = Inv_def [THEN iffD2, rule_format]
lemmas InvE [elim] = Inv_def [THEN iffD1, elim_format, rule_format]

lemma Invariant_rule [case_names Inv_init Inv_trans]:
  assumes "\<And>s0. init E s0 \<Longrightarrow> I s0"
     and  "\<And>s e s'. \<lbrakk>E: s \<midarrow>e\<rightarrow> s'; reach E s; I s\<rbrakk> \<Longrightarrow> I s'"
  shows "Inv E I"
  unfolding Inv_def
proof (intro allI impI)
  fix s
  assume "reach E s"
  then show "I s" using assms
    by (induction s rule: reach.induct) (auto)
qed

text \<open>Invariant rule that allows strengthening the proof with another invariant.\<close>
lemma Invariant_rule_Inv [case_names Inv_other Inv_init Inv_trans]:
  assumes "Inv E J"
     and  "\<And>s0. init E s0 \<Longrightarrow> I s0"
     and  "\<And>s e s'. \<lbrakk>E: s \<midarrow>e\<rightarrow> s'; reach E s; I s; J s; J s'\<rbrakk> \<Longrightarrow> I s'"
  shows "Inv E I"
  unfolding Inv_def
proof (intro allI impI)
  fix s
  assume "reach E s"
  then show "I s" using assms
    by (induction s rule: reach.induct)(auto 3 4)
qed

(********************************************************************************)
subsection \<open>Traces\<close>
(********************************************************************************)

type_synonym 'e trace = "'e list"

inductive
  trace :: "('e, 's) ES \<Rightarrow> 's \<Rightarrow> 'e trace \<Rightarrow> 's \<Rightarrow> bool"  ("(4_: _ \<midarrow>\<langle>_\<rangle>\<rightarrow> _)" [50, 50, 50] 90)
  for E s
  where
    trace_nil [simp,intro!]:
      "E: s \<midarrow>\<langle>[]\<rangle>\<rightarrow> s"
  | trace_snoc [intro]:
      "\<lbrakk> E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'; E: s' \<midarrow>e\<rightarrow> s'' \<rbrakk> \<Longrightarrow> E: s \<midarrow>\<langle>\<tau> @ [e]\<rangle>\<rightarrow> s''"

thm trace.induct

inductive_cases trace_nil_invert [elim!]: "E: s \<midarrow>\<langle>[]\<rangle>\<rightarrow> t"
inductive_cases trace_snoc_invert [elim]: "E: s \<midarrow>\<langle>\<tau> @ [e]\<rangle>\<rightarrow> t"

lemma trace_init_independence [elim]:
  assumes "E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'" "trans E = trans F"
  shows "F: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'"
  using assms
by (induction rule: trace.induct) auto

lemma trace_single [simp, intro!]: "\<lbrakk> E: s \<midarrow>e\<rightarrow> s' \<rbrakk> \<Longrightarrow> E: s \<midarrow>\<langle>[e]\<rangle>\<rightarrow> s'"
  by (auto intro: trace_snoc[where \<tau> = "[]", simplified])

text \<open>Next, we prove an introduction rule for a "cons" trace and a case analysis rule
distinguishing the empty trace and a "cons" trace.\<close>

lemma trace_consI:
  assumes
    "E: s'' \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'" "E: s \<midarrow>e\<rightarrow> s''"
  shows
    "E: s \<midarrow>\<langle>e # \<tau>\<rangle>\<rightarrow> s'"
  using assms
by (induction rule: trace.induct) (auto dest: trace_snoc)

lemma trace_cases_cons:
  assumes
    "E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'"
    "\<lbrakk> \<tau> = []; s' = s \<rbrakk> \<Longrightarrow> P"
    "\<And>e \<tau>' s''. \<lbrakk> \<tau> = e # \<tau>'; E: s \<midarrow>e\<rightarrow> s''; E: s'' \<midarrow>\<langle>\<tau>'\<rangle>\<rightarrow> s' \<rbrakk> \<Longrightarrow> P"
  shows "P"
  using assms
by (induction rule: trace.induct) fastforce+

lemma trace_consD: "(E: s \<midarrow>\<langle>e # \<tau>\<rangle>\<rightarrow> s') \<Longrightarrow> \<exists> s''. (E: s \<midarrow>e\<rightarrow> s'') \<and> (E: s'' \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s')"
  by(auto elim: trace_cases_cons)

text \<open>We show how a trace can be appended to another.\<close>

lemma trace_append: "(E: s \<midarrow>\<langle>\<tau>\<^sub>1\<rangle>\<rightarrow> s') \<and> (E: s' \<midarrow>\<langle>\<tau>\<^sub>2\<rangle>\<rightarrow> s'') \<Longrightarrow> E: s \<midarrow>\<langle>\<tau>\<^sub>1@\<tau>\<^sub>2\<rangle>\<rightarrow> s''"
  by(induction \<tau>\<^sub>1 arbitrary: s)
    (auto dest!: trace_consD intro: trace_consI)

lemma trace_append_invert: "(E: s \<midarrow>\<langle>\<tau>\<^sub>1@\<tau>\<^sub>2\<rangle>\<rightarrow> s'') \<Longrightarrow> \<exists>s' . (E: s \<midarrow>\<langle>\<tau>\<^sub>1\<rangle>\<rightarrow> s') \<and> (E: s' \<midarrow>\<langle>\<tau>\<^sub>2\<rangle>\<rightarrow> s'')"
  by (induction \<tau>\<^sub>1 arbitrary: s) (auto intro!: trace_consI dest!: trace_consD)

text\<open>We prove an induction scheme for combining two traces, similar to @{text list_induct2}.\<close>

lemma trace_induct2 [consumes 3, case_names Nil Snoc]:
  "\<lbrakk>E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s''; F: t \<midarrow>\<langle>\<sigma>\<rangle>\<rightarrow> t''; length \<tau> = length \<sigma>;
    P [] s [] t;
    \<And>\<tau> s' e s'' \<sigma> t' f t''.
    \<lbrakk>E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'; E: s'\<midarrow>e\<rightarrow> s''; F: t \<midarrow>\<langle>\<sigma>\<rangle>\<rightarrow> t'; F: t'\<midarrow>f\<rightarrow> t''; P \<tau> s' \<sigma> t'\<rbrakk>
      \<Longrightarrow> P (\<tau> @ [e]) s'' (\<sigma> @ [f]) t''\<rbrakk>
  \<Longrightarrow> P \<tau> s'' \<sigma> t''"
proof (induction \<tau> s'' arbitrary: \<sigma> t'' rule: trace.induct)
  case trace_nil
  then show ?case by auto
next
  case (trace_snoc \<tau> s' e s'')
  from \<open>length (\<tau> @ [e]) = length \<sigma>\<close> and \<open>F: t \<midarrow>\<langle>\<sigma>\<rangle>\<rightarrow> t''\<close>
  obtain f \<sigma>' t'
    where "\<sigma> = \<sigma>' @ [f]" "length \<tau> = length \<sigma>'" "F: t \<midarrow>\<langle>\<sigma>'\<rangle>\<rightarrow> t'" "F: t' \<midarrow>f\<rightarrow> t''"
    by (auto elim: trace.cases)
  then show ?case using trace_snoc by blast
qed

subsubsection \<open>Relate traces to reachability and invariants\<close>
(********************************************************************************)

lemma reach_trace_equiv: "reach E s \<longleftrightarrow> (\<exists>s0 \<tau>. init E s0 \<and> E: s0 \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s)"  (is "?A \<longleftrightarrow> ?B")
proof
  assume "?A" then show "?B"
    by (induction s rule: reach.induct) auto
next
  assume "?B"
  then obtain s0 \<tau> where "E: s0 \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s" "init E s0" by blast
  then show "?A"
    by (induction \<tau> s rule: trace.induct) auto
qed

lemma reach_traceI: "\<lbrakk>init E s0; E: s0 \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s\<rbrakk> \<Longrightarrow> reach E s"
  by(auto simp add: reach_trace_equiv)

lemma reach_trace_extend: "\<lbrakk>E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'; reach E s\<rbrakk> \<Longrightarrow> reach E s'"
  by (induction \<tau> s' rule: trace.induct) auto

lemma Inv_trace: "\<lbrakk>Inv E I; init E s0; E: s0 \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'\<rbrakk> \<Longrightarrow> I s'"
  by (auto simp add: Inv_def reach_trace_equiv)

subsubsection \<open>Trace semantics of event systems\<close>
(********************************************************************************)

text \<open>We define the set of traces of an event system.\<close>

definition traces :: "('e, 's) ES \<Rightarrow> 'e trace set" where
  "traces E = {\<tau>. \<exists>s s'. init E s \<and> E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'}"

lemma tracesI [intro]: "\<lbrakk> init E s; E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s' \<rbrakk> \<Longrightarrow> \<tau> \<in> traces E"
  by (auto simp add: traces_def)

lemma tracesE [elim]: "\<lbrakk> \<tau> \<in> traces E; \<And>s s'. \<lbrakk> init E s; E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s' \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
  by (auto simp add: traces_def)

lemma traces_nil [simp, intro!]: "init E s \<Longrightarrow> [] \<in> traces E"
  by (auto simp add: traces_def)

text\<open>We now define a trace property satisfaction relation: an event system satisfies a property
@{term "\<phi>"}, if its traces are contained in @{term \<phi>}.\<close>

definition trace_property :: "('e, 's) ES \<Rightarrow> 'e trace set \<Rightarrow> bool" (infix "\<Turnstile>\<^sub>E\<^sub>S" 90) where
  "E \<Turnstile>\<^sub>E\<^sub>S \<phi> \<longleftrightarrow> traces E \<subseteq> \<phi>"

lemmas trace_propertyI = trace_property_def [THEN iffD2, OF subsetI, rule_format]
lemmas trace_propertyE [elim] = trace_property_def [THEN iffD1, THEN subsetD, elim_format]
lemmas trace_propertyD = trace_property_def [THEN iffD1, THEN subsetD, rule_format]

text \<open>Rules for showing trace properties using a stronger trace-state invariant.\<close>

lemma trace_invariant:
  assumes
    "\<tau> \<in> traces E"
    "\<And>s s'. \<lbrakk> init E s; E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s' \<rbrakk> \<Longrightarrow> I \<tau> s'"
    "\<And>s. I \<tau> s \<Longrightarrow> \<tau> \<in> \<phi>"
  shows "\<tau> \<in> \<phi>" using assms
  by (auto)

lemma trace_property_rule:
  assumes
    "\<And>s0. init E s0 \<Longrightarrow> I [] s0"
    "\<And>s s' \<tau> e s''.
       \<lbrakk> init E s; E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'; E: s' \<midarrow>e\<rightarrow> s''; I \<tau> s'; reach E s' \<rbrakk> \<Longrightarrow> I (\<tau>@[e]) s''"
    "\<And>\<tau> s. \<lbrakk> I \<tau> s; reach E s \<rbrakk> \<Longrightarrow> \<tau> \<in> \<phi>"
  shows "E \<Turnstile>\<^sub>E\<^sub>S \<phi>"
proof (rule trace_propertyI, erule trace_invariant[where I="\<lambda>\<tau> s. I \<tau> s \<and> reach E s"])
  fix \<tau> s s'
  assume "E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'" and "init E s"
  then show "I \<tau> s' \<and> reach E s'"
    by (induction \<tau> s' rule: trace.induct) (auto simp add: assms)
qed (auto simp add: assms)

text \<open>Similar to @{thm trace_property_rule}, but allows matching pure state invariants directly.\<close>
lemma Inv_trace_property:
  assumes "Inv E I" and "[] \<in> \<phi>"
      and "(\<And>s \<tau> s' e s''.
      \<lbrakk>init E s; E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'; E: s' \<midarrow>e\<rightarrow> s''; I s; I s'; reach E s'; \<tau> \<in> \<phi>\<rbrakk> \<Longrightarrow> \<tau>@[e] \<in> \<phi>)"
    shows "E \<Turnstile>\<^sub>E\<^sub>S \<phi>"
  using assms(1,2)
  by (intro trace_property_rule[where I="\<lambda>\<tau> s. \<tau> \<in> \<phi>"]) (auto intro: assms(3))

subsection \<open>Simulation\<close>
(********************************************************************************)

text \<open>We first define the simulation preorder on pairs of states and derive a series of
useful coinduction principles.\<close>

coinductive
  sim :: "('e, 's ) ES \<Rightarrow> ('f, 't ) ES \<Rightarrow> ('e \<Rightarrow> 'f) \<Rightarrow> 's \<Rightarrow> 't \<Rightarrow> bool"
  for E F \<pi>
  where
    "\<lbrakk> \<And>e s'. (E: s \<midarrow>e\<rightarrow> s') \<Longrightarrow> \<exists>t'. (F: t \<midarrow>\<pi> e\<rightarrow> t') \<and> sim E F \<pi> s' t' \<rbrakk> \<Longrightarrow> sim E F \<pi> s t"

abbreviation
  simS :: "('e, 's ) ES \<Rightarrow> ('f, 't ) ES \<Rightarrow> 's \<Rightarrow> ('e \<Rightarrow> 'f) \<Rightarrow> 't \<Rightarrow> bool"
          ("(5_,_: _ \<sqsubseteq>\<^sub>_ _)" [50, 50, 50, 60, 50] 90)
where
  "simS E F s \<pi> t \<equiv> sim E F \<pi> s t"

lemmas sim_coinduct_id = sim.coinduct[where \<pi>=id, consumes 1, case_names sim]

text \<open>We prove a simplified and slightly weaker coinduction rule for simulation and
register it as the default rule for @{term sim}.\<close>

lemma sim_coinduct_weak [consumes 1, case_names sim, coinduct pred: sim]:
  assumes
    "R s t"
    "\<And>s t a s'. \<lbrakk> R s t;  E: s\<midarrow>a\<rightarrow> s'\<rbrakk> \<Longrightarrow> (\<exists>t'. (F: t\<midarrow>\<pi> a\<rightarrow> t') \<and> R s' t')"
  shows
    "E,F: s \<sqsubseteq>\<^sub>\<pi> t"
  using assms
  by (coinduction arbitrary: s t rule: sim.coinduct) (fastforce)

(*
lemmas sim_coinduct_weak_id [consumes 1, case_names sim, coinduct pred: sim] =
  sim_coinduct_weak [where \<pi>="id"]
*)

(*
  CHECK: declaring sim_refl as [intro] makes proof of simulation_soundness loop! (why?)
*)
lemma sim_refl: "E,E: s \<sqsubseteq>\<^sub>id s"
  by (coinduction arbitrary: s) auto

lemma sim_trans: "\<lbrakk> E,F: s \<sqsubseteq>\<^sub>\<pi>1 t; F,G: t \<sqsubseteq>\<^sub>\<pi>2 u \<rbrakk> \<Longrightarrow> E,G: s \<sqsubseteq>\<^sub>(\<pi>2 \<circ> \<pi>1) u"
proof (coinduction arbitrary: s t u)
  case (sim a s' s t)
  with \<open>E,F: s \<sqsubseteq>\<^sub>\<pi>1 t\<close> obtain t' where "F: t \<midarrow>\<pi>1 a\<rightarrow> t'" "E,F: s' \<sqsubseteq>\<^sub>\<pi>1 t'"
    by (cases rule: sim.cases) auto
  moreover
  from \<open>F,G: t \<sqsubseteq>\<^sub>\<pi>2 u\<close> \<open>F: t \<midarrow>\<pi>1 a\<rightarrow> t'\<close> obtain u' where "G: u \<midarrow>\<pi>2 (\<pi>1 a)\<rightarrow> u'" "F,G: t' \<sqsubseteq>\<^sub>\<pi>2 u'"
    by (cases rule: sim.cases) auto
  ultimately
  have "\<exists>t' u'. (G: u \<midarrow>\<pi>2 (\<pi>1 a)\<rightarrow> u') \<and> (E,F: s' \<sqsubseteq>\<^sub>\<pi>1 t') \<and> (F,G: t' \<sqsubseteq>\<^sub>\<pi>2 u')"
    by auto
  then show ?case by auto
qed

text \<open>Extend transition simulation to traces.\<close>

lemma trace_sim:
  assumes "E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'" "E,F: s \<sqsubseteq>\<^sub>\<pi> t"
  shows "\<exists>t'. (F: t \<midarrow>\<langle>map \<pi> \<tau>\<rangle>\<rightarrow> t') \<and> (E,F: s' \<sqsubseteq>\<^sub>\<pi> t')"
  using assms
proof (induction \<tau> s' rule: trace.induct)
  case trace_nil
  then show ?case by auto
next
  case (trace_snoc \<tau> s' e s'')
  then obtain t' where "F: t \<midarrow>\<langle>map \<pi> \<tau>\<rangle>\<rightarrow> t'" "E,F: s' \<sqsubseteq>\<^sub>\<pi> t'" by auto
  from \<open>E,F: s' \<sqsubseteq>\<^sub>\<pi> t'\<close> \<open>E: s'\<midarrow>e\<rightarrow> s''\<close>
  obtain t'' where "F: t' \<midarrow>\<pi> e\<rightarrow> t''" "E,F: s'' \<sqsubseteq>\<^sub>\<pi> t''"  by (elim sim.cases) fastforce
  then show ?case using \<open>F: t \<midarrow>\<langle>map \<pi> \<tau>\<rangle>\<rightarrow> t'\<close> \<open>E: s \<midarrow>\<langle>\<tau>\<rangle>\<rightarrow> s'\<close> \<open>E: s'\<midarrow>e\<rightarrow> s''\<close> by auto
qed

subsubsection \<open>Simulation for event systems\<close>
(********************************************************************************)

definition
  sim_ES :: "('e, 's ) ES \<Rightarrow> ('e \<Rightarrow> 'f) \<Rightarrow> ('f, 't ) ES \<Rightarrow> bool"  ("(3_ \<sqsubseteq>\<^sub>_ _)" [50, 60, 50] 95)
where
  "E \<sqsubseteq>\<^sub>\<pi> F \<longleftrightarrow> (\<exists>R.
     (\<forall>s0. init E s0 \<longrightarrow> (\<exists>t0. init F t0 \<and> R s0 t0)) \<and>
     (\<forall>s t. R s t \<longrightarrow> E,F: s \<sqsubseteq>\<^sub>\<pi> t))"

lemma sim_ES_I:
  assumes
    "\<And>s0. init E s0 \<Longrightarrow> (\<exists>t0. init F t0 \<and> R s0 t0)" and
    "\<And>s t. R s t \<Longrightarrow> E,F: s \<sqsubseteq>\<^sub>\<pi> t"
  shows "E \<sqsubseteq>\<^sub>\<pi> F"
  using assms
  by (auto simp add: sim_ES_def)

lemma sim_ES_E:
  assumes
    "E \<sqsubseteq>\<^sub>\<pi> F"
    "\<And>R. \<lbrakk> \<And>s0. init E s0 \<Longrightarrow> (\<exists>t0. init F t0 \<and> R s0 t0); \<And>s t. R s t \<Longrightarrow> E,F: s \<sqsubseteq>\<^sub>\<pi> t \<rbrakk> \<Longrightarrow> P"
  shows "P"
  using assms
  by (auto simp add: sim_ES_def)

text \<open>Different rules to set up a simulation proof. Include reachability or weaker invariant(s)
in precondition of ``simulation square''.\<close>

lemma simulate_ES:
  assumes
    init: "\<And>s0. init E s0 \<Longrightarrow> (\<exists>t0. init F t0 \<and> R s0 t0)" and
    step: "\<And>s t a s'. \<lbrakk> R s t; reach E s; reach F t; E: s\<midarrow>a\<rightarrow> s' \<rbrakk>
                    \<Longrightarrow> (\<exists>t'. (F: t\<midarrow>\<pi> a\<rightarrow> t') \<and> R s' t')"
  shows "E \<sqsubseteq>\<^sub>\<pi> F"
  by (auto 4 4 intro!: sim_ES_I[where R="\<lambda>s t. R s t \<and> reach E s \<and> reach F t"] dest: init
               intro: sim_coinduct_weak[where R="\<lambda>s t. R s t \<and> reach E s \<and> reach F t"] dest: step)

lemma simulate_ES_with_invariants:
  assumes
    init: "\<And>s0. init E s0 \<Longrightarrow> (\<exists>t0. init F t0 \<and> R s0 t0)" and
    step: "\<And>s t a s'.
             \<lbrakk> R s t; I s; J t; E: s\<midarrow>a\<rightarrow> s' \<rbrakk> \<Longrightarrow> (\<exists>t'. (F: t\<midarrow>\<pi> a\<rightarrow> t') \<and> R s' t')" and
    invE: "\<And>s. reach E s \<longrightarrow> I s" and
    invE: "\<And>t. reach F t \<longrightarrow> J t"
  shows "E \<sqsubseteq>\<^sub>\<pi> F" using assms
  by (auto intro: simulate_ES[where R=R])

lemmas simulate_ES_with_invariant = simulate_ES_with_invariants[where J="\<lambda>s. True", simplified]

text \<open>Variants with a functional simulation relation, aka refinement mapping.\<close>

lemma simulate_ES_fun:
  assumes
    init: "\<And>s0. init E s0 \<Longrightarrow> init F (h s0)" and
    step: "\<And>s a s'. \<lbrakk> E: s\<midarrow>a\<rightarrow> s'; reach E s; reach F (h s) \<rbrakk> \<Longrightarrow> F: h s\<midarrow>\<pi> a\<rightarrow> h s'"
  shows "E \<sqsubseteq>\<^sub>\<pi> F"
  using assms
  by (auto intro!: simulate_ES[where R="\<lambda>s t. t = h s"])

lemma simulate_ES_fun_with_invariants:
  assumes
    init: "\<And>s0. init E s0 \<Longrightarrow> init F (h s0)" and
    step: "\<And>s a s'. \<lbrakk> E: s\<midarrow>a\<rightarrow> s'; I s; J (h s) \<rbrakk> \<Longrightarrow> F: h s\<midarrow>\<pi> a\<rightarrow> h s'" and
    invE: "\<And>s. reach E s \<longrightarrow> I s" and
    invF: "\<And>t. reach F t \<longrightarrow> J t"
  shows "E \<sqsubseteq>\<^sub>\<pi> F"
  using assms
  by (auto intro!: simulate_ES_fun)

lemmas simulate_ES_fun_with_invariant =
  simulate_ES_fun_with_invariants[where J="\<lambda>t. True", simplified]

text \<open>Reflexivity and transitivity for ES simulation.\<close>

lemma sim_ES_refl: "E \<sqsubseteq>\<^sub>id E"
  by (auto intro: sim_ES_I[where R="(=)"] sim_refl)

lemma sim_ES_trans:
  assumes "E \<sqsubseteq>\<^sub>\<pi>1 F" and "F \<sqsubseteq>\<^sub>\<pi>2 G" shows "E \<sqsubseteq>\<^sub>(\<pi>2 \<circ> \<pi>1) G"
proof -
  from \<open>E \<sqsubseteq>\<^sub>\<pi>1 F\<close> obtain R\<^sub>1 where
    "\<And>s0. init E s0 \<Longrightarrow> (\<exists>t0. init F t0 \<and> R\<^sub>1 s0 t0)"
    "\<And>s t. R\<^sub>1 s t \<Longrightarrow> E,F: s \<sqsubseteq>\<^sub>\<pi>1 t"
    by (auto elim!: sim_ES_E)
  moreover
  from \<open>F \<sqsubseteq>\<^sub>\<pi>2 G\<close> obtain R\<^sub>2 where
    "\<And>t0. init F t0 \<Longrightarrow> (\<exists>u0. init G u0 \<and> R\<^sub>2 t0 u0)"
    "\<And>t u. R\<^sub>2 t u \<Longrightarrow> F,G: t \<sqsubseteq>\<^sub>\<pi>2 u"
    by (auto elim!: sim_ES_E)
  ultimately show ?thesis
    by (auto intro!: sim_ES_I[where R="R\<^sub>1 OO R\<^sub>2"] sim_trans simp add: OO_def) blast
qed

subsubsection \<open>Soundness for trace inclusion and property preservation\<close>
(********************************************************************************)

lemma simulation_soundness: "E \<sqsubseteq>\<^sub>\<pi> F \<Longrightarrow> (map \<pi>)`traces E \<subseteq> traces F"
  by (fastforce simp add: sim_ES_def image_def dest: trace_sim)

lemmas simulation_rule = simulate_ES [THEN simulation_soundness]
lemmas simulation_rule_id = simulation_rule[where \<pi>="id", simplified]

text \<open>This allows us to show that properties are preserved under simulation.\<close>

(*
lemma property_preservation_trivial:
  "\<lbrakk>  map \<pi>`traces E \<subseteq> traces F; F \<Turnstile>\<^sub>E\<^sub>S P; \<And>\<tau>. map \<pi> \<tau> \<in> P \<Longrightarrow> \<tau> \<in> Q \<rbrakk> \<Longrightarrow> E \<Turnstile>\<^sub>E\<^sub>S Q"
  by (auto simp add: trace_property_def)
*)

corollary property_preservation:
  "\<lbrakk>E \<sqsubseteq>\<^sub>\<pi> F; F \<Turnstile>\<^sub>E\<^sub>S P; \<And>\<tau>. map \<pi> \<tau> \<in> P \<Longrightarrow> \<tau> \<in> Q \<rbrakk> \<Longrightarrow> E \<Turnstile>\<^sub>E\<^sub>S Q"
  by (auto simp add: trace_property_def dest: simulation_soundness)

(********************************************************************************)
subsection \<open>Simulation up to simulation preorder\<close>
(********************************************************************************)

lemma sim_coinduct_upto_sim [consumes 1, case_names sim]:
  assumes
    major:  "R s t" and
    S: "\<And>s t a s'. \<lbrakk> R s t; E: s \<midarrow>a\<rightarrow> s'\<rbrakk> \<Longrightarrow>
          \<exists>t'. (F: t \<midarrow>\<pi> a\<rightarrow> t') \<and> ((sim E E id) OO R OO (sim F F id)) s' t'"
  shows
    "E,F: s \<sqsubseteq>\<^sub>\<pi> t"
proof -
  let ?R_upto = "((sim E E id) OO R OO (sim F F id))"
  from major have "?R_upto s t" by (auto intro: sim_refl)
  then show ?thesis
  proof (coinduction arbitrary: s t)
    case (sim a s' s t)
    from \<open>((sim E E id) OO R OO (sim F F id)) s t\<close> obtain s1 t1 where
      "E,E: s \<sqsubseteq>\<^sub>id s1" "R s1 t1" "F,F: t1 \<sqsubseteq>\<^sub>id t" by (elim relcomppE)
    from \<open>E,E: s \<sqsubseteq>\<^sub>id s1\<close> \<open>E: s\<midarrow>a\<rightarrow> s'\<close>
    obtain s1' where "E: s1\<midarrow>a\<rightarrow> s1'" "E,E: s' \<sqsubseteq>\<^sub>id s1'" by (cases rule: sim.cases) auto
    from \<open>R s1 t1\<close> \<open>E: s1\<midarrow>a\<rightarrow> s1'\<close> S
    obtain t1' where "F: t1\<midarrow>\<pi> a\<rightarrow> t1'" "?R_upto s1' t1'" by force
    from \<open>F,F: t1 \<sqsubseteq>\<^sub>id t\<close> \<open>F: t1\<midarrow>\<pi> a\<rightarrow> t1'\<close>
    obtain t' where "F: t\<midarrow>\<pi> a\<rightarrow> t'" "F,F: t1' \<sqsubseteq>\<^sub>id t'" by (cases rule: sim.cases) auto
    from \<open>F: t\<midarrow>\<pi> a\<rightarrow> t'\<close> \<open>E,E: s' \<sqsubseteq>\<^sub>id s1'\<close> \<open>?R_upto s1' t1'\<close> \<open>F,F: t1' \<sqsubseteq>\<^sub>id t'\<close>
    have "((sim E E id) OO R OO (sim F F id)) s' t'"
      apply(auto simp add: OO_def) using comp_id sim_trans by metis
    then have "\<exists>t'. (F: t\<midarrow>\<pi> a\<rightarrow> t') \<and> ?R_upto s' t'"
      using \<open>F: t\<midarrow>\<pi> a\<rightarrow> t'\<close> by (auto intro: sim_trans)
    then show ?case using S by fastforce
  qed
qed

end


TITLE: Reference Request: Mature introduction to differential geometry
QUESTION [5 upvotes]: I didn't want to call it an advanced introduction, at the risk of sounding absurd.
What I'm looking for is a mature and/or modern introduction to differential geometry. Let me clarify three things: what I mean by mature is that the book should assume (or at least be targeted towards) someone who has experience reading math, and say a solid background in analysis, topology, and algebra (and maybe a very basic intro to differential geometry). What I mean by modern is that it does not shy away from using modern algebraic and analytic machinery. What I mean by "and/or" is that of course, I would be interested in either modern introductions or mature introductions, due to fear that maybe both is a tall order.
I know do Carmo has "Differential Geometry of Curves and Surfaces." Is that the best choice?

REPLY [5 votes]: The most user-friendly and elementary introduction to Differential Geometry is Loring Tu's An Introduction to Manifolds (2nd Edition) which really tells you how to make effective calculations .
Part of the friendliness is that Tu  gives at the beginning of each chapter a careful motivating explanation of its content, enriched by a short historical  introduction and photograph of a main contributor.
A more comprehensive treatise which will take you further in the subject, is our friend John Lee's rich and extremely accurate Introduction to Smooth Manifolds.
It covers all the main aspects of Manifold Theory in a detailed way and has many insightful drawings, a must in a geometry book.
 Do not confuse this book with Jeffrey Lee's Manifolds and Differential Geometry, which also seems excellent but which I haven't used sufficiently for me to comment on it.
The most encyclopedic treatise is Spivak's five volume (!)  A Comprehensive Introduction to Differential Geometry.
I can't begin to explain why this is one othe most extraordinary books ever written in Differential Geometry and even in all of Mathematics, but let me just describe one feature.
In Volume 2 Spivak gives a 19 page translation of Riemann's inaugural lecture, which so excited Gauss, and then goes on to explain using today's notation what Riemann meant.
This is invaluable because Riemann was inventing the concept of a differentiable riemannian manifold in that talk, but didn't have the necessary tools (essentially abstract topology) to be completely rigorous.
The modern definition of a manifold was  given only in 1913 by Hermann Weyl (in dimension one) and in 1936 by Hassler Whitney (in arbitrary dimension).
Similarly Spivak also explains Gauss's work in modern notation.
These "translations" from classical mathematics into modern notions and notations are just one of the gems of Spivak's masterful and incredibly original treatise.


text:
(*
    Author:      René Thiemann
                 Akihisa Yamada
    License:     BSD
*)
section \<open>Divmod-Int\<close>

text \<open>We provide the divmod-operation on type int for efficiency reasons.\<close>

theory Divmod_Int
imports Main
begin

definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
  "divmod_int n m = (n div m, n mod m)"

text \<open>We implement @{const divmod_int} via @{const divmod_integer}
  instead of invoking both division and modulo separately.\<close>

context
includes integer.lifting
begin

lemma divmod_int_code[code]: "divmod_int m n = map_prod int_of_integer int_of_integer
  (divmod_integer (integer_of_int m) (integer_of_int n))"
  unfolding divmod_int_def divmod_integer_def map_prod_def split prod.simps
proof
  show "m div n = int_of_integer
     (integer_of_int m div integer_of_int n)"
    by (transfer, simp)
  show "m mod n = int_of_integer
     (integer_of_int m mod integer_of_int n)"
    by (transfer, simp)
qed
end

end


TITLE: Atiyah-Macdonald Question 1.7
QUESTION [1 upvotes]: I have a solution to this question which I know to be wrong, but I can't find the mistake! The question reads "Let $A$ be a ring in which every element $x$ satisfies $x^n = x$ for some $n>1$. Show that every prime ideal in $A$ is maximal."
My solution goes:
We have $x^n-x = 0 \implies x(x^{n-1}-1) = 0$ so either $x$ is nilpotent or a unit or 0. If $x$ is nilpotent then so is $x^{n-1}$ as the nilradical is an ideal and so by Question 1 we have $x^{n-1}-1$ is a unit in $A$. Thus
$$0 = x(x^{n-1}-1)(x^{n-1}-1)^{-1} = x.$$
 Hence every non-zero element of $A$ is a unit and then the only prime and maximal ideal is (0).
I can't see where I've made the mistake but I must have somewhere otherwise it implies that all Boolean rings have two elements.

REPLY [0 votes]: We have $x^n-x = 0 \implies x(x^{n-1}-1) = 0$ so either $x$ is nilpotent or a unit or 0.

There are two mistakes in one here.  It appears you think that you are able to conclude that $x=0$ or $x^{n-1}-1=0$ from this line.
Firstly, as mentioned in a comment, this does not have to be an integral domain, and it need not be true.
Secondly, $x^{n-1}-1=0$ does not imply $x$ is nilpotent, it implies $x$ is a unit.
But basically the reasoning you gave is relevant, because you should be applying all this reasoning to $R/P$ where $P$ is a prime ideal. That proves that $R/P$ is a field, therefore $P$ is maximal.


text:
\begin{document}
\theoremstyle{plain}
\newtheorem{Thm}{Theorem}
\newtheorem{Cor}{Corollary}
\newtheorem{Con}{Conjecture}
\newtheorem{Main}{Main Theorem}

\newtheorem{Lem}{Lemma}
\newtheorem{Prop}{Proposition}

\theoremstyle{definition}
\newtheorem{Def}{Definition}
\newtheorem{Note}{Note}
\newtheorem{Ex}{Example}

\theoremstyle{remark}
\newtheorem{notation}{Notation}
\renewcommand{\thenotation}{}

\errorcontextlines=0
\numberwithin{equation}{section}
\renewcommand{\rm}{\normalshape}

\title
   {Reflection of a wave off a surface}
\author{Brendan Guilfoyle}
\address{Brendan Guilfoyle\\
          Department of Mathematics and Computing \\
          Institute of Technology, Tralee \\
          Clash \\
          Tralee  \\
          Co. Kerry \\
          Ireland.}
\email{brendan.guilfoyle@@ittralee.ie}

\author{Wilhelm Klingenberg}
\address{Wilhelm Klingenberg\\
 Department of Mathematical Sciences\\
 University of Durham\\
 Durham DH1 3LE\\
 United Kingdom.}
\email{wilhelm.klingenberg@@durham.ac.uk }

\date{July 22, 2002}

\begin{abstract}
Recent advances in twistor theory are applied to geometric optics in
${\Bbb{R}}^3$. The general formulae for reflection of a wavefront in
a surface are derived and in three special cases explicit descriptions
are provided: when the
reflecting surface is a plane, when the incoming wave is a plane
and when the incoming wave is spherical. In each case particular
examples are computed exactly and the results plotted to illustrate
the outgoing wavefront.

\end{abstract}

\maketitle

\section{Introduction}

In geometric optics, Huygens' principle allows one to describe the
propagation of light from two alternative perspectives: one can trace
the rays or one can trace the wavefronts. The drawback with the former
description is that following a finite number of rays may not describe
all of the phenomenon under study, while the formation of caustics in
wavefronts can cause difficulties in the latter description \cite{arn}.

In this paper we utilise recent work \cite{gak1} in twistor theory to
go back and forth between these two perspectives and thus describe the most
elementary of optical phenomena: reflection. In particular, we
consider the following situation: an incoming wave of light is
reflected on a surface in ${\Bbb{R}}^3$.  Given the shape
of the incoming wavefront and the reflecting surface, can one describe
the reflected wavefront? Throughout, we assume that the medium is
homogenous and that the speed of propagation is unity.

The technique we employ in answering this question comes from the
minitwistor correspondence which identifies the space of
oriented affine lines in ${\Bbb{R}}^3$ with the tangent bundle to the
2-sphere. This has a long history and has been used in various
contexts. In particular,  it has been used in the construction of
minimal surfaces \cite{weier}, solutions to the wave equation
\cite{whitt} and the monopole equation \cite{hitch}.

The general context of this work is within the study of line
congruences, that is, 2-parameter families of oriented lines in
${\Bbb{R}}^3$ \cite{hlav} \cite{hosch} \cite{pott}. A line congruence
is integrable if it is orthogonal to a family of surfaces in
${\Bbb{R}}^3$.  At the outset it is not clear that the reflection of
an integrable congruence in an arbitrary surface is itself
integrable. However, in Theorem \ref{t:int} that is precisely what we
prove. This is the celebrated Theorem of Malus, independently proven
by Hamilton in 1827.

In our formalism, going from an integrable line
congruence to the orthogonal surface is equivalent to inverting a
Cauchy-Riemann operator. The
reflection problem can then be broken down into four steps. First we
transfer from the incoming wavefront to its associated ray system and
we do the same for the reflecting surface. The reflection law
relates the outgoing rays to these two line congruences at the point of
contact, and, finally, we transform the outgoing rays to the
associated wavefront.

We present the general formulae relating all of these stages for an
arbitrary incoming wavefront and reflecting surface (Theorem
\ref{t:main}). We go on to give explicit descriptions for three special
cases: when the reflecting surface is a plane (Proposition
\ref{t:planesurf}), when the incoming wave is a plane (Proposition
\ref{t:planepar}) and when the incoming wave is spherical (Proposition
\ref{t:sphwave}). In each case, particular examples are computed
exactly and the results plotted to illustrate the outgoing wavefront.

The next section contains the background details of the twistor
construction we use - further details can be found in
\cite{gak2}.  In section 3 we deduce the required reflection law and
establish the fact that the outgoing ray system is integrable if and
only if the incoming rays are integrable.

In section 4 we turn to the
simplest type of reflection, namely, reflection of an arbitary
wavefront in a plane. Section 5
deals with the general formulae for reflection of a plane wavefront in
an arbitrary surface. As an illustration of our technique we determine
the reflection of a plane wave in a sphere and a torus. In the final
section we give the general formulae for reflection of a spherical
wavefront in an arbitrary surface, and illustrate the technique in the
case where the surface is the unit sphere.

\section{The Twistor Correspondence}

The key to our approach is the following geometric construction. Let
($x^1,x^2,x^3$) be Euclidean coordinates on
${\Bbb{R}}^3={\Bbb{C}}\oplus{\Bbb{R}}$ and set $z=x^1+ix^2$, $t=x^3$.

Consider an oriented line in ${\Bbb{R}}^3$ passing through ($z$, $t$) with
direction given by $\xi\in S^2\subset{\Bbb{R}}^3$, where $\xi$ is
obtained by stereographic projection from the south pole of the unit
sphere about the origin onto the
plane through the equator.

Then the minimal distance vector from the line to the origin is given by
\cite{gak1}
\[
\eta\frac{\partial}{\partial \xi}+\overline{\eta}\frac{\partial}{\partial \overline{\xi}}\in T_\xi S^2,
\]
where
\[
\eta=\frac{1}{2}(z-2t\xi-\overline{z}\xi^2),
\]
and the point ($z$, $t$) is a distance
\[
r=\frac{\overline{\xi}z+\xi\overline{z}+(1-\xi\overline{\xi})t}{1+\xi\overline{\xi}}.
\]
from the point on the line closest to the origin.

Conversely, given $\eta$ and $r$ and the direction of the line $\xi$,
the point ($z$, $t$) in ${\Bbb{R}}^3$ can be found by
\begin{equation}\label{e:coord1}
z=\frac{2(\eta-\overline{\eta}\xi^2)+2\xi(1+\xi\overline{\xi})r}{(1+\xi\overline{\xi})^2},
\end{equation}
\begin{equation}\label{e:coord2}
t=\frac{-2(\eta\overline{\xi}+\overline{\eta}\xi)+(1-\xi^2\overline{\xi}^2)r}{(1+\xi\overline{\xi})^2}.
\end{equation}

Now an oriented line in ${\Bbb{R}}^3$ is uniquely determined by $\xi$ and
$\eta$ as above. This is the minitwistor correspondence \cite{hitch},
where the space of oriented lines in ${\Bbb{R}}^3$ is identified with
the tangent bundle to the unit sphere about the origin.

\begin{Def}
A {\it line congruence} is a 2-parameter family of oriented
lines.
\end{Def}
 \begin{Def}
A line congruence is {\it integrable} if it is orthogonal to a family of
surfaces in ${\Bbb{R}}^3$.
\end{Def}

Suppose the line congruence is given by
$\nu\rightarrow(\xi(\nu,\bar{\nu}),\eta(\nu,\bar{\nu}))$, for
$\nu\in{\Bbb{C}}$.

\begin{Thm}\cite{gak2}
A line congruence is integrable iff
\begin{equation}\label{e:intcond}
\partial\left(\frac{\eta}{(1+\xi\bar{\xi})^2}\bar{\partial}\bar{\xi}+
  \frac{\bar{\eta}}{(1+\xi\bar{\xi})^2}\bar{\partial}\xi \right)=
\bar{\partial}\left(\frac{\bar{\eta}}{(1+\xi\bar{\xi})^2}\partial\xi+
  \frac{\eta}{(1+\xi\bar{\xi})^2}\partial\bar{\xi} \right),
\end{equation}
where $\partial$ is differentiation with respect to $\nu$.

This equation is the integrability condition for the existence of a
real solution $r$ to the following equation
\begin{equation}\label{e:pot}
\bar{\partial}r=\frac{2(\eta\bar{\partial}\bar{\xi}+\bar{\eta}\bar{\partial}\xi)}{(1+\xi\bar{\xi})^2},
\end{equation}
where $r$ is now considered as a function of $\nu$ and $\bar{\nu}$.
\end{Thm}

Thus, by the above theorem, given an integrable line congruence, we
can find a local description for the orthogonal surfaces by inverting
the $\bar{\partial}$ operator. The real constant of integration gives
the affine parameter along the lines normal to these surfaces. An
explicit description of the
surfaces in ${\Bbb{R}}^3$ can then be obtained by inserting $\xi$, $\eta$ and $r$, as
functions of $\nu$ and $\bar{\nu}$ into (\ref{e:coord1}) and
(\ref{e:coord2}).

Away from flat points, a surface can be parameterized by its normal
direction \cite{gak2}, i.e. $\nu=\xi$ and $\eta=F(\xi,\bar{\xi})$ for
some complex function $F$. In this case we refer to $F$ as the {\it
twistor function} of the surface, the integrability condition
(\ref{e:intcond}) reduces to the simpler
\[
\partial\left(\frac{F}{(1+\xi\bar{\xi})^2}\right)=
\bar{\partial}\left(\frac{\bar{F}}{(1+\xi\bar{\xi})^2} \right),
\]
and the function $r$ satisfies
\[
\bar{\partial}r=\frac{2F}{(1+\xi\bar{\xi})^2}.
\]
We will refer to $r$ as the {\it potential function} for the surface.

At a number of points in this paper we use Euclidean motions to
simplify the equations for reflection. A translation which takes the
origin to ($z$, $t$) is the quadratic holomorphic transformation
\[
\xi\rightarrow\xi, \qquad \qquad \eta\rightarrow\eta
    +\frac{1}{2}(z-2t\xi-\bar{z}\xi^2),
\]
while a rotation about the origin is given by the fractional linear
transformation:
\[
\xi\rightarrow\frac{\alpha\xi-\bar{\beta}}{\beta\xi+\bar{\alpha}},
\qquad \qquad \eta\rightarrow\frac{\eta}{(\beta\xi+\bar{\alpha})^2},
\]
where $\alpha, \beta\in{\Bbb{C}}$ satisfy
$\alpha\bar{\alpha}+\beta\bar{\beta}=1$.

\section{Reflection in a Surface}

Consider a ray with direction $\xi_1$ and perpendicular distance
vector $\eta_1$ striking a surface $S$ at the point ($z_0$,
$t_0$), where the normal direction is $\xi_0$ and  the perpendicular distance
vector  is $\eta_0$. Let $\xi_2$ be the direction of the outgoing wave and
$\eta_2$ be the perpendicular distance vector (see Figure 1).

\setlength{\epsfxsize}{3in}
\begin{center}
   \mbox{\epsfbox{reflection.eps}}
\end{center}

For the surface $S$, suppose that the point of reflection is a
distance $r_0$ from the minimal distance point on the normal line to the
origin, so that, by (\ref{e:coord1}) and (\ref{e:coord2})

\[
z_0=\frac{2(\eta_0-\overline{\eta}_0\xi_0^2)+2\xi_0(1+\xi_0\overline{\xi}_0)r_0}{(1+\xi_0\overline{\xi}_0)^2}, \qquad\qquad
t_0=\frac{-2(\eta_0\overline{\xi}_0+\overline{\eta}_0\xi_0)+(1-\xi_0^2\overline{\xi}_0^2)r_0}{(1+\xi_0\overline{\xi}_0)^2}.
\]

On the other hand, since both the incoming and outgoing rays contain
($z_0$, $t_0$),
\[
\eta_i=\frac{1}{2}(z_0-2t_0\xi_i-\overline{z}_0\xi_i^2),
\]
for $i=1,2$.

Combining the previous three equations we have, after some
rearrangement,
\begin{equation}\label{e:perpdists}
\eta_i=\frac{(1+\bar{\xi}_0\xi_i)^2\eta_0
-(\xi_0-\xi_i)^2\bar{\eta}_0
+(\xi_0-\xi_i)(1+\bar{\xi}_0\xi_i)(1+\xi_0\bar{\xi}_0)r_0
}{(1+\xi_0\bar{\xi}_0)^2}.
\end{equation}
We turn now to the law of reflection.

\begin{Prop}
If $\xi_1$ is the direction of the incoming ray, $\xi_2$ the outgoing
ray direction and  $\xi_0$ the normal direction at the point of
reflection, then

\begin{equation}\label{e:reflaw}
\xi_2=\frac{2\xi_0\bar{\xi}_1+1-\xi_0\bar{\xi}_0}
           {(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0}.
\end{equation}

\end{Prop}

\begin{pf}
A rotation about any point $\xi_0$ on ${\Bbb{P}}^1$ is described by a unitary
fractional linear transformation:
\[
\mbox{Rot}_{\xi_0}(\xi)=\frac{\alpha\xi-\bar{\beta}}{\beta\xi+\bar{\alpha}},
\]
where $\alpha, \beta\in{\Bbb{C}}$ satisfy
$\alpha\bar{\alpha}+\beta\bar{\beta}=1$. The inverse rotation is given
by
\begin{equation}\label{e:invrot}
\mbox{Rot}_{\xi_0}^{-1}(\xi)=\frac{\bar{\alpha}\xi+\bar{\beta}}{-\beta\xi+\alpha}.
\end{equation}
Let $S_{\xi_0}$ be the rotation
\[
S_{\xi_0}(\xi)=\frac{\alpha\xi-\bar{\beta}}{\beta\xi+\bar{\alpha}},
\]
where
\[
\alpha=\frac{1}{\sqrt{1+\xi_0\bar{\xi}_0}} \qquad\qquad
\beta=\frac{\bar{\xi}_0}{\sqrt{1+\xi_0\bar{\xi}_0}}.
\]
Clearly $S_{\xi_0}$ is a rotation that takes $\xi_0$ to zero (the
North pole). Thus, if we denote reflection through $\xi_0$ by
$R_{\xi_0}$, then $R_{\xi_0}=S_{\xi_0}^{-1}\circ R_{0}\circ S_{\xi_0}$.

Now $R_{0}(\xi)=-\xi$, so using (\ref{e:invrot}) and the definition of
$S_{\xi_0}$ we find that
\[
R_{\xi_0}(\xi)=\frac{(\xi_0\bar{\xi}_0-1)\xi+2\xi_0}
          {2\bar{\xi}_0\xi+1-\xi_0\bar{\xi}_0}.
\]
Alternatively, we can define $R_{\xi_0}$ as above and check that it is
a rotation (obvious), and satisfies $R_{\xi_0}(\xi_0)=\xi_0$ and
$R_{\xi_0}\circ R_{\xi_0}(\xi)=\xi$. Thus it is a
rotation through 180$^0$ about $\xi_0$ i.e. reflection in
$\xi_0$.

Finally, the law of reflection says that the direction $\xi_2$ of
the outgoing ray is obtained by reflecting the antipodal direction of
the incoming ray $\xi_1$ through the normal direction $\xi_0$ at the
point of reflection.

To complete the proposition, we note that the antipodal map on
${\Bbb{P}}^1$ is $\xi\rightarrow-\bar{\xi}^{-1}$, so that
\[
\xi_2=R_{\xi_0}\left(-\frac{1}{\bar{\xi}}\right)
=\frac{2\xi_0\bar{\xi}_1+1-\xi_0\bar{\xi}_0}
           {(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0},
\]
as claimed.
\end{pf}

The equations governing reflection are:

\begin{Thm}\label{t:main}
Consider a wavefront given by
$\nu_1\rightarrow(\xi_1(\nu_1,\bar{\nu}_1),\eta_1(\nu_1,\bar{\nu}_1))$
reflecting off a surface given by
$\nu_0\rightarrow(\xi_0(\nu_0,\bar{\nu}_0),\eta_0(\nu_0,\bar{\nu}_0))$
and $r_0(\nu_0,\bar{\nu}_0)$. Then the reflected wavefront is
determined by

\begin{equation}\label{e:reflawa}
\xi_2=\frac{2\xi_0\bar{\xi}_1+1-\xi_0\bar{\xi}_0}
           {(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0},
\end{equation}
\begin{equation}\label{e:key1}
\eta_1=\frac{(1+\bar{\xi}_0\xi_1)^2\eta_0
-(\xi_0-\xi_1)^2\bar{\eta}_0
+(\xi_0-\xi_1)(1+\bar{\xi}_0\xi_1)(1+\xi_0\bar{\xi}_0)r_0,
}{(1+\xi_0\bar{\xi}_0)^2}
\end{equation}
\begin{equation}\label{e:key2}
\eta_2=\frac{(\bar{\xi}_0-\bar{\xi}_1)^2\eta_0
-(1+\xi_0\bar{\xi}_1)^2\bar{\eta}_0
+(\bar{\xi}_0-\bar{\xi}_1)(1+\xi_0\bar{\xi}_1)(1+\xi_0\bar{\xi}_0)r_0
}{((1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0)^2}.
\end{equation}
Equation (\ref{e:key1})
determines the intersection of the incident rays with the surface,
while (\ref{e:reflawa}) and (\ref{e:key2}) determine the direction and
perpendicular distance from the origin of the reflected rays.
\end{Thm}
\begin{pf}
These come from combining the reflection law (\ref{e:reflaw}) with
(\ref{e:perpdists}), after some rearrangement for $\eta_2$.
\end{pf}

In general, the reflected line congruence can be parameterized by
$\nu_1$, the parameter for the incoming wavefront.

\begin{Thm}\label{t:int}
The surface, incident and reflected congruences satisfy the following
relationship:
\begin{equation}\label{e:twist}
\frac{\eta_2\bar{\partial}_1\bar{\xi}_2+\bar{\eta}_2\bar{\partial}_1\xi_2}{(1+\xi_2\bar{\xi}_2)^2}=
\frac{\eta_1\bar{\partial}_1\bar{\xi}_1+\bar{\eta}_1\bar{\partial}_1\xi_1}{(1+\xi_1\bar{\xi}_1)^2}+
\bar{\partial}_1\left(\frac{|\xi_0-\xi_1|^2-|1+\xi_0\bar{\xi}_1|^2}
    {(1+\xi_0\bar{\xi}_0)(1+\xi_1\bar{\xi}_1)}\;r_0
\right),
\end{equation}
where $\partial_1$ is differentiation with respect to $\nu_1$, the
parameter for the incoming wave.
\end{Thm}
\begin{pf}
We start by differentiating the reflection law (\ref{e:reflawa}):
\[
\partial_1\xi_2=\frac{-(1+\xi_0\bar{\xi}_0)^2\partial_1\bar{\xi}_1+2(\bar{\xi}_0- \bar{\xi}_1)^2\partial_1\xi_0+2(1+\xi_0\bar{\xi}_1)^2\partial_1\bar{\xi}_0}{[(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0]^2},
\]
\[
\bar{\partial}_1\xi_2=\frac{-(1+\xi_0\bar{\xi}_0)^2\bar{\partial}_1\bar{\xi}_1+2(\bar{\xi}_0-\bar{\xi}_1)^2\bar{\partial}_1\xi_0+2(1+\xi_0\bar{\xi}_1)^2\bar{\partial}_1\bar{\xi}_0}{[(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0]^2}.
\]
The reflection law (\ref{e:reflawa}) also implies
\[
1+\xi_2\bar{\xi}_2=\frac{(1+\xi_0\bar{\xi}_0)^2(1+\xi_1\bar{\xi}_1)}{[(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0][(1-\xi_0\bar{\xi}_0)\xi_1-2\xi_0]}.
\]
Thus, using (\ref{e:key1}) and (\ref{e:key2}) we find
\begin{align}\nonumber
\frac{\eta_2\bar{\partial}_1\bar{\xi}_2+\bar{\eta}_2\bar{\partial}_1\xi_2}{(1+\xi_2\bar{\xi}_2)^2}=&\frac{\eta_1\bar{\partial}_1\bar{\xi}_1+\bar{\eta}_1\bar{\partial}_1\xi_1}{(1+\xi_1\bar{\xi}_1)^2}
+\frac{2(|\xi_0-\xi_1|^2-|1+\xi_0\bar{\xi}_1|^2)(\eta_0\bar{\partial}_1\bar{\xi}_0+\bar{\eta}_0\bar{\partial}_1\xi_0)}{(1+\xi_0\bar{\xi}_0)^3(1+\xi_1\bar{\xi}_1)}\\\nonumber
&+\frac{2[(\xi_0-\xi_1)(1+\xi_0\bar{\xi}_1)[(1+\xi_1\bar{\xi}_1)\bar{\partial}_1\bar{\xi}_0-(1+\xi_0\bar{\xi}_0)\bar{\partial}_1\bar{\xi}_1]]}{(1+\xi_0\bar{\xi}_0)^2(1+\xi_1\bar{\xi}_2)}\;r_0\\
&+\frac{2[(\bar{\xi}_0-\bar{\xi}_1)(1+\bar{\xi}_0\xi_1)[(1+\xi_1\bar{\xi}_1)\bar{\partial}_1\xi_0-(1+\xi_0\bar{\xi}_0)\bar{\partial}_1\xi_1]]}{(1+\xi_0\bar{\xi}_0)^2(1+\xi_1\bar{\xi}_2)}\;r_0\label{e:inta}.
\end{align}
Now, since we are reflecting in a surface, we have the potential
function $r_0$ satisfying
\[
\frac{2(\eta_0\bar{\partial}_0\bar{\xi}_0+\bar{\eta}_0\bar{\partial}_0\xi_0)}{(1+\xi_0\bar{\xi}_0)^2}=\bar{\partial}_0r_0,
\]
and so
\begin{align}
\frac{2(\eta_0\bar{\partial}_1\bar{\xi}_0+\bar{\eta}_0\bar{\partial}_1\xi_0)}{(1+\xi_0\bar{\xi}_0)^2}=&\frac{2(\eta_0(\bar{\partial}_1\bar{\nu}_0\bar{\partial}_0\bar{\xi}_0+\bar{\partial}_1\nu_0\partial_0\bar{\xi}_0)
+\bar{\eta}_0(\bar{\partial}_1\nu_0\partial_0\xi_0+\bar{\partial}_1\bar{\nu}_0\bar{\partial}_0\xi_0)}{(1+\xi_0\bar{\xi}_0)^2}\nonumber\\
&=\frac{2(\bar{\partial}_1\bar{\nu}_0(\eta_0\bar{\partial}_0\bar{\xi}_0+\bar{\eta}_0\bar{\partial}_0\xi_0)+\bar{\partial}_1\nu_0(\eta_0\partial_0\bar{\xi}_0+\bar{\eta}_0\partial_0\xi_0))}{(1+\xi_0\bar{\xi}_0)^2}\nonumber\\
&=\bar{\partial}_1\bar{\nu}_0\bar{\partial}_0r_0+\bar{\partial}_1\nu_0\partial_0r_0
\nonumber\\
&=\bar{\partial}_1r_0. \nonumber
\end{align}
Substituting this in (\ref{e:inta}) we get that
\begin{align}\nonumber
\frac{\eta_2\bar{\partial}_1\bar{\xi}_2+\bar{\eta}_2\bar{\partial}_1\xi_2}{(1+\xi_2\bar{\xi}_2)^2}=&\frac{\eta_1\bar{\partial}_1\bar{\xi}_1+\bar{\eta}_1\bar{\partial}_1\xi_1}{(1+\xi_1\bar{\xi}_1)^2}
+\frac{|\xi_0-\xi_1|^2-|1+\xi_0\bar{\xi}_1|^2}{(1+\xi_0\bar{\xi}_0)(1+\xi_1\bar{\xi}_1)}\bar{\partial}_1r_0\\\nonumber
&+\frac{2[(\xi_0-\xi_1)(1+\xi_0\bar{\xi}_1)[(1+\xi_1\bar{\xi}_1)\bar{\partial}_1\bar{\xi}_0-(1+\xi_0\bar{\xi}_0)\bar{\partial}_1\bar{\xi}_1]]}{(1+\xi_0\bar{\xi}_0)^2(1+\xi_1\bar{\xi}_2)}\;r_0\\\nonumber
&+\frac{2[(\bar{\xi}_0-\bar{\xi}_1)(1+\bar{\xi}_0\xi_1)[(1+\xi_1\bar{\xi}_1)\bar{\partial}_1\xi_0-(1+\xi_0\bar{\xi}_0)\bar{\partial}_1\xi_1]]}{(1+\xi_0\bar{\xi}_0)^2(1+\xi_1\bar{\xi}_2)}\;r_0,\nonumber
\end{align}
and the last three terms on the right hand side are $\bar{\partial}_1$ of
the real function, as stated in the theorem.
\end{pf}

As a corollary we get the Theorem of Malus:

\begin{Cor}
A reflected congruence is integrable if and only if the initial
congruence is integrable.
\end{Cor}
\begin{pf}
Since the second term on the right-hand side of (\ref{e:twist}) is
$\bar{\partial}_1$ of a real function, the integrability condition
(\ref{e:intcond}) means that the outgoing congruence is integrable if
and only if the incoming wave is integrable.
\end{pf}

In the next sections we consider three special cases: that of
reflection of an arbitrary wavefront in a plane, and
that of plane and spherical wavefronts reflected off an arbitrary
surface. In all cases the
resulting wavefront can be explicitly determined.

More generally, assume that the incident wave can be
described by $\eta_1=F_1(\xi_1,\bar{\xi}_1)$ for some complex function
$F_1$. Suppose further that we can invert (\ref{e:key1}) for $\xi_1$
as a function of $\xi_0$ and $\eta_0$. Then we can substitute
this in (\ref{e:reflawa}) and (\ref{e:key2})
to find both $\xi_2$ and $\eta_2$ as a function of $\xi_0$ and
$\eta_0$. Finally, we can find the potential function $r_2$ by
integrating (\ref{e:pot}).

\section{Reflection in a Plane}

Consider an arbitrary wave described parametrically by
$\xi_1(\nu,\bar{\nu})$ and $\eta_1(\nu,\bar{\nu})$. We want to determine
the resulting  wave  after reflection in a plane. By a rotation we can
align the plane with the $x^1x^2$-plane so that the initial wave lies in the region $x^3>0$.
\begin{Prop}\label{t:planesurf}
The reflection of a wave given by $\xi_1(\nu,\bar{\nu})$ and
$\eta_1(\nu,\bar{\nu})$ in the $x^1x^2$-plane is
\begin{equation}\label{e:refinpl}
\xi_2=\frac{1}{\bar{\xi}_1},
\qquad\qquad
\eta_2=-\frac{\bar{\eta}_1}{\bar{\xi}_1^2}.
\end{equation}
\end{Prop}

\begin{pf}
The $x^1x^2$-plane is given by $\xi_0=r_0=0$. Inserting this in the
reflection law (\ref{e:reflawa}) immediately gives the first of the
above equations. Inserting it in (\ref{e:key1}) and (\ref{e:key2}) we
get
\begin{equation}\label{e:step1}
\eta_1=\eta_0-\xi_1^2\bar{\eta}_0,
\qquad\qquad
\eta_2=\eta_0-\frac{\bar{\eta}_0}{\bar{\xi}_1^2}.
\end{equation}
Adding the first of these to $\xi_1^2$ times its complex conjugate gives
\[
\eta_0=\frac{\eta_1+\xi_1^2\bar{\eta}_1}{1-\xi_1^2\bar{\xi}_1^2}.
\]
Inserting this in the second of (\ref{e:step1}) gives the result.
\end{pf}

\subsection{Reflection of a Spherical Wavefront in a Plane}
Consider a spherical wavefront with source ($0,0,t_1$). This
congruence is given by $\eta_1=-2t_1\xi_1$. Substituting this in
(\ref{e:refinpl}) we find
\[
\xi_2=\frac{1}{\bar{\xi}_1}
\qquad\qquad
\eta_2=\frac{2t_1}{\bar{\xi}_1}.
\]
Combining these two we see that $\eta_2=2t_1\xi_2$, which is a
spherical congruence with source ($0,0,-t_1$). Thus we retrieve
the well-known law of reflection, whereby the reflection of a
spherical wave centered at ($0,0,t_1$) in a plane mirror is another
spherical wave with virtual centre ($0,0,-t_1$).

\section{Reflection of a Plane Wavefront}

Consider an incoming wavefront with fixed direction, i.e. a plane
wavefront. In this case, the reflected wave can be expressed
explicitly in terms of the reflecting surface:

\begin{Prop}\label{t:planepar}
The reflection of a plane wavefront with direction $\xi_1$ off a
surface given by $\xi_0(\nu,\bar{\nu})$ and $\eta_0(\nu,\bar{\nu})$ is
    given by
\begin{equation}\label{e:planewave1}
\xi_2=\frac{2\xi_0\bar{\xi}_1+1-\xi_0\bar{\xi}_0}
           {(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0},
\end{equation}
\begin{equation}\label{e:planewave2}
\eta_2=\frac{(\bar{\xi}_0-\bar{\xi}_1)^2\eta_0
-(1+\xi_0\bar{\xi}_1)^2\bar{\eta}_0
+(\bar{\xi}_0-\bar{\xi}_1)(1+\xi_0\bar{\xi}_1)(1+\xi_0\bar{\xi}_0)r_0
}{((1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0)^2},
\end{equation}
the reflected congruence being parameterized by the parameter value
$\nu$ of the surface at the point of reflection.
\end{Prop}
\begin{pf}

Since the incident angle is constant, there is no need to determine
the points of intersection, and the above equations are just the
equation of reflection (\ref{e:reflawa}) and equation (\ref{e:key2}).
\end{pf}

In this proposition, the resulting wavefront is parameterized by the point
of reflection on the surface. For a plane wave it is also possible to parameterise the
outgoing wave by its direction:

\begin{Prop}\label{t:planedir}
Suppose $S$ a surface in ${\Bbb{R}}^3$, given by the
$\eta_0=F_0(\xi,\bar{\xi})$ with potential function
$r_0(\xi,\bar{\xi})$, is struck by a plane wave with normal direction
$-\bar{\xi}_1^{-1}$. Then the reflected wave is given by the line
congruence ($\xi$, $\eta_2=F_2(\xi,\bar{\xi})$) with
\begin{equation}\label{e:planeperp}
F_2(\xi,\bar{\xi})=\frac{1}{4}\left(
(1+\gamma)^2F_0(\xi_0,\bar{\xi}_0)
  -(\xi-\gamma\xi_1)^2\bar{F}_0(\xi_0,\bar{\xi}_0)
   +2(\xi_1-\xi)\gamma\;r_0(\xi_0,\bar{\xi}_0)
\right),
\end{equation}
where
\begin{equation}\label{e:xi0}
\xi_0=\frac{\xi\bar{\xi}\xi_1\bar{\xi}_1-1\pm\sqrt{(1+\xi\bar{\xi})(1+\xi_1\bar{\xi}_1)(1+\bar{\xi}\xi_1)(1+\xi\bar{\xi}_1)}}
   {\bar{\xi}(1+\xi\bar{\xi}_1)+\bar{\xi}_1(1+\bar{\xi}\xi_1)},
\end{equation}
and
\[
\gamma=\pm\sqrt{\frac{(1+\xi\bar{\xi}_1)(1+\xi\bar{\xi})}
    {(1+\bar{\xi}\xi_1)(1+\xi_1\bar{\xi}_1)}}.
\]
The two signs yield the same line congruence with opposite
orientation, and can be chosen to point in the outgoing direction.
\end{Prop}
\begin{pf}
From the reflection law (\ref{e:reflawa}) with $\xi_2=\xi$ and
$\xi_1\rightarrow-\bar{\xi}_1^{-1}$ we have
\[
\xi=\frac{(\xi_0\bar{\xi}_0-1)\xi_1+2\xi_0}
           {2\bar{\xi}_0\xi_1+1-\xi_0\bar{\xi}_0}.
\]
This can be recast as a quadratic equation for $\xi_0$, which has solution
(\ref{e:xi0}). From these, after some calculation, we find the following expressions
\[
1+\xi_0\bar{\xi}_0=\pm\frac{2\sqrt{b^2+\beta\bar{\beta}}(-b\pm\sqrt{b^2+\beta\bar{\beta}})}{\beta\bar{\beta}},
\qquad\qquad
1-\xi_0\bar{\xi}_0=\frac{2b(-b\pm\sqrt{b^2+\beta\bar{\beta}})}{\beta\bar{\beta}},
\]
\[
1+\xi\bar{\xi}_0=\frac{\beta-b\xi\pm\xi\sqrt{b^2+\beta\bar{\beta}}}{\beta},
\qquad\qquad
\xi_0-\xi=\frac{-\xi\bar{\beta}-b\pm\sqrt{b^2+\beta\bar{\beta}}}{\bar{\beta}},
\]
where we have introduced
\[
b=1-\xi\bar{\xi}\xi_1\bar{\xi}_1 \qquad\qquad
 \beta=\xi(1+\bar{\xi}\xi_1)+\xi_1(1+\xi\bar{\xi}_1).
\]
Then we compute the following combinations of the above
\[
\frac{1+\xi\bar{\xi}_0}{1+\xi_0\bar{\xi}_0}=
\frac{\pm\sqrt{(1+\xi\bar{\xi}_1)(1+\xi\bar{\xi})}+
        \sqrt{(1+\bar{\xi}\xi_1)(1+\xi_1\bar{\xi}_1)}}
 {2\sqrt{(1+\bar{\xi}\xi_1)(1+\xi_1\bar{\xi}_1)}},
\]
\[
\frac{\xi_0-\xi}{1+\xi_0\bar{\xi}_0}=
\frac{\pm\xi_1\sqrt{(1+\xi\bar{\xi}_1)(1+\xi\bar{\xi})}-
        \xi\sqrt{(1+\bar{\xi}\xi_1)(1+\xi_1\bar{\xi}_1)}}
 {2\sqrt{(1+\bar{\xi}\xi_1)(1+\xi_1\bar{\xi}_1)}},
\]
\[
\frac{(\xi_0-\xi)(1+\xi\bar{\xi}_0)}{1+\xi_0\bar{\xi}_0}=
\pm\frac{1}{2}(\xi_1-\xi)\sqrt{\frac{(1+\xi\bar{\xi}_1)(1+\xi\bar{\xi})}
   {(1+\bar{\xi}\xi_1)(1+\xi_1\bar{\xi}_1)}}.
\]
Substituting these in (\ref{e:key2}) gives the result
stated.
\end{pf}

We also have the following corollary for waves travelling down the
$x^3$-axis:

\begin{Cor}\label{c:planex3}
Suppose $S$ a surface in ${\Bbb{R}}^3$, given by the
$\eta_0=F_0(\xi,\bar{\xi})$ with potential function
$r_0(\xi,\bar{\xi})$, is struck by a plane wave moving down the
$x^3$-axis. Then the reflected wave is given by the line congruence
($\xi$, $\eta_2=F_2(\xi,\bar{\xi})$) with
\begin{equation}\label{e:planeperp1}
F_2(\xi,\bar{\xi})=\frac{1}{4}\left(
\left(1+\sqrt{1+\xi\bar{\xi}}\right)^2F_0(\xi_0,\bar{\xi}_0)
  -\xi^2\bar{F}_0(\xi_0,\bar{\xi}_0)
   -2\xi\sqrt{1+\xi\bar{\xi}}\;r_0(\xi_0,\bar{\xi}_0)
\right),
\end{equation}
where
\[
\xi_0=\frac{-1+\sqrt{1+\xi\bar{\xi}}}{\bar{\xi}}.
\]
\end{Cor}
\begin{pf}
This follows from the above Proposition \ref{t:planedir} by setting $\xi_1=0$.
\end{pf}

By way of example, we now compute the twistor function for
a plane wave  after reflection off the unit sphere and the rotationally symmetric torus.

\subsection{Reflection of a Plane Wavefront in the Unit Sphere}

By translation we can move the unit sphere to the origin in
${\Bbb{R}}^3$ and by a rotation we can set the direction of the plane
wave to be down the $x^3$-axis. Thus we can use corollary
\ref{c:planex3}.

The twistor function and potential for the unit sphere at the origin
are $F_0=0$ and $r_0=1$. Thus, substituting these in
(\ref{e:planeperp1}), the reflected wavefront is given by
\[
F_2=-\frac{1}{2}\xi\sqrt{1+\xi\bar{\xi}},
\qquad\qquad
r_2=\frac{2}{\sqrt{1+\xi\bar{\xi}}}+C.
\]
Figure 2 shows the resulting outgoing wavefronts (which are
axially symmetric, but not spherically symmetric).

\setlength{\epsfxsize}{3in}
\begin{center}
   \mbox{\epsfbox{plsphere.eps}}
\end{center}

\subsection{Reflection of a Plane Wavefront in a Torus}

Consider the torus with core radius $a$ and meridian radius $b$ which is
rotationally symmetric about the $x^3$-axis. This has twistor function and potential
\[
F_0=\frac{a}{2}(1-\xi\overline{\xi})\sqrt{\frac{\xi}{\overline{\xi}}},
\qquad\qquad
r_0=\frac{2a\sqrt{\xi\overline{\xi}}}{1+\xi\overline{\xi}}+b.
\]
In what follows we will consider the case where $a=2$ and $b=1$. We
will deal with three cases: a wave travelling down the $x^3$-axis, up
the $x^1$-axis and one striking the torus at an angle of 45$^0$ to the
vertical.

\subsubsection{Plane wavefront moving down the $x^3$-axis}
The line congruence resulting from reflection of a plane wave moving
down the $x^3$-axis can be found directly from corollary
\ref{c:planex3}. The result is
\[
F_2=\frac{2(1-\xi\overline{\xi})
             -\sqrt{\xi\bar{\xi}}\sqrt{1+\xi\bar{\xi}}}{2}\sqrt{\frac{\xi}{\overline{\xi}}},
\qquad\qquad
r_2=\frac{4\sqrt{\xi\overline{\xi}}+2\sqrt{1+\xi\bar{\xi}}}{1+\xi\overline{\xi}},
\]
where we have integrated $F_2$ to obtain $r_2$.

Figure 3 shows the complete wavefront as it leaves the
torus. Notice the annular shadow.

\setlength{\epsfxsize}{3in}
\begin{center}
   \mbox{\epsfbox{pltorus2.eps}}
\end{center}

\subsubsection{Plane wavefront moving up the $x^1$-axis}
In order to determine the reflection of a plane wave approaching from
another direction we shall use Proposition \ref{t:planepar}. If the
direction of the incoming wave is $\xi_1$, substitution of the torus
twistor function and potential in (\ref{e:planewave2}) gives
\begin{equation}\label{e:pltorus1}
\eta_2=\frac{[(\bar{\xi}_0-\bar{\xi}_1)^2\xi_0
-(1+\xi_0\bar{\xi}_1)^2\bar{\xi}_0](1-\xi_0\bar{\xi}_0)
+(\bar{\xi}_0-\bar{\xi}_1)(1+\xi_0\bar{\xi}_1)
     [(1+\xi_0\bar{\xi}_0)\sqrt{\xi_0\bar{\xi}_0}+4\xi_0\bar{\xi}_0]}
{\sqrt{\xi_0\bar{\xi}_0}((1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0)^2}.
\end{equation}
Integrating this gives the potential function
\begin{equation}\label{e:pltorus2}
r_2=\frac{4[2(|\bar{\xi}_0-\bar{\xi}_1|^2
-|1+\xi_0\bar{\xi}_1|^2)\sqrt{\xi_0\bar{\xi}_0}+
+(\xi_0\bar{\xi}_0(1-\xi_1\bar{\xi}_1)-\bar{\xi}_0\xi_1-\xi_0\bar{\xi}_1)
     (1+\xi_0\bar{\xi}_0)]}
{(1+\xi_1\bar{\xi}_1)(1+\xi_0\bar{\xi}_0)^2}.
\end{equation}

For a wave travelling along the $x^1$-axis we set $\xi_1=1$. The
resulting wavefront is shown in Figure 4.

\setlength{\epsfxsize}{3in}
\begin{center}
   \mbox{\epsfbox{toruside.eps}}
\end{center}

\subsubsection{Plane wavefront at an angle of 45$^0$ to the vertical}
Finally, a portion of the reflected wavefront generated by an incident
wave making an angle of 45$^0$ with the $x^3$-axis is shown in Figure 5. This is obtained by setting $\xi_1=2.4$ in (\ref{e:pltorus1})
and (\ref{e:pltorus2}).

\setlength{\epsfxsize}{3in}
\begin{center}
   \mbox{\epsfbox{pltorus45.eps}}
\end{center}

\section{Reflection of a Spherical Wavefront}

Assume that the wavefront is spherical, that is, the rays have a
single focus. By a translation we can move this focus to the origin
and then the wavefront is simply given by $\eta_1=0$. Every point in
${\Bbb{R}}^3$, other than the origin, is contained on two oriented
lines in the congruence (the same line with both orientations).

\begin{Prop}\label{t:sphwave}
A spherical wavefront, with focus the origin, reflected off a surface
(not containing the origin) determined by $\xi_0(\nu,\bar{\nu})$, $\eta_0(\nu,\bar{\nu})$ and $r_0(\nu,\bar{\nu})$ gives rise to the congruence
\begin{equation}\label{e:spherical1}
\xi_2=\frac{2\eta_0+2\bar{\eta}_0\xi_0^2\pm2\xi_0\beta_0}{2 (\xi_0\bar{\eta}_0-\bar{\xi}_0\eta_0)-(1+\xi_0\bar{\xi}_0)^2r_0\pm(1-\xi_0\bar{\xi}_0)\beta_0 },
\end{equation}
\begin{equation}\label{e:spherical2}
\eta_2=\alpha_1^2\eta_0-\alpha_2^2\bar{\eta}_0-2(1+\xi_0\bar{\xi}_0)\alpha_3r_0,
\end{equation}
where
\[
\alpha_1=\frac{2\bar{\eta}_0\xi_0-(1+\xi_0\bar{\xi}_0)r_0\pm\beta_0 }{2(\xi_0\bar{\eta}_0-\bar{\xi}_0\eta_0)
 -(1+\xi_0\bar{\xi}_0)^2r_0\pm(1-\xi_0\bar{\xi}_0)\beta_0 },
\]
\[
\alpha_2=\frac{2\eta_0+\xi_0(1+\xi_0\bar{\xi}_0)r_0\pm\xi_0\beta_0 }{2(\xi_0\bar{\eta}_0-\bar{\xi}_0\eta_0)
 -(1+\xi_0\bar{\xi}_0)^2r_0\pm(1-\xi_0\bar{\xi}_0)\beta_0 },
\]
\[
\alpha_3=\frac{4\eta_0\bar{\eta}_0\xi_0-(\eta_0-\bar{\eta}_0\xi_0^2)(1+\xi_0\bar{\xi}_0)r_0\pm(\eta_0+\bar{\eta}_0\xi_0^2)\beta_0 }{(2(\xi_0\bar{\eta}_0-\bar{\xi}_0\eta_0)
 -(1+\xi_0\bar{\xi}_0)^2r_0\pm(1-\xi_0\bar{\xi}_0)\beta_0 )^2},
\]
and
\[
\beta_0=\sqrt {4 \eta_0 \bar{\eta}_0+(1+\xi_0\bar{\xi}_0)^2r_0^2}.
\]
Here the two different signs give the same line congruence with the
opposite orientation, and can be chosen to point in the outgoing direction.

\end{Prop}
\begin{pf}

Setting $\eta_1=0$ in (\ref{e:key1}) we get a quadratic equation for
$\xi_1$, with solution:
\[
\xi_1=\frac{2(\eta_0\bar{\xi}_0+\bar{\eta}_0\xi_0)
 -(1-\xi^2_0\bar{\xi}_0^2)r_0 \pm(1+\xi_0\bar{\xi}_0)\beta_0}
{2(\bar{\eta}_0-\eta_0\bar{\xi}_0^2)+2\bar{\xi}_0(1+\xi_0\bar{\xi}_0)r_0}.
\]
Inserting this in (\ref{e:reflawa}) yields the expression for $\xi_2$
in the theorem. In addition we find that
\[
\bar{\xi}_1-\bar{\xi}_0=\frac{(2\bar{\eta}_0\xi_0-(1+\xi_0\bar{\xi}_0)r_0\pm\beta_0 )(1+\xi_0\bar{\xi}_0)}{2(\eta_0-\bar{\eta}_0\xi_0^2)+2\xi_0(1+\xi_0\bar{\xi}_0)r_0},
\]
\[
1+\xi_0\bar{\xi}_1=\frac{(2\eta_0+\xi_0(1+\xi_0\bar{\xi}_0)r_0\pm\xi_0\beta_0 )(1+\xi_0\bar{\xi}_0)}{2(\eta_0-\bar{\eta}_0\xi_0^2)+2\xi_0(1+\xi_0\bar{\xi}_0)r_0},
\]
while
\[
(1-\xi_0\bar{\xi}_0)\bar{\xi}_1-2\bar{\xi}_0=\frac{(2(\xi_0\bar{\eta}_0-\bar{\xi}_0\eta_0)
 -(1+\xi_0\bar{\xi}_0)^2r_0\pm(1-\xi_0\bar{\xi}_0)\beta_0 )(1+\xi_0\bar{\xi}_0)}{2(\eta_0-\bar{\eta}_0\xi_0^2)+2\xi_0(1+\xi_0\bar{\xi}_0)r_0}.
\]
Substituting these in (\ref{e:key2}) completes the theorem.
\end{pf}

\subsection{Reflection of a Spherical Wavefront in the Unit Sphere}

Consider the unit sphere, centred at (0,0,$-$2). This is determined by

\[
\eta_0=2\xi_0, \qquad \qquad r_0=1-2\frac{1-\xi_0\bar{\xi}_0}{1+\xi_0\bar{\xi}_0}.
\]
Thus
\[
\beta_0=\sqrt{1+10\xi_0\bar{\xi}_0+r\xi_0^2\bar{\xi}_0^2},
\]
and by (\ref{e:spherical1})
\[
\xi_2=\frac{2\xi_0(2(1+\xi_0\bar{\xi}_0)+\beta_0)}
  {1-2\xi_0\bar{\xi}_0-3\xi_0^2\bar{\xi}_0^2+(1-\xi_0\bar{\xi}_0)\beta_0},
\]
where we have chosen the $+$ sign in the equations. Further
straightforward, if lengthy, calculations establish that
\[
\alpha_1=\frac{1+\xi_0\bar{\xi}_0+\beta_0}{1-2\xi_0\bar{\xi}_0-3\xi_0^2\bar{\xi}_0^2+\beta_0},
\qquad\qquad
\alpha_2=\frac{\xi_0(3(1+\xi_0\bar{\xi}_0)+\beta_0)}{1-2\xi_0\bar{\xi}_0-3\xi_0^2\bar{\xi}_0^2+\beta_0},
\]
\[
\alpha_3=\frac{\xi_0(1+\xi_0\bar{\xi}_0+\beta_0)}{(1-2\xi_0\bar{\xi}_0-3\xi_0^2\bar{\xi}_0^2+\beta_0)^2}.
\]
Finally, substitution of these in (\ref{e:spherical2}) gives
\[
\eta_2=\frac{4 \xi_0(1-3\xi_0\bar{\xi}_0)(1+3 \xi_0\bar{\xi}_0+ \sqrt {1+10 \xi_0\bar{\xi}_0+9 \xi_0^{2} \bar{\xi}_0^{2}} )}{1 +\xi_0 \bar{\xi}_0 -7 \xi_0^{2} \bar{\xi}_0^{2}+9 \xi_0^{3} \bar{\xi}_0^{3}+(1-4\xi_0 \bar{\xi}_0+3 \xi_0^{2} \bar{\xi}_0^{2})\sqrt {1+10 \xi_0 \bar{\xi}_0+ 9 \xi_0^{2} \bar{\xi}_0^{2}} }.
\]
To find the potential function $r_2$ we invert (\ref{e:pot}) with
$\nu=\xi_0$, since we are parameterising the outgoing rays by the
direction of the normal to the surface at the point of
intersection. After some computation we obtain
\[
r_2=\frac{-2(1-3\xi_0 \bar{\xi}_0)^2\sqrt {1+10 \xi_0 \bar{\xi}_0+ 9
    \xi_0^{2} \bar{\xi}_0^{2}}}{1+11 \xi_0 \bar{\xi}_0+19 \xi_0^{2} \bar{\xi}_0^{2}+ 9\xi_0^{3} \bar{\xi}_0^{3}}+C.
\]

At this juncture we have found parametric expressions for $\xi_2$,
$\eta_2$ and $r_2$, that is, the complete description of the outgoing
wave. If we graph the wavefronts the results are similar to the plane
wave reflected off the sphere. By way of comparison, Figure 6
compares a cross-section of the two wavefronts in a plane containing
the $x^3$-axis. The shaded area represents the shadow cast by the surface.

\setlength{\epsfxsize}{4in}
\begin{center}
   \mbox{\epsfbox{plvssp.eps}}
\end{center}

config: arxiv