chapter AFP

session Projected_Gradient_Descent = "HOL-Analysis" +
  options [timeout = 600]
  theories
    Gradient_Preliminaries
    Convex_Differentiable
    Smooth_Convex
    Abstract_Descent
    Gradient_Descent
    Gradient_Descent_Rates
    Gradient_Descent_Convergence
    Projection_Geometry
    Projection_Optimization
    Projected_Gradient_Descent_Convergence
    Projected_Gradient_Mapping
    Projected_Gradient_Mapping_Rates
    Projected_Gradient_Descent_Residual_Convergence
    Strong_Convex
    Projected_Gradient_Descent_Linear_Rate
    Lipschitz_Smoothness
    Examples_Quadratic
    Examples_Projected_Quadratic
    Main_Results
    Examples_Using_Main_Results
    Projected_Gradient_Descent
  document_files
    "root.tex"
    "root.bib"