### Abstract

Deep learning has had a profound impact on computer science in recent years, with applications to search engines, image recognition and language processing, bioinformatics, and more. Recently, Cohen et al. provided theoretical evidence for the superiority of deep learning over shallow learning. This formalization of their work simplifies and generalizes the original proof, while working around the limitations of the Isabelle type system. To support the formalization, I developed reusable libraries of formalized mathematics, including results about the matrix rank, the Lebesgue measure, and multivariate polynomials, as well as a library for tensor analysis.

### License

BSD License

### Topics

- Computer science/Machine learning
- Mathematics/Analysis

### Session Deep_Learning

- Tensor
- Tensor_Subtensor
- Tensor_Plus
- Tensor_Scalar_Mult
- Tensor_Product
- Tensor_Unit_Vec
- Tensor_Rank
- Tensor_Matricization
- DL_Rank_CP_Rank
- DL_Flatten_Matrix
- DL_Network
- DL_Concrete_Matrices
- DL_Missing_Finite_Set
- DL_Deep_Model
- DL_Deep_Model_Poly
- Lebesgue_Functional
- Lebesgue_Zero_Set
- DL_Shallow_Model
- DL_Fundamental_Theorem_Network_Capacity

### Depends on

- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Polynomial Interpolation
- Executable Multivariate Polynomials
- Vector Spaces

### Used by

- Quantum Hoare Logic

### Auto-related entries

- Knight’s Tour Revisited Revisited
- Factorization of Polynomials with Algebraic Coefficients
- A Sound Type System for Physical Quantities, Units, and Measurements
- WebAssembly
- Minkowski’s Theorem

## Cite

×

Deep_Learning-AFP

    @article{Deep_Learning-AFP,
      author  = {Alexander Bentkamp},
      title   = {Expressiveness of Deep Learning},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Deep_Learning.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Nov 10, 2016 : Isabelle2016