Skip to content
Started 1 yr 7 mo ago
Took 11 hr on workerlrz5
Success

#2086 (Oct 6, 2022, 1:33:09 AM)

Build Artifacts
Changes

Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

  1. fix author entry; regen website (detail)
  2. add change history revision (detail)
  3. Added scene spaces, improvements to prisms, and improvements to the alphabet command. (detail)
  4. merge from afp-2021-1 (detail)
  5. new entry Query_Optimization (detail)
  6. remove temp file (detail)
  7. Complex_Bounded_Operators: Various changes:

    - Removed auxiliary constant `the_riesz_rep_bilinear'`
    - Renamed constant `the_riesz_rep_bilinear` -> `the_riesz_rep_sesqui` and defined differently but equivalently
    - Renamed constant `bifunctional` -> `bidual_embedding`
      (and renamed lemmas containing `bifunctional` accordingly)
    - Renamed lemmas `the_riesz_rep_bilinear_apply` -> `the_riesz_rep_sesqui_apply`,
      `cblinfun_extension_exists_norm` -> `cblinfun_extension_norm_bounded_dense`
    - New theorems: `rank1_compose_left`, `rank1_compose_right`, `rank1_scaleC`,
      `rank1_uminus`, `rank1_uminus_iff`, `rank1_adj`, `rank1_adj_iff`,
      `bidual_embedding_surj`, `Cblinfun_comp_bounded_cbilinear`, `Cblinfun_comp_bounded_sesquilinear`, `bounded_clinear_0`,
      `bounded_antilinear_0`, `bounded_cbilinear_0`, `bounded_sesquilinear_0`, `bounded_cbilinear_apply_bounded_clinear`,
      `bounded_sesquilinear_apply_bounded_clinear`, `cblinfun_extension_exists_hilbert`,  `trunc_ell2_reduces_norm`,
      `trunc_ell2_add`, `trunc_ell2_scaleC`, `bounded_clinear_trunc_ell2`
    - Theorem `cblinfun_extension_exists_proj`: Reformulated one assumption (detail)

Started by an SCM change

This run spent:

  • 7.8 sec waiting;
  • 11 hr build duration;
  • 11 hr total from scheduled to completion.
Revision: 4a064fad28b2b7c4a7a969334fdf22fc4165afc8
Revision: 33daf9a750b86aa162f420514b0459563ca0d2ae