Theory Dual_Bases

theory Dual_Bases
  imports Brackets
begin

section{*Dual Bases*}

context finite_dimensional_vector_space
begin

subsection{*Theorem 1.*}

text{*We recall here that @{term X} is a basis for the vector space @{term V}
  and @{term indexing_X} is a way to provide the basis with coordinates.*}

text{*The definition of @{term indexing} is polymorphic, and in this lemma
  will be used both for the basis @{term X} and also for the set of scalars.*}

text{*In this lemma will be useful the results in file @{text Vector_Space_K_n.thy},
  for instance @{thm linear_combination_unique} and 
  @{thm lin_comb_is_the_linear_combination_indexing}, where it is proved that 
  any element in @{term "carrier V"} can be expressed in a unique way
  as a linear combination of the elements in @{term X}.*}
thm lin_comb_is_the_linear_combination_indexing
find_theorems "(∃!f. _)"

lemma theorem_1:
  assumes ia: "indexing ((A::'a set), fA)"
  and c: "card A = dimension"
  shows "(∃!y. linear_functional y ∧ (∀i∈{..<dimension}. <indexing_X i, y> = fA i))"
proof -
  def y == "(λx. (\<Oplus>\<^bsub>K\<^esub>i∈{..<dimension}. (lin_comb x) (indexing_X i) ⊗ (fA i)))"
  show ?thesis
  proof (rule ex1I [of _ y], rule conjI)
    show "linear_functional y"
      unfolding y_def 
      unfolding linear_functional_def additive_functional_def 
        multiplicative_functional_def
      sorry
    (*Take a look at linear_map_iso_V_K_n, lin_comb_additivity and lin_comb_homogeneity
        since they prove really similar things*)
    show "∀i∈{..<dimension}. y (indexing_X i) = fA i"
    proof (rule ballI)
      fix i assume i: "i ∈ {..<dimension}"
      show "y (indexing_X i) = fA i"
        unfolding y_def
        using lin_comb_basis
        sorry
    qed
  next
    show "!!ya. linear_functional ya ∧ (∀i∈{..<dimension}. ya (indexing_X i) = fA i) ==> ya = y"
      sorry
  qed
qed          

subsection{*Theorem 2.*}

term linear_functional

definition delta :: "nat => nat => 'a"
  where "delta i j = (if i = j then \<one> else \<zero>)"

definition linear_functional_basis :: "nat => ('c => 'a)"
  where "linear_functional_basis n = (λx. delta (preim2 x) n)"

definition linear_functional_basis_set :: "('c => 'a) set"
  where "linear_functional_basis_set = {(λx. delta (preim2 x) n) | n. n ∈ {..<dimension}}"

lemma theorem_2:
  shows "vector_space.basis K V' (λx f y. x ⊗ f y) linear_functional_basis_set"
proof -
  interpret V': vector_space K V' "(λx f y. x ⊗ f y)" using vector_space_V' .
  show ?thesis
    sorry
qed

subsection{*Theorem 3.*}

lemma theorem_3:
  assumes x_ne_0: "x ≠ \<zero>\<^bsub>V\<^esub>"
  shows "∃y. linear_functional y ∧ <x,y> ≠ \<zero>\<^bsub>K\<^esub>"
  sorry

corollary theorem_3_c:
  assumes x_ne_0: "u ≠ v"
  shows "∃y. linear_functional y ∧ <u,y> ≠ <v,y>"
  sorry

end

end