Theory Affine

(*
   Mike Stannett
   Feb 2023
*)

section ‹ Affine ›

text ‹This theory defines affine transformations and established their
key properties.›

theory Affine
  imports Translations LinearMaps
begin


class Affine = Translations + LinearMaps
begin



abbreviation affine :: "('a Point ⇒ 'a Point) ⇒ bool" 
  where "affine A ≡ ∃ L T . (linear L) ∧ (translation T) ∧ (A = T ∘ L)"


abbreviation affInvertible :: "('a Point ⇒ 'a Point) ⇒ bool"
  where "affInvertible A ≡ affine A ∧ invertible A"


abbreviation isLinearPart :: "('a Point ⇒ 'a Point) ⇒ ('a Point ⇒ 'a Point) ⇒ bool"
  where "isLinearPart A L ≡ (affine A) ∧ (linear L) ∧ 
          (∃ T. (translation T ∧ A = T ∘ L))"

abbreviation isTranslationPart  :: "('a Point ⇒ 'a Point) ⇒ ('a Point ⇒ 'a Point) ⇒ bool"
  where "isTranslationPart A T ≡ (affine A) ∧ (translation T) ∧ 
          (∃ L. (linear L ∧ A = T ∘ L))"

(* affine approximation *)

subsection ‹ Affine approximation ›

text ‹A key concept in the proof is affine approximation. We will eventually 
assert that worldview transformation can be approximated by invertible affine 
transformations.›

abbreviation affineApprox :: "('a Point ⇒ 'a Point) ⇒ 
                           ('a Point ⇒ 'a Point => bool) ⇒
                            'a Point ⇒ bool"
  where "affineApprox A f x ≡ (isFunction f) ∧ 
           (affInvertible A) ∧ (diffApprox (asFunc A) f x)"


fun applyAffineToLine :: "('a Point ⇒ 'a Point) 
                ⇒ 'a Point set ⇒ 'a Point set ⇒ bool"
  where "applyAffineToLine A l l' ⟷ (affine A) ∧ 
    (∃ T L b d . ((linear L) ∧ (translation T) ∧ (A = T ∘ L) ∧
       (l = line b d) ∧ (l' = (line (A b) (L d)))))"


(* miscellaneous *)

abbreviation affConstantOn ::  "('a Point ⇒ 'Point) ⇒ 'a Point ⇒ 'a Point set ⇒ bool"
  where "affConstantOn A x s ≡ (∃ε>0. ∀y∈s. (y within ε of x) ⟶ ((A y) = (A x)))"


(* ****************************************************************** *)
(* LEMMAS *)

lemma lemTranslationPartIsUnique:
  assumes "isTranslationPart A T1"
and       "isTranslationPart A T2"
shows     "T1 = T2"
proof -
  obtain L1 where T1: "linear L1 ∧ A = T1 ∘ L1" using assms(1) by auto 
  obtain L2 where T2: "linear L2 ∧ A = T2 ∘ L2" using assms(2) by auto 
  obtain t1 where t1: "∀ x. T1 x = (x ⊕ t1)" using assms(1) by auto
  obtain t2 where t2: "∀ x. T2 x = (x ⊕ t2)" using assms(2) by auto

  have "T1 origin = A origin" using T1 assms(1) by auto
  also have  "... = T2 origin" using T2 assms(2) by auto
  finally have "T1 origin = T2 origin" by auto
  hence "t1 = t2" using t1 t2 by auto
  hence "∀ x. (T1 x = T2 x)" using t1 t2 by auto
  thus ?thesis by auto
qed



lemma lemLinearPartIsUnique:
  assumes "isLinearPart A L1"
and       "isLinearPart A L2"
shows     "L1 = L2"
proof -
  obtain T1 where T1: "translation T1 ∧ A = T1 ∘ L1" using assms(1) by auto
  obtain T2 where T2: "translation T2 ∧ A = T2 ∘ L2" using assms(2) by auto

  have 1: "isTranslationPart A T1" using assms(1) T1 by auto
  have 2: "isTranslationPart A T2" using assms(2) T2 by auto
  hence T1T2: "T1 = T2" using 1 2 lemTranslationPartIsUnique[of "A" "T1" "T2"] by auto

  obtain t where t: "∀ x. T1 x = (x ⊕ t)" using T1 by auto
  define T where "T = mkTranslation (origin ⊖ t)" 
  hence 3: "T ∘ A = L1" using T1 t lemInverseTranslation by auto
  have "T ∘ A = L2" using T_def T2 t T1T2 lemInverseTranslation by auto

  thus ?thesis using 3 by auto
qed


lemma lemLinearImpliesAffine:
assumes "linear L"
shows "affine L"
proof - 
  have 1: "L = id ∘ L" by fastforce
  thus ?thesis using assms lemIdIsTranslation by blast
qed


lemma lemTranslationImpliesAffine:
assumes "translation T"
shows "affine T"
proof - 
  have "T = T ∘ id" by force
  thus ?thesis using assms lemIdIsLinear by blast
qed


lemma lemAffineDiff:
  assumes "linear L"
and       "∃ T . ((translation T) ∧ (A = T ∘ L))"
  shows "((A p) ⊖ (A q)) = L (p ⊖ q)"
proof -
  obtain T where T: "(translation T) ∧ (A = T ∘ L)" using assms(2) by auto
  thus ?thesis using assms(1) by auto
qed


lemma lemAffineImpliesTotalFunction:
  assumes "affine A"
  shows "isTotalFunction (asFunc A)"
  by simp


lemma lemAffineEqualAtBase:
  assumes "affineApprox A f x"
  shows   "∀y. (f x y) ⟷ (y = A x)"
proof -
  have diff: "diffApprox (asFunc A) f x" using assms(1) by simp
  { fix y
    assume y: "f x y"
    hence "f x y ∧ (asFunc A) x (A x)" by auto
    hence "A x = y" using diff lemApproxEqualAtBase[of "f" "x" "asFunc A" "y"]
      by auto
  }
  hence l2r: "∀y . f x y ⟶ y = A x" by auto

  { obtain y where y: "f x y" using diff by auto
    hence "y = A x" using l2r by auto
    hence "f x (A x)" using y by auto
  }
  thus ?thesis using l2r by blast
qed


lemma lemAffineOfPointOnLine:
  assumes "(linear L) ∧ (translation T) ∧ (A = T ∘ L)"
and       "x = (b ⊕ (a⊗d))"
  shows   "A x = ((A b) ⊕ (a ⊗ (L d)))"
proof -
  have "(L x = ((L b) ⊕ (L (a ⊗ d)))) ∧ (L (a ⊗ d) = (a ⊗ (L d)))" 
    using assms by blast
  hence "A x = T ((L b) ⊕ (a ⊗ (L d)))" using assms(1) by auto
  also have "... = ((T (L b)) ⊕ (a ⊗ (L d)))" 
    using assms(1) lemTranslationSum[of "T" "L b" "a ⊗ (L d)"] by auto
  finally show ?thesis using assms(1) by auto
qed



(* applyAffineToLine takes for granted that the image of a line is a line.
   We need to prove that this is true *)
lemma lemAffineOfLineIsLine: 
  assumes "isLine l"
  shows "(applyAffineToLine A l l')  ⟷  (affine A ∧ l' = applyToSet (asFunc A) l)"
proof - 
  { assume lhs: "applyAffineToLine A l l'"
    hence affA: "affine A" by fastforce
    have "∃ T L b d . (linear L) ∧ (translation T) ∧ (A = T ∘ L) ∧
       (l = line b d) ∧ (l' = (line (A b) (L d)))" using lhs by auto
    then obtain T L b d where TL: "(linear L) ∧ (translation T) ∧ (A = T ∘ L) ∧
       (l = line b d) ∧ (l' = (line (A b) (L d)))"
      using lhs by blast
    { fix p'
      { assume "p' ∈ l'"
        then obtain a where a: "p' = ( (A b) ⊕ (a ⊗ (L d)) )" using TL by auto
        define p where p: "p = (b ⊕ (a⊗d))"
        hence "p' ∈ applyToSet (asFunc A) l" using a TL lemAffineOfPointOnLine by auto
      }
      hence "(p' ∈ l') ⟶ (p' ∈ applyToSet (asFunc A) l)" by auto
    }
    hence l2r: "l' ⊆ (applyToSet (asFunc A) l)" by auto

    { fix p'
      { assume "p' ∈ applyToSet (asFunc A) l"
        then obtain p where p: "p ∈ l ∧ p' = A p" by auto
        then obtain a where a: "p = (b ⊕ (a⊗d))" using TL by auto
        hence "A p = ((A b) ⊕ (a ⊗ (L d)))" using TL lemAffineOfPointOnLine by auto
        hence "p' ∈ l'" using TL p by auto
      }
      hence "(p' ∈ applyToSet (asFunc A) l) ⟶ (p' ∈ l')" using l2r by auto
    }
    hence "(applyToSet (asFunc A) l) ⊆ l'" by auto
    hence "affine A ∧ l' = applyToSet (asFunc A) l" using affA l2r by auto
  }
  hence rtp1: "(applyAffineToLine A l l') ⟶ (affine A ∧ l' = applyToSet (asFunc A) l)"
    by blast

  { assume rhs: "(affine A) ∧ (l' = applyToSet (asFunc A) l)"

    obtain b d where bd: "l = line b d" using assms(1) by auto
    obtain T L where TL: "(linear L) ∧ (translation T) ∧ (A = T ∘ L)"
      using rhs by auto

    { fix p'
      assume "p' ∈ l'"
      then obtain p where p: "(p ∈ l) ∧ (A p = p')" using rhs by auto
      then obtain a where a: "p = (b ⊕ (a⊗d))" using bd by auto
      hence "A p = ((A b) ⊕ (a ⊗ (L d)))" 
        using TL lemAffineOfPointOnLine by auto
      hence "p' ∈ line (A b) (L d)" using  p by auto
    }
    hence l2r: "l' ⊆ line (A b) (L d)" by force

    { fix p'
      assume "p' ∈ line (A b) (L d)"
      then obtain a where a: "p' = ( (A b) ⊕ (a ⊗ (L d)) )" using TL by auto
      define p where p: "p = (b ⊕ (a⊗d))"
      hence "A p = ((A b) ⊕ (a ⊗ (L d)))" 
        using TL lemAffineOfPointOnLine by auto
      hence "A p = p'" using a by simp
      hence "p' ∈ applyToSet (asFunc A) l" using p bd by auto
    }
    hence "line (A b) (L d) = l'" using rhs l2r by blast

    hence "applyAffineToLine A l l'" using TL bd by auto
  }
  hence "(affine A) ∧ (l' = applyToSet (asFunc A) l) 
                   ⟶ (applyAffineToLine A l l')"
    by blast

  thus ?thesis using rtp1 by blast
qed
      
      

lemma lemOnLineUnderAffine:
  assumes "(affine A) ∧ (onLine p l)"
shows     "onLine (A p) (applyToSet (asFunc A) l)"
proof -

  define l' where l': "l' = applyToSet (asFunc A) l"
  have lineL: "isLine l" using assms by auto

  hence Tll': "applyAffineToLine A l l'" 
    using lemAffineOfLineIsLine[of "l" "A" "l'"] assms l'
    by blast
  hence "∃ T' L b d . (linear L) ∧ (translation T') ∧ (A = T' ∘ L) ∧
       (l = line b d) ∧ (l' = (line (A b) (L d)))" by force
  then obtain T' L b d 
    where TLbd: "(linear L) ∧ (translation T') ∧ (A = T' ∘ L) ∧
       (l = line b d) ∧ (l' = (line (A b) (L d)))" by blast
  then obtain a where a: "p = (b ⊕ (a⊗d))" using assms by auto

  hence "A p = ((A b) ⊕ (a ⊗ (L d)))" using lemAffineOfPointOnLine TLbd by auto
  thus ?thesis using l' TLbd by blast
qed



lemma lemLineJoiningUnderAffine:
  assumes "affine A"
  shows   "applyToSet (asFunc A) (lineJoining p q) = lineJoining (A p) (A q)"
proof - 
  obtain T L where TL: "translation T ∧ linear L ∧ A = T∘L" using assms(1) by auto
  hence "((A q) ⊖ (A p)) = L (q⊖p)" by auto

  { fix a
    have "(a⊗((A q) ⊖ (A p))) = L (a ⊗ (q⊖p))" 
      using TL lemLinearProps[of "L" "a" "q⊖p"] by force
  }
  hence as: "∀a. (a⊗((A q) ⊖ (A p))) = L (a ⊗ (q⊖p))" by auto

  { fix x'
    assume "x' ∈ applyToSet (asFunc A) (lineJoining p q)"
    then obtain x where x: "x ∈ (lineJoining p q) ∧ x' = A x" by force
    then obtain a where a: "x = (p ⊕ (a⊗(q⊖p)))" by force

    have expandL: "L (p ⊕ (a⊗(q⊖p))) = ((L p) ⊕ (L (a⊗(q⊖p))))" 
      using TL lemLinearProps[of "L" "0" "p" "(a⊗(q⊖p))"]     
      by fast

    have "x' = A (p ⊕ (a⊗(q⊖p)))" using x a by fast
    also have "... = (T (L (p ⊕ (a⊗(q⊖p)))))" using TL by force
    also have "... = T ((L p) ⊕ (L (a⊗(q⊖p))))" using expandL by force
    finally have "x' = ((T (L p)) ⊕ (L (a⊗(q⊖p))))"
      using TL lemTranslationSum[of "T" "L p" "L (a⊗(q⊖p))"]
      by auto
    hence "x' ∈ lineJoining (A p) (A q)" using TL as by auto
  }
  hence l2r: "applyToSet (asFunc A) (lineJoining p q) ⊆ lineJoining (A p) (A q)" 
    by force

  { fix x'
    assume "x' ∈ lineJoining (A p) (A q)"
    hence "∃a . x' = ((T (L p)) ⊕ (a⊗((A q)⊖(A p))))" 
      using TL by auto
    then obtain a where a: "x' = ((T (L p)) ⊕ (a⊗((A q)⊖(A p))))" 
      using TL by fast
    hence "x' = ((T (L p)) ⊕ (L (a⊗(q⊖p))))" using as by force
    also have "... = T ( (L p) ⊕ (L (a⊗(q⊖p))))" 
      using TL lemTranslationSum[of "T" "L p" "L (a⊗(q⊖p))"] by simp
    also have "... = T ( L (p ⊕ (a⊗(q⊖p))) )"
      using TL lemLinearProps[of "L" "0" "p" "a⊗(q⊖p)"] by auto
    finally have "x' = A (p ⊕ (a⊗(q⊖p)))" using TL by auto
    hence "x' ∈ applyToSet (asFunc A) (lineJoining p q)" by auto
  }
  thus ?thesis using l2r by auto
qed




lemma lemAffineIsCts:
  assumes "affine A"
  shows   "cts (asFunc A) x"
proof -
  
  have "∃ T L . (translation T)∧(linear L)∧(A = T ∘ L)" using assms by auto
  then obtain T L where TL: "(translation T)∧(linear L)∧(A = T ∘ L)" by auto

  define f where f: "f = asFunc L"
  define g where g: "g = asFunc T"
  have 1: "cts f x" using f TL lemLinearIsCts[of "L" "x"] by auto
  have 2: "∀y. (f x y) ⟶ (cts g y)" 
    using f g TL lemTranslationIsCts[of "T" "x"] by auto
  have "cts (composeRel g f) x" using 1 2 lemCtsOfCtsIsCts[of "f" "x" "g"] by simp
  thus ?thesis using f g TL by auto
qed

 
lemma lemAffineContinuity:
  assumes "affine A"
  shows "∀ x. ∀ε>0. ∃δ>0 . ∀p. (p within δ of x) ⟶ ((A p) within ε of (A x))"
proof -
  { fix x 
    { fix e
      assume epos: "e > 0"
  
      have "(asFunc A) x (A x) ∧ (cts (asFunc A) x)" 
        using assms lemAffineIsCts[of "A" "x"] by auto
      hence u: "(∀ε>0. ∃δ>0. (applyToSet (asFunc A) (ball x δ)) ⊆ ball (A x) ε)"
        by force
      then obtain d where d: "(d > 0) ∧ 
                            (applyToSet (asFunc A) (ball x d)) ⊆ ball (A x) e"
        using epos by force
  
      { fix p
        assume "p within d of x"
        hence "(A p) within e of (A x)" using d lemSep2Symmetry by force
      }
      hence "∃d>0 . ∀p. (p within d of x) ⟶ ((A p) within e of (A x))"
        using d by auto
    }
    hence "∀e>0. ∃d>0 . ∀p. (p within d of x) ⟶ ((A p) within e of (A x))"
      by auto
  }
  thus ?thesis by auto
qed


lemma lemAffOfAffIsAff:
  assumes "(affine A) ∧ (affine B)"
shows     "affine (B ∘ A)"
proof - 
  obtain TA LA TB LB where props: 
            "translation TA ∧ linear LA ∧ translation TB ∧ linear LB ∧
                 A = TA ∘ LA  ∧  B = TB ∘ LB" using assms by blast
  then obtain ta tb where ts: "(∀p. TA p = (p ⊕ ta)) ∧ (∀p. TB p = (p ⊕ tb))" by auto

  { fix p
    have "(B ∘ A) p = ((LB ( (LA p) ⊕ ta )) ⊕ tb)" using props ts by force
    also have "... = (((LB (LA p)) ⊕ (LB ta)) ⊕ tb)" using props by force
    also have "... = (((LB∘LA) p) ⊕ ((LB ta)⊕tb))" using add_assoc by force
    finally have "(B ∘ A) p = ((mkTranslation ((LB ta)⊕tb)) ∘ (LB∘LA)) p" by force
  }
  hence BA: "(B ∘ A) = (mkTranslation ((LB ta)⊕tb)) ∘ (LB∘LA)" by auto

  define T where T: "T = mkTranslation ((LB ta)⊕tb)"
  hence trans: "translation T" using lemMkTrans by blast
  define L where L: "L = (LB∘LA)"
  hence lin: "linear L" using lemLinOfLinIsLin[of "LA" "LB"] props by auto

  hence "(translation T) ∧ (linear L) ∧ ((B∘A) = (T∘L))" using T L trans lin BA by auto
  thus ?thesis by auto
qed



lemma lemInverseAffine:
  assumes "affInvertible A"
shows     "∃A' . (affine A') ∧ (∀ p q . A p = q ⟷ A' q = p)"
proof -
  obtain A' where A': "(∀ p q. A p = q ⟷ A' q = p)" 
    using assms by metis

(*  Have A = T o L,  so want to show that  A' =  L' o T' 

    First have to show that L is invertible, so we can obtain linear L'.
    Use the fact that L = T' o A.
*)
  obtain T L where TL: "translation T ∧ linear L ∧ (A = T ∘ L)" using assms(1) by auto

  obtain T' where T': "(translation T') ∧ (∀ p q . T p = q ⟷ T' q = p)" 
    using TL lemInverseTrans[of "T"] by auto

  { fix p
    { fix q
      assume Ap: "A p = q"
      hence  "T (L p) = q" using TL by auto
      hence  "L p = T' q" using T' by auto
      hence  "L  p = (T' ∘ A) p" using Ap by auto
    }
  }
  hence L: "L = (T' ∘ A)" by auto

  { fix q
    obtain r where r: "(T' r = q)" using T' by auto
    then obtain p where p: "(A p = r) ∧ (∀x. A x = r ⟶ x = p)" using A' by auto
    hence 1: "L p = q" using L r by auto
    { fix x
      assume "L x = q"
      hence "T' (A x) = q" using L by auto
      hence "A x = r" using r T' lemTranslationInjective[of "T'"] by force
      hence "x = p" using p A' by blast
    } hence "∃p . (L p = q) ∧ (∀x. L x = q ⟶ x = p)" using 1 by auto
  }
  hence invL: "invertible L" by blast

  then obtain L' where L': "(linear L') ∧ (∀ p q . L p = q ⟷ L' q = p)" 
    using TL lemInverseLinear[of "L"] by blast

  (* Main section of proof *)
  { fix p q
    have "A' q = p  ⟷  T (L p) = q" using A' TL by auto
    also have "...  ⟷  T' q = L p" using T' by auto
    also have "...  ⟷  L p = T' q" by auto
    also have "...  ⟷  L' (T' q) = p" using L' by auto
    finally have "A' q = p  ⟷  (L'∘T') q = p" by auto
  }
  hence "A' = L' ∘ T'" by auto
  hence "affine A'" using lemAffOfAffIsAff[of "T'" "L'"]
                          lemTranslationImpliesAffine[of "T'"] T'
                          lemLinearImpliesAffine[of "L'"] L'
    by auto

  thus ?thesis using A' by auto
qed



lemma lemAffineApproxDomainTranslation:
  assumes "translation T"
and       "affineApprox A f x"
and       "∀ p q . T p = q  ⟷  T' q = p"
shows     "affineApprox (A∘T) (composeRel f (asFunc T)) (T' x)"
proof -

  define A0 where A0: "A0 = A ∘ T"
  define g where g: "g = composeRel f (asFunc T)"

  have ToT': "∀ p . T (T' p) = p" using assms(3) by force
  have T'oT: "∀ p . T' (T p) = p" using assms(3) by force
  obtain t where t: "∀ p . T p = (p ⊕ t)" using assms(1) by force 
  hence mkT: "T = mkTranslation t" by force

  { fix p q
    have "T' p = q  ⟷  T q = p" using assms(3) by auto
    also have "... ⟷ (q ⊕ t) = p" using t by auto
    also have "... ⟷ q = (p ⊕ (origin ⊖ t))" by force
    finally have "T' p = q  ⟷  q = (p ⊕ (origin ⊖ t))" by force
    hence "T' p = q  ⟷  q = mkTranslation (origin ⊖ t) p" by force
  }
  hence mkT': "T' = mkTranslation (origin ⊖ t)" by force
  hence transT': "translation T'" using lemMkTrans by blast

  (* 3a: isFunction g *)
  have funcF: "isFunction f" using assms(2) by auto
  hence rtp3a: "isFunction g" using g by auto

  (* 3b: affine A0 *)
  have affA: "affine A" using assms(2)  by auto
  hence rtp3b: "affine A0" 
    using lemAffOfAffIsAff[of "T" "A"] lemTranslationImpliesAffine[of "T"]
          A0 affA assms(1)
    by blast

  (* 3c: invertible A0 *)
  { fix q
    obtain p where p: "(A p = q) ∧ (∀x. A x = q ⟶ x = p)" using assms(2) by blast
    define p0 where p0: "p0 = T' p"
    hence Tp0: "T p0 = p" using assms(3) by blast
    hence 1: "A0 p0 = q" using A0 p by auto
    { fix x
      assume "A0 x = q"
      hence  "T x = p" using A0 p by fastforce
      hence  "x = p0" using Tp0 assms(1) lemTranslationInjective[of "T"] by force
    }
    hence "∀x. A0 x = q ⟶ x = p0" by auto

    hence "∃p0. (A0 p0 = q) ∧ (∀x. A0 x = q ⟶ x = p0)" using 1 by auto
  }
  hence rtp3c: "invertible A0" by auto

  (* 3d: diffApprox (asFunc A0) g origin *)
  have "diffApprox (asFunc A) f x" using assms(2) by auto
  hence dAx: "(definedAt f x) ∧
    (∀ ε > 0 . (∃ δ > 0 . (∀ y .
      ( (y within δ of x)
        ⟶ 
        ( (definedAt f y) ∧ (∀ u v . (f y u ∧ (asFunc A) y v) ⟶
         ( sep2 v u ) ≤ (sqr ε) * sep2 y x )))  )
  ))" by blast
  hence "(definedAt f x) ∧ (x = T (T' x))" using assms(1) ToT' by auto
  hence rtp3d1: "(definedAt g (T' x))" using g by auto 

  { fix e
    assume epos: "e > 0"
    then obtain d where d: "(d > 0) ∧ (∀ y .
      ( (y within d of x)
        ⟶ 
        ( (definedAt f y) ∧ (∀ u v . (f y u ∧ (asFunc A) y v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 y x )))  )"
      using dAx by force
    { fix y
      assume "y within d of (T' x)"
      hence "(T y) within d of (T (T' x))" using assms(1) lemBallTranslation by auto
      hence "(T y) within d of x" using ToT' by auto
      hence "(definedAt f (T y)) ∧ (∀ u v . (f (T y) u ∧ (asFunc A) (T y) v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 (T y) x )"
        using d by blast
      hence "(definedAt g y) ∧ (∀ u v . (g y u ∧ (asFunc A0) y v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 (T y) x )" using g A0 by auto
      hence "(definedAt g y) ∧ (∀ u v . (g y u ∧ (asFunc A0) y v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 y (T' x) )" 
        using transT' lemTranslationPreservesSep2[of "T'" "T y" "x"]  T'oT
        by auto
    }
    hence "∃d > 0. ∀y . (y within d of (T' x)) ⟶ 
             (definedAt g y) ∧ (∀ u v . (g y u ∧ (asFunc A0) y v) ⟶
                   ( sep2 v u ) ≤ (sqr e) * sep2 y (T' x) )"
      using d by fast
  }
  hence rtp3d2: "∀e>0. ∃d > 0. ∀y . (y within d of (T' x)) ⟶ 
             (definedAt g y) ∧ (∀ u v . (g y u ∧ (asFunc A0) y v) ⟶
                   ( sep2 v u ) ≤ (sqr e) * sep2 y (T' x) )"
    by auto
  hence rtp3d: "diffApprox (asFunc A0) g (T' x)" using rtp3d1 by fast

  have rtp3: "affineApprox A0 g (T' x)" using rtp3a rtp3b rtp3c rtp3d by blast

  thus ?thesis using A0 g by fast
qed



lemma lemAffineApproxRangeTranslation:
  assumes "translation T"
and       "affineApprox A f x"
shows     "affineApprox (T∘A) (composeRel (asFunc T) f) x"
proof -

  define A0 where A0: "A0 = T ∘ A"
  define g where g: "g = composeRel (asFunc T) f"

  obtain T' where T': "(translation T') ∧ (∀ p q . T p = q ⟷ T' q = p)"
    using assms(1) lemInverseTrans[of "T"] by auto


  have ToT': "∀ p . T (T' p) = p" using T' by force
  have T'oT: "∀ p . T' (T p) = p" using T' by force
  obtain t where t: "∀ p . T p = (p ⊕ t)" using assms(1) by auto 
  hence mkT: "T = mkTranslation t" by auto

  { fix p q
    have "T' p = q  ⟷  T q = p" using T' by auto
    also have "... ⟷ (q ⊕ t) = p" using t by auto
    also have "... ⟷ q = (p ⊕ (origin ⊖ t))" by force
    finally have "T' p = q  ⟷  q = (p ⊕ (origin ⊖ t))" by force
    hence "T' p = q  ⟷  q = mkTranslation (origin ⊖ t) p" by force
  }
  hence mkT': "T' = mkTranslation (origin ⊖ t)" by auto
  hence transT': "translation T'" using lemMkTrans by blast

  (* 3a: isFunction g *)
  have funcF: "isFunction f" using assms(2) by auto
  hence rtp3a: "isFunction g" using g by auto

  (* 3b: affine A0 *)
  have affA: "affine A" using assms(2)  by auto
  hence rtp3b: "affine A0" 
    using lemAffOfAffIsAff[of "A" "T"] lemTranslationImpliesAffine[of "T"]
          A0 affA assms(1)
    by blast

  (* 3c: invertible A0 *)
  { fix q
    obtain p where p: "(A p = T' q) ∧ (∀x. A x = T' q ⟶ x = p)" using assms(2) by blast
    hence "T' q = A p" by auto
    hence "T (A p) = q" using T' ToT' by auto
    hence 1: "A0 p = q" using A0 by auto

    { fix x
      assume "A0 x = q"
      hence  "T (A x) = q" using A0 by auto
      hence  "T' (T (A x)) = T' q" by auto
      hence  "A x = T' q" using T'oT by auto
      hence  "x = p" using p by auto
    }
    hence "∀x. A0 x = q ⟶ x = p" by auto

    hence "∃p0. (A0 p0 = q) ∧ (∀x. A0 x = q ⟶ x = p0)" using 1 by auto
  }
  hence rtp3c: "invertible A0" by auto

  (* 3d: diffApprox (asFunc A0) g origin *)
  have "diffApprox (asFunc A) f x" using assms(2) by auto
  hence dAx: "(definedAt f x) ∧
    (∀ ε > 0 . (∃ δ > 0 . (∀ y .
      ( (y within δ of x)
        ⟶ 
        ( (definedAt f y) ∧ (∀ u v . (f y u ∧ (asFunc A) y v) ⟶
         ( sep2 v u ) ≤ (sqr ε) * sep2 y x )))  )
  ))" by blast
  hence rtp3d1: "definedAt g x" using g by auto 

  { fix e
    assume epos: "e > 0"
    then obtain d where d: "(d > 0) ∧ (∀ y .
      ( (y within d of x)
        ⟶ 
        ( (definedAt f y) ∧ (∀ u v . (f y u ∧ (asFunc A) y v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 y x )))  )"
      using dAx by auto
    { fix y
      assume "y within d of x"
      hence "(definedAt f y) ∧ (∀ u v . (f y u ∧ (asFunc A) y v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 y x )" using d by force
      hence "(definedAt g y) ∧ (∀ u v . (f y u ∧ (asFunc A) y v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 y x )" using g by force
      hence "(definedAt g y) ∧ (∀ u v . (g y u ∧ (asFunc A0) y v) ⟶
         ( sep2 v u ) ≤ (sqr e) * sep2 y x )" 
        using g A0 assms(1) lemBallTranslation by force
    }
    hence "∃d>0. ∀y . (y within d of x) ⟶ 
             (definedAt g y) ∧ (∀ u v . (g y u ∧ (asFunc A0) y v) ⟶
                   ( sep2 v u ) ≤ (sqr e) * sep2 y x )"
      using d by force
  }
  hence rtp3d2: "∀e>0. ∃d > 0. ∀y . (y within d of x) ⟶ 
             (definedAt g y) ∧ (∀ u v . (g y u ∧ (asFunc A0) y v) ⟶
                   ( sep2 v u ) ≤ (sqr e) * sep2 y x )"
    by auto
  hence rtp3d: "diffApprox (asFunc A0) g x" using rtp3d1 by auto

  hence rtp3: "affineApprox A0 g x" using rtp3a rtp3b rtp3c rtp3d by auto

(*  Needs to know that T is properly defined, hence inclusion of mkT *)
  thus ?thesis using g A0 mkT by best

qed


(* Local identities are globally the identity *)
lemma lemAffineIdentity:
  assumes "affine A"
and       "e > 0"
and       "∀ y . (y within e of x) ⟶ (A y = y)"
shows     "A = id"
proof -

  obtain T L where TL: "translation T ∧ linear L ∧ A = T∘L" using assms(1) by auto

  have "x within e of x" using assms(2) by auto
  hence xfixed: "A x = x" using assms(3) by auto

  { fix p
    define d where d: "d = (p ⊖ x)"
    then obtain a where a: "(a > 0) ∧ (norm2 (a⊗d) < sqr e)"
      using assms(2) lemSmallPoints[of "e" "d"] by auto

    define p' where p': "p' = ((a⊗d)⊕x)"
    hence p'fixed: "A p' = p'" using a assms(3) lemSep2Symmetry by auto

    have p'x: "(p' ⊖ x) = (a ⊗ (p ⊖ x))" using p' d by auto
    hence "((1/a)⊗(p'⊖x)) = (p⊖x)" using a lemScaleAssoc[of "1/a" "a" "p⊖x"] by auto
    hence p: "p = (((1/a)⊗(p'⊖x)) ⊕ x)" by auto

    hence "L p =  L (((1/a)⊗(p'⊖x)) ⊕ x)" by auto
    also have "... = ((L ((1/a)⊗(p'⊖x)))  ⊕ (L x))" using TL by blast
    also have "... = ((L x) ⊕ (L ((1/a)⊗(p'⊖x))))" using add_commute by simp
    finally have "A p = ((A x) ⊕ (L ((1/a)⊗(p'⊖x))))"
      using TL lemTranslationSum by auto

    hence 1: "A p = (x ⊕ (L ((1/a)⊗(p'⊖x))))" using xfixed by auto

    have "(L ((1/a)⊗(p'⊖x))) = ((1/a) ⊗ (L (p'⊖x)))" using TL by blast
    also have "... = ((1/a) ⊗ ( (L p') ⊖ (L x) ))" using TL by auto
    also have "... = ((1/a) ⊗ ( (A p') ⊖ (A x) ))" using TL by auto
    also have "... = ((1/a) ⊗ (p' ⊖ x))" using p'fixed xfixed by auto
    finally have "(L ((1/a)⊗(p'⊖x))) = (p⊖x)" using p by auto

    hence "A p = (x ⊕ (p ⊖ x))" using 1 by auto
    hence "A p = p" using add_diff_eq by auto
  }
  thus ?thesis by auto
qed



end (* of class Affine *)


end (* of theory Affine *)