Skip to content

feat(Analysis/InnerProductSpace/Reproducing): add bilinear form and integral operator for Mercers theorem#42003

Draft
TJHeeringa wants to merge 18 commits into
leanprover-community:masterfrom
TJHeeringa:mercersTheorem
Draft

feat(Analysis/InnerProductSpace/Reproducing): add bilinear form and integral operator for Mercers theorem#42003
TJHeeringa wants to merge 18 commits into
leanprover-community:masterfrom
TJHeeringa:mercersTheorem

Commits

Commits on Jul 14, 2026

Commits on Jul 17, 2026

Commits on Jul 20, 2026

Commits on Jul 22, 2026

Commits on Jul 23, 2026

Commits on Jul 24, 2026