Commit 2023-06-09 02:13 f5cb6f28

View on Github →

feat: port MeasureTheory.Integral.CircleIntegral (#4858)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/CircleIntegral.lean

added theorem CircleIntegrable.out

added def CircleIntegrable

added theorem ContinuousOn.circleIntegrable'

added theorem ContinuousOn.circleIntegrable

added theorem Set.Countable.preimage_circleMap

added theorem abs_circleMap_zero

added def cauchyPowerSeries

added theorem cauchyPowerSeries_apply

added theorem circleIntegrable_const

added theorem circleIntegrable_iff

added theorem circleIntegrable_sub_inv_iff

added theorem circleIntegrable_sub_zpow_iff

added theorem circleIntegrable_zero_radius

added theorem circleIntegral.integral_congr

added theorem circleIntegral.integral_const_mul

added theorem circleIntegral.integral_eq_zero_of_hasDerivWithinAt'

added theorem circleIntegral.integral_eq_zero_of_hasDerivWithinAt

added theorem circleIntegral.integral_radius_zero

added theorem circleIntegral.integral_smul

added theorem circleIntegral.integral_smul_const

added theorem circleIntegral.integral_sub

added theorem circleIntegral.integral_sub_center_inv

added theorem circleIntegral.integral_sub_inv_of_mem_ball

added theorem circleIntegral.integral_sub_inv_smul_sub_smul

added theorem circleIntegral.integral_sub_zpow_of_ne

added theorem circleIntegral.integral_sub_zpow_of_undef

added theorem circleIntegral.integral_undef

added theorem circleIntegral.norm_integral_le_of_norm_le_const'

added theorem circleIntegral.norm_integral_le_of_norm_le_const

added theorem circleIntegral.norm_integral_lt_of_norm_le_const_of_lt

added theorem circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const

added def circleIntegral

added theorem circleIntegral_def_Icc

added def circleMap

added theorem circleMap_eq_center_iff

added theorem circleMap_mem_closedBall

added theorem circleMap_mem_sphere'

added theorem circleMap_mem_sphere

added theorem circleMap_ne_center

added theorem circleMap_ne_mem_ball

added theorem circleMap_not_mem_ball

added theorem circleMap_sub_center

added theorem circleMap_zero

added theorem circleMap_zero_radius

added theorem continuous_circleMap

added theorem continuous_circleMap_inv

added theorem deriv_circleMap

added theorem deriv_circleMap_eq_zero_iff

added theorem deriv_circleMap_ne_zero

added theorem differentiable_circleMap

added theorem hasDerivAt_circleMap

added theorem hasFPowerSeriesOn_cauchy_integral

added theorem hasSum_cauchyPowerSeries_integral

added theorem hasSum_two_pi_I_cauchyPowerSeries_integral

added theorem image_circleMap_Ioc

added theorem le_radius_cauchyPowerSeries

added theorem lipschitzWith_circleMap

added theorem measurable_circleMap

added theorem norm_cauchyPowerSeries_le

added theorem periodic_circleMap

added theorem range_circleMap

added theorem sum_cauchyPowerSeries_eq_integral