Skip to content

feat: weighted sums of antitone functions, an implicit square-root bound, and quadratic bounds on log (1 + x) - #379

Open
RemyDegenne wants to merge 3 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/numerical-lemmas-worker1
Open

feat: weighted sums of antitone functions, an implicit square-root bound, and quadratic bounds on log (1 + x)#379
RemyDegenne wants to merge 3 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/numerical-lemmas-worker1

refactor: make the derivative-sign comparison a public calculus lemma

e46b37b
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning and 1 notice
app-credentials
succeeded Nov 14, 2026 in 3s