Commit 2023-06-09 14:37 33666e3f

View on Github →

feat: port MeasureTheory.Integral.CircleTransform (#4908)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/CircleTransform.lean

added theorem Complex.abs_circleTransformBoundingFunction_le

added def Complex.circleTransform

added def Complex.circleTransformBoundingFunction

added def Complex.circleTransformDeriv

added theorem Complex.circleTransformDeriv_bound

added theorem Complex.circleTransformDeriv_eq

added theorem Complex.circleTransformDeriv_periodic

added theorem Complex.continuousOn_abs_circleTransformBoundingFunction

added theorem Complex.continuousOn_prod_circle_transform_function

added theorem Complex.continuous_circleTransform

added theorem Complex.continuous_circleTransformDeriv

added theorem Complex.integral_circleTransform