* HOL/Multivariate_Analysis: Replaced "basis :: 'a::euclidean_space => nat => real" and "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space" on euclidean spaces by using the inner product "_ \<bullet> _" with vectors from the Basis set. "\<Chi>\<Chi> i. f i" is replaced by "SUM i : Basis. f i *r i".
With this change the following constants are also chanegd or removed: DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation) a $$ i ~> inner a i (where i : Basis) cart_base i removed \<pi>, \<pi>' removed Theorems about these constants where removed. Renamed lemmas: component_le_norm ~> Basis_le_norm euclidean_eq ~> euclidean_eq_iff differential_zero_maxmin_component ~> differential_zero_maxmin_cart euclidean_simps ~> inner_simps independent_basis ~> independent_Basis span_basis ~> span_Basis in_span_basis ~> in_span_Basis norm_bound_component_le ~> norm_boound_Basis_le norm_bound_component_lt ~> norm_boound_Basis_lt component_le_infnorm ~> Basis_le_infnorm INCOMPATIBILITY. This change was suggested by Brian Huffman and it finished his introduction of the Basis set. - Johannes _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev