Repository navigation

Formalize the Leshno universal approximation theorem - #246

Open

yuanyi-350 wants to merge 9 commits into

LeanMachineLearning:mainfrom

yuanyi-350:formalize-llps-universal-approximation

Open

Formalize the Leshno universal approximation theorem#246
yuanyi-350 wants to merge 9 commits into
LeanMachineLearning:mainfrom
yuanyi-350:formalize-llps-universal-approximation

Commits on Sep 12, 2026
- Formalize the Leshno universal approximation theorem
  yuanyi-350
  committed
  51d6faa
- Refactor universal approximation proofs and APIs
  yuanyi-350
  committed
  34981bc
- Refactor annihilator proofs and continuous map coercion
  yuanyi-350
  committed
  3497550
- run lake exe mk_all
  yuanyi-350
  committed
  b0d8af1
- fix ci
  yuanyi-350
  committed
  b728941
Commits on Sep 13, 2026
- Refactor universal approximation statements and simplify proofs
  yuanyi-350
  committed
  7196327
Commits on Sep 14, 2026
- remove useless lemmas
  yuanyi-350
  committed
  618825d
Commits on Sep 23, 2026
- solve merge conflicts
  yuanyi-350
  committed
  8476bf7
- Fix deprecated rwa syntax
  yuanyi-350
  committed
  6101a70