Commit 2026-06-09 04:56 064ebe2e

View on Github →

feat: continuity of posLog (#40349) Establish continuity of posLog. As a trivial corollary, establish continuity of the proximitiy function.

Estimated changes

Modified Mathlib/Analysis/Complex/ValueDistribution/Proximity/Basic.lean

added theorem ValueDistribution.continuous_proximity_top

Modified Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

added theorem Real.continuous_posLog

added theorem Real.posLog_apply

modified theorem Real.posLog_def