Commit 2025-03-05 19:21 df474f93

View on Github →

feat: congruence theorems for interval/circle integrals (#22372) Prove that integrals are invariant when functions are changed along a discrete set. This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

added theorem CircleIntegrable.congr_codiscreteWithin

added theorem analyticOnNhd_circleMap

added theorem circleIntegrable_congr_codiscreteWithin

added theorem circleIntegral.circleIntegral_congr_codiscreteWithin

added theorem circleMap_preimage_codiscrete

added theorem contDiff_circleMap

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

added theorem IntervalIntegrable.congr_codiscreteWithin

added theorem intervalIntegrable_congr_codiscreteWithin

added theorem intervalIntegral.integral_congr_ae_restrict

added theorem intervalIntegral.integral_congr_codiscreteWithin

Created Mathlib/MeasureTheory/Topology.lean

added theorem ae_restrict_le_codiscreteWithin

Modified Mathlib/Topology/DiscreteSubset.lean

added theorem discreteTopology_of_codiscreteWithin