Stream: Is there code for X?

Topic: Connecting vec spaces from Jordan_Normal_Form to topology

Sage Binder (May 30 2024 at 00:41):

Hi all, I am working with the vector/matrix framework provided by Jordan_Normal_Form from the AFP. I am wondering if there are connections between this framework and topological notions. For instance, given n, I'd like to state that the n-dimensional sphere (as a subset of carrier_vec n) is compact.

Jonathan Julian Huerta y Munive (May 30 2024 at 10:12):

There is a weak connection that requires work. The Jordan Normal Form matrices have been connected to HOL matrices (their type denoted 'a ^ 'n). See what the authors claim in this AFP entry. If you find that they are using an isomorphism, you could prove the following:

lemma "compact (sphere x r)" for x :: "('a::{metric_space, heine_borel})^'n"
  unfolding compact_eq_bounded_closed
  unfolding bounded_def closed_def open_contains_ball
  apply safe
   apply (metis less_eq_real_def mem_sphere)
  apply clarsimp
  subgoal for y
    apply (cases "dist x y > r")
     apply (rule_tac x="dist x y - r" in exI, clarsimp)
    apply (metis add.commute add_less_cancel_left diff_add_cancel dist_commute dist_triangle linorder_not_less)
    apply (rule_tac x="r - dist x y" in exI, clarsimp)
    apply (metis add.commute add_less_cancel_left diff_add_cancel dist_commute dist_triangle linorder_not_less)
    done
  done

and then you could try to connect this result to the JNF-matrices via their isomorphism.

Unfortunately, using the find_theorems command (i.e. find_theorems name: compact name: sphere) from the Perron_Frobenius AFP entry, only throws the standard theorem from HOL-Analysis (Elementary_Normed_Spaces.compact_sphere). Also, SErAPIS does not show anything after a quick search.

Sage Binder (May 31 2024 at 08:32):

Ah, thank you for the direction! The connection in that AFP entry looks alright to work with.

For posterity: after asking the question, I came across a similar kind of isomorphism between the HOL matrices and JNF matrices provided by the Complex_Bounded_Operators AFP entry, but to my (inexperienced) eye, it looked more difficult to work with than the connection in Perron_Frobenius.

Last updated: Dec 21 2024 at 16:20 UTC