{"entities":{"Q7361955":{"pageid":31521404,"ns":120,"title":"Item:Q7361955","lastrevid":105369533,"modified":"2026-10-07T13:38:06Z","type":"item","id":"Q7361955","labels":{"en":{"language":"en","value":"The Sigmoid Function and the Universal Approximation Theorem"}},"descriptions":{"en":{"language":"en","value":"AFP entry Sigmoid_Universal_Approximation"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7fad78b2098b141bc943ead4f5435e0734d5a199","datavalue":{"value":"https://isa-afp.org/entries/Sigmoid_Universal_Approximation.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361955$B283AFD1-D095-46B1-A9DF-30CCD68DECA3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1dee5eef72567f68024f6e6f6a29dae74ed5cfd5","datavalue":{"value":{"time":"+2025-05-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361955$3709730C-D1E5-4FFD-AFCC-03CFB2BBCAC4","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"0bf4d3ca5eedd1d75f040083aae2b975258503f7","datavalue":{"value":"Dustin Bryant","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361955$D5E8E83C-439B-498D-A199-8ED2F3DC1F3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"00b93769b3b750eeb530768bd1922ef7b991d486","datavalue":{"value":"Jim Woodcock","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361955$20E025CE-F5EB-4BD7-9E05-B7F070DD8505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"c9ddb9cb8edac3e4e3079ad62f4b03206fa5cc4b","datavalue":{"value":"Simon Foster","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361955$0154131E-EE16-4BE7-88B7-1E57071173E3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d079ebec65f52619623b99eb9281c324ae1c3f33","datavalue":{"value":{"text":"The Sigmoid Function and the Universal Approximation Theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361955$8A0EEA2C-A96D-4937-B89E-2F7E613E80A7","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"95f5d8a87184a5d95e0a9c2821ecde0fdba49fec","datavalue":{"value":"We present a machine-checked Isabelle/HOL development of the sigmoid function \\[ \\sigma(x)=\\frac{e^{x}}{1+e^{x}}, \\] together with its most important analytic properties. After proving positivity, strict monotonicity, \\(C^{\\infty}\\) smoothness, and the limits at \\(\\pm\\infty\\), we derive a closed-form expression for the \\(n\\)-th derivative using Stirling numbers of the second kind, following the combinatorial argument of Minai and Williams. These results are packaged into a small reusable library of lemmas on \\(\\sigma\\). Building on this analytic groundwork we mechanise a constructive version of the classical Universal Approximation Theorem: for every continuous function \\(f\\colon[a,b]\\to\\mathbb{R}\\) and every \\(\\varepsilon>0\\) there is a single\u2011hidden\u2011layer neural network with sigmoidal activations whose output is within \\(\\varepsilon\\) of \\(f\\) everywhere on \\([a,b]\\). Our proof follows the method of Costarell and Spigler, giving the first fully verified end-to\u2011end proof of this theorem inside a higher\u2011order proof assistant.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361955$EFFCEDCE-5FD8-459A-AF6D-6EE377D82F5C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cd92ac4f3c0c833c82097dfb978d14edcac1a0a","datavalue":{"value":{"entity-type":"item","numeric-id":4011460,"id":"Q4011460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$876E3EAF-74C0-4102-9251-66FD2C830F85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"910d66a9432b2cd7b20379efb8233af4f3945f0a","datavalue":{"value":{"entity-type":"item","numeric-id":5399935,"id":"Q5399935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$39E76028-8C9A-4046-8496-3CA1D106C1AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"306ff5799f14f929904fdf8429c081dfbd2964c7","datavalue":{"value":{"entity-type":"item","numeric-id":5916442,"id":"Q5916442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$F4D2F2CF-3DB4-45FF-9B69-3AE9C24DC2DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$99C247DE-E838-42D2-A885-F5F7087E6846","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$161A6ED3-2D8C-4FD2-BCB3-A654544FD9FD","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ce3280e9ef2fb44c844e03b65b6366a348e2eeb2","datavalue":{"value":{"entity-type":"item","numeric-id":7360783,"id":"Q7360783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$3C00FE0E-D22C-46B2-AB30-3A740F14A21D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ef6655bf04dd34fee9f7dc3b2763244f951e30fe","datavalue":{"value":{"entity-type":"item","numeric-id":7360822,"id":"Q7360822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$3E5427E6-A517-44FD-86BE-D85580DA9D0C","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361955$69982C54-CD7E-41D1-A64F-1598907B88AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The Sigmoid Function and the Universal Approximation Theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_Sigmoid_Function_and_the_Universal_Approximation_Theorem"}}}}}