Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-07 00:12 fdfc2229

View on Github →

feat(measure_theory/integral): Circle integral transform (#13885) Some basic definitions and results related to circle integrals of a function. These form part of #13500

Estimated changes

Modified src/measure_theory/integral/circle_integral.lean

added theorem continuous_circle_map_inv

Created src/measure_theory/integral/circle_integral_transform.lean

added theorem complex.abs_circle_transform_bounding_function_le

added def complex.circle_transform

added def complex.circle_transform_bounding_function

added def complex.circle_transform_deriv

added theorem complex.circle_transform_deriv_bound

added theorem complex.circle_transform_deriv_eq

added theorem complex.circle_transform_deriv_periodic

added theorem complex.continuous_circle_transform

added theorem complex.continuous_circle_transform_deriv

added theorem complex.continuous_on_abs_circle_transform_bounding_function

added theorem complex.continuous_on_prod_circle_transform_function

added theorem complex.integral_circle_transform