Theory LinearMaps

(*
   Mike Stannett
   Feb 2023
*)

section ‹ LinearMaps ›

text ‹This theory defines linear maps and establishes their main properties. ›

theory LinearMaps
  imports Functions CauchySchwarz Matrices
begin


class LinearMaps = Functions + CauchySchwarz + Matrices
begin

(*
  These functions are all single-valued, so we define them
  as having type ('a Point ⇒ 'a Point). We can use the
  asFunc function to convert them to relational form
  where necessary.
*)



(* This definition contains unnecessary terms, but this makes
it simpler to use it below. *)
abbreviation linear :: "('a Point ⇒ 'a Point) ⇒ bool" where
"linear L ≡ (L origin = origin)
          ∧ (∀ a p .  L (a ⊗ p) = (a ⊗ (L p)))
          ∧ (∀ p q . L (p ⊕ q) = ((L p) ⊕ (L q)))
          ∧ (∀ p q . L (p ⊖ q) = ((L p) ⊖ (L q)))"



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

(* Used to enable explicit substitutions *)
lemma lemLinearProps:                                             
  assumes "linear L"
  shows "(L origin = origin) ∧ (L (a ⊗ p) = (a ⊗ (L p))) 
            ∧ (L (p ⊕ q) = ((L p) ⊕ (L q)))
                ∧ (L (p ⊖ q) = ((L p) ⊖ (L q)))"
using assms by simp



lemma lemMatrixApplicationIsLinear: "linear (applyMatrix m)"
  using lemDotScaleRight lemDotSumRight lemDotDiffRight 
  by fastforce


lemma lemLinearIsMatrixApplication:
  assumes "linear L"
  shows   "∃ m . L = (applyMatrix m)"
proof -
  define Lt where "Lt = L tUnit"
  define Lx where "Lx = L xUnit"
  define Ly where "Ly = L yUnit"
  define Lz where "Lz = L zUnit"
  define M  where "M = transpose ⦇ trow = Lt, xrow = Lx, yrow = Ly, zrow = Lz ⦈"

  have trowM: "trow M = ⦇ tval = (tval Lt), xval = (tval Lx),
                         yval = (tval Ly), zval = (tval Lz) ⦈" 
    using M_def by auto
  have xrowM: "xrow M = ⦇ tval = (xval Lt), xval = (xval Lx),
                         yval = (xval Ly), zval = (xval Lz) ⦈" 
    using M_def by auto
  have yrowM: "yrow M = ⦇ tval = (yval Lt), xval = (yval Lx),
                         yval = (yval Ly), zval = (yval Lz) ⦈" 
    using M_def by auto
  have zrowM: "zrow M = ⦇ tval = (zval Lt), xval = (zval Lx),
                         yval = (zval Ly), zval = (zval Lz) ⦈" 
    using M_def by auto


  { fix u :: "'a Point"
    define tvu where tvu: "tvu = ((tval u)⊗tUnit)"
    define xvu where xvu: "xvu = ((xval u)⊗xUnit)"
    define yvu where yvu: "yvu = ((yval u)⊗yUnit)"
    define zvu where zvu: "zvu = ((zval u)⊗zUnit)"

    have u: "u = (tvu ⊕ (xvu ⊕ (yvu ⊕ zvu)))"
      using tvu xvu yvu zvu lemPointDecomposition[of "u"] by simp

    (* Calculate (M u) *)
    have Mu: "applyMatrix M u = ⦇ tval = dot (trow M) u,
                        xval = dot (xrow M) u,
                        yval = dot (yrow M) u,
                        zval = dot (zrow M) u ⦈" by simp

    have tvalMu: "tval (applyMatrix M u) = 
       (tval Lt)*(tval u) + (tval Lx)*(xval u) + (tval Ly)*(yval u) + (tval Lz)*(zval u)"
      using Mu trowM by force
    have xvalMu: "xval (applyMatrix M u) = 
       (xval Lt)*(tval u) + (xval Lx)*(xval u) + (xval Ly)*(yval u) + (xval Lz)*(zval u)"
      using Mu xrowM by force
    have yvalMu: "yval (applyMatrix M u) = 
       (yval Lt)*(tval u) + (yval Lx)*(xval u) + (yval Ly)*(yval u) + (yval Lz)*(zval u)"
      using Mu yrowM by force
    have zvalMu: "zval (applyMatrix M u) = 
       (zval Lt)*(tval u) + (zval Lx)*(xval u) + (zval Ly)*(yval u) + (zval Lz)*(zval u)"
      using Mu zrowM by force

    (* Calculate (L u) *)
    hence Lu: "L u  = ((L tvu) ⊕ ((L xvu) ⊕ ((L yvu) ⊕ (L zvu))))"
      using assms u
            lemLinearProps[of "L" "0" "tvu" "xvu ⊕ (yvu ⊕ zvu)"]
            lemLinearProps[of "L" "0" "xvu" "yvu ⊕ zvu"]
      by auto
    have Ltvu: "L tvu = ((tval u)⊗Lt)" 
      using tvu Lt_def assms lemLinearProps[of "L" "tval u" "tUnit"] by auto
    have Lxvu: "L xvu = ((xval u)⊗Lx)" 
      using xvu Lx_def assms lemLinearProps[of "L" "xval u" "xUnit"] by auto
    have Lyvu: "L yvu = ((yval u)⊗Ly)" 
      using yvu Ly_def assms lemLinearProps[of "L" "yval u" "yUnit"] by auto
    have Lzvu: "L zvu = ((zval u)⊗Lz)" 
      using zvu Lz_def assms lemLinearProps[of "L" "zval u" "zUnit"] by auto

    hence Lu': "L u = (((tval u)⊗Lt) ⊕ (((xval u)⊗Lx) 
                        ⊕ (((yval u)⊗Ly) ⊕ ((zval u)⊗Lz))))"
      using Lu Ltvu Lxvu Lyvu Lzvu by force
  
    hence "L u = applyMatrix M u"  
      using Lu' add_assoc tvalMu xvalMu yvalMu zvalMu mult_commute by simp
  }
  hence "∀ u. L u = applyMatrix M u" by auto
  thus ?thesis by force
qed



lemma lemLinearIffMatrix: "linear L ⟷ (∃ M. L = applyMatrix M)"
  using lemMatrixApplicationIsLinear lemLinearIsMatrixApplication 
  by auto



lemma lemIdIsLinear: "linear id"
  by simp



lemma lemLinearIsBounded:
  assumes "linear L"
  shows   "bounded L"
proof -
  obtain M where M: "L = applyMatrix M" using assms lemLinearIffMatrix by auto
  define tr where "tr = trow M"
  define xr where "xr = xrow M"
  define yr where "yr = yrow M"
  define zr where "zr = zrow M"
  define bnd where "bnd = (sqr(norm tr)+sqr(norm xr)+sqr(norm yr)+sqr(norm zr))"

  define n 
    where n: "n = ⦇ tval=norm tr, xval=norm xr, yval=norm yr, zval=norm zr ⦈"
  hence "bnd = dot n n" using bnd_def  by auto
  hence norm2n: "bnd = norm2 n" by simp
  hence bndnonneg: "bnd ≥ 0" by simp

  { assume bndpos: "bnd > 0"
    { fix p :: "'a Point"
  
      define q where "q = applyMatrix M p"
      hence "q = ⦇ tval=dot tr p, xval=dot xr p,yval=dot yr p, zval=dot zr p ⦈"
        using tr_def xr_def yr_def zr_def by auto
      hence 1: "dot q q = sqr (dot tr p) + sqr (dot xr p) 
                          + sqr (dot yr p) + sqr(dot zr p)"
        by auto
      also have "… ≤ sqr (dot tr p) + sqr (dot xr p) + sqr (dot yr p) 
                        + (sqr(norm zr)*sqr(norm p))"
        using lemCauchySchwarzSqr4[of "zr" "p"]  lemNormSqrIsNorm2 by auto
      also have "… ≤ sqr (dot tr p) + sqr (dot xr p) + (sqr(norm yr)*sqr(norm p)) 
                        + (sqr(norm zr)*sqr(norm p))"
        using lemCauchySchwarzSqr4[of "yr" "p"]  lemNormSqrIsNorm2 by auto
      also have "… ≤ sqr (dot tr p) + (sqr(norm xr)*sqr(norm p)) + (sqr(norm yr)*sqr(norm p)) 
                        + (sqr(norm zr)*sqr(norm p))"
        using lemCauchySchwarzSqr4[of "xr" "p"]  lemNormSqrIsNorm2 by auto
      also have "… ≤ (sqr(norm tr)*sqr(norm p)) + (sqr(norm xr)*sqr(norm p)) + (sqr(norm yr)*sqr(norm p)) 
                        + (sqr(norm zr)*sqr(norm p))"
        using lemCauchySchwarzSqr4[of "tr" "p"]  lemNormSqrIsNorm2 by auto
      finally have "dot q q ≤ (sqr(norm tr)*sqr(norm p)) + (sqr(norm xr)*sqr(norm p)) + (sqr(norm yr)*sqr(norm p)) 
                        + (sqr(norm zr)*sqr(norm p))" by auto
      hence "dot q q ≤ (sqr(norm tr)+sqr(norm xr)+sqr(norm yr)+sqr(norm zr))*sqr(norm p)"
        using distrib_right by auto
      hence "norm2 q ≤ bnd * sqr(norm p)" using bnd_def by simp
      hence "norm2 (applyMatrix M p) ≤ bnd * norm2 p"
        using q_def lemNormSqrIsNorm2  by simp
    }
    hence "∀ p. norm2 (applyMatrix M p) ≤ bnd * norm2 p" by auto
    hence "∃ bnd > 0 . ∀ p. norm2 (applyMatrix M p) ≤ bnd * norm2 p" 
      using bndpos by auto
  }
  hence case1: "(bnd > 0) ⟶ (bounded (applyMatrix M))" by simp

  { assume bnd0: "bnd = 0"
    hence "n = origin" using lemNullImpliesOrigin norm2n by auto
    hence "(norm tr = 0) ∧ (norm xr = 0) ∧ (norm yr = 0) ∧ (norm zr = 0)"
      using n by simp
    hence allzero: "(tr = origin)∧(xr=origin)∧(yr=origin)∧(zr=origin)"
      using lemZeroNorm by auto  
   
    define one where "one = (1::'a)"
    hence onepos: "one > 0" by simp
    { fix p :: "'a Point"
      have "applyMatrix M p = origin" 
        using allzero tr_def xr_def yr_def zr_def by auto
      hence "norm2(applyMatrix M p) = 0" by auto
      hence "norm2(applyMatrix M p) ≤ one * (norm2 p)" using onepos by auto
    }
    hence "∀ p .  norm2(applyMatrix M p) ≤ one * (norm2 p)" by auto
    hence "∃ one > 0 . ∀ p .  norm2(applyMatrix M p) ≤ one * (norm2 p)"
      using onepos by auto
    hence "bounded (applyMatrix M)" by simp
  }
  hence case2: "(bnd = 0) ⟶ (bounded (applyMatrix M))" by simp

  thus ?thesis using case1 case2 bndnonneg M by auto
qed



lemma lemLinearIsCts:
  assumes "linear L"
  shows   "cts (asFunc L) x"
proof -
  { fix x' 
    assume x': "x' = L x"

    have "bounded L" using assms(1) lemLinearIsBounded[of "L"] by auto
    then obtain bnd where bnd: "(bnd > 0) ∧ (∀p. norm2(L p) ≤ bnd*(norm2 p))"
      by auto
    then obtain bb where bb: "(bb > 0) ∧ (sqr bb) > bnd" 
      using bnd lemSquareExistsAbove[of "bnd"] by auto
  
    { fix p
      have p1: "norm2 (L p) ≤ bnd*(norm2 p)" using bnd by simp
      have "bnd*(norm2 p) ≤ (sqr bb)*(norm2 p)" using bb mult_mono by auto
      hence "norm2 (L p) ≤ (sqr bb)*(norm2 p)" using p1 by simp
    }
    hence bbbnd: "∀p . norm2 (L p) ≤ (sqr bb)*(norm2 p)" by auto
   
    { fix e
      assume epos: "e > 0"
      define d where d: "d = e/bb"
      hence dpos: "d > 0" using epos bb by simp
      have "(d = e/bb) ∧ (bb ≠ 0)" using d bb by auto
      hence esqr: "(sqr d)*(sqr bb) = sqr e" by simp
  
  
      { fix p'
        assume p': "p' ∈ applyToSet (asFunc L) (ball x d)"
        then obtain p where p: "(p ∈ ball x d) ∧ (p' = L p)" by auto
        hence p_near_x: "p within d of x" using lemSep2Symmetry[of "p" "x"] by force
  
        have "norm2 (L (p⊖x)) ≤ (sqr bb) * norm2 (p⊖x)" using bbbnd by blast
        hence 1: "norm2 (L (p⊖x)) ≤ (sqr bb) * (sep2 p x)" by auto
        have "(sqr bb)*(sep2 p x) < (sqr bb)*(sqr d)"
          using lemMultPosLT bb p_near_x by auto
        hence 2: "norm2 (L (p⊖x)) < (sqr bb) * (sqr d)" using 1  by simp
                        
        have "(L (p⊖x)) = ((L p) ⊖ (L x))" using assms(1) by auto
        hence "norm2 (L (p⊖x)) = sep2 p' x'" using p x' by force
        hence "sep2 p' x' <  (sqr bb) * (sqr d)" using 2 by simp
        hence "sep2 p' x' <  sqr e" using d bb by auto
        hence "p' ∈ ball x' e" using lemSep2Symmetry by auto
      }
      hence "applyToSet (asFunc L) (ball x d) ⊆ ball x' e" by auto
      hence "∃d>0. applyToSet (asFunc L) (ball x d) ⊆ ball x' e" 
        using dpos by auto
    }
    hence "∀e>0. ∃d>0. applyToSet (asFunc L) (ball x d) ⊆ ball x' e" 
      by auto
  }
  thus ?thesis by auto
qed


lemma lemLinOfLinIsLin:
assumes "(linear A) ∧ (linear B)"
shows   "linear (B ∘ A)"
proof -
  have 1: "(B ∘ A) origin = origin" using assms by auto
  have 2: "∀ a p . (B ∘ A)(a ⊗ p) = (a ⊗ ((B ∘ A) p))" using assms by auto
  have 3: "∀ p q . (B ∘ A) (p ⊕ q) = (((B ∘ A) p) ⊕ ((B ∘ A) q))" using assms by auto
  have 4: "∀ p q . (B ∘ A) (p ⊖ q) = (((B ∘ A) p) ⊖ ((B ∘ A) q))" using assms by auto
  thus ?thesis using 1 2 3 by force
qed



lemma lemInverseLinear:
  assumes "linear A"
and       "invertible A"
shows     "∃A' . (linear A') ∧ (∀ p q. A p = q ⟷ A' q = p)"
proof -
  obtain L where L: "(∀ p q. A p = q ⟷ L q = p)" 
    using assms(2) by metis

  have 1: "L origin = origin" using assms L by auto

  { fix p' q' a
    obtain p where p: "(A p = p') ∧ (∀z. A z = p' ⟶ z = p)" using assms(2) by blast
    obtain q where q: "(A q = q') ∧ (∀z. A z = q' ⟶ z = q)" using assms(2) by blast

    have "L (a ⊗ p') = L ( a ⊗ (A p) )" using p by auto
    also have "... = L ( A ( a ⊗ p ) )" using assms(1) by auto
    also have "... = (a ⊗ p)" using L by blast
    finally have 2: "L (a ⊗ p') = (a ⊗ (L p'))" using p L by auto

    have "L (p' ⊕ q') = L ((A p) ⊕ (A q))" using p q by auto
    also have "... = L( A (p ⊕ q) )" using assms(1) by auto
    also have "... = (p ⊕ q)" using p q L by auto
    finally have 3: "L (p' ⊕ q') = ( (L p') ⊕ (L q') )" using p q L by auto

    have "L (p' ⊖ q') = L ((A p) ⊖ (A q))" using p q by auto
    also have "... = L( A (p ⊖ q) )" using assms(1) by auto
    also have "... = (p ⊖ q)" using p q L by auto
    finally have 4: "L (p' ⊖ q') = ( (L p') ⊖ (L q') )" using p q L by auto

    hence "(L origin = origin) ∧  
           (L (a ⊗ p') = (a ⊗ (L p'))) ∧
           (L (p' ⊕ q') = ( (L p') ⊕ (L q') )) ∧ 
           (L (p' ⊖ q') = ( (L p') ⊖ (L q') ))"
      using 1 2 3 by auto
  }
  hence "linear L" by auto

  thus ?thesis using L by auto
qed



end (* of class LinearMaps *)


end (* of theory LinearMaps *)