Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-25 10:29 0aca7061

View on Github →

feat(measure_theory/integral): define circle_integral (#10906)

Estimated changes

Modified src/algebra/periodic.lean

added theorem function.periodic.image_Ioc

Created src/measure_theory/integral/circle_integral.lean

added theorem abs_circle_map_zero

added def cauchy_power_series

added theorem cauchy_power_series_apply

added theorem circle_integrable.add

added theorem circle_integrable.neg

added theorem circle_integrable.out

added def circle_integrable

added theorem circle_integrable_const

added theorem circle_integrable_iff

added theorem circle_integrable_sub_inv_iff

added theorem circle_integrable_sub_zpow_iff

added theorem circle_integrable_zero_radius

added theorem circle_integral.integral_congr

added theorem circle_integral.integral_const_mul

added theorem circle_integral.integral_eq_zero_of_has_deriv_within_at'

added theorem circle_integral.integral_eq_zero_of_has_deriv_within_at

added theorem circle_integral.integral_radius_zero

added theorem circle_integral.integral_smul

added theorem circle_integral.integral_smul_const

added theorem circle_integral.integral_sub

added theorem circle_integral.integral_sub_center_inv

added theorem circle_integral.integral_sub_inv_of_mem_ball

added theorem circle_integral.integral_sub_zpow_of_ne

added theorem circle_integral.integral_sub_zpow_of_undef

added theorem circle_integral.integral_undef

added theorem circle_integral.norm_integral_le_of_norm_le_const'

added theorem circle_integral.norm_integral_le_of_norm_le_const

added def circle_integral

added def circle_map

added theorem circle_map_eq_center_iff

added theorem circle_map_mem_closed_ball

added theorem circle_map_mem_sphere'

added theorem circle_map_mem_sphere

added theorem circle_map_ne_center

added theorem circle_map_sub_center

added theorem circle_map_zero_radius

added theorem continuous_circle_map

added theorem continuous_on.circle_integrable'

added theorem continuous_on.circle_integrable

added theorem deriv_circle_map

added theorem deriv_circle_map_eq_zero_iff

added theorem deriv_circle_map_ne_zero

added theorem differentiable_circle_map

added theorem has_deriv_at_circle_map

added theorem has_fpower_series_on_cauchy_integral

added theorem has_sum_cauchy_power_series_integral

added theorem has_sum_two_pi_I_cauchy_power_series_integral

added theorem image_circle_map_Ioc

added theorem le_radius_cauchy_power_series

added theorem lipschitz_with_circle_map

added theorem measurable_circle_map

added theorem norm_cauchy_power_series_le

added theorem periodic_circle_map

added theorem range_circle_map

added theorem sum_cauchy_power_series_eq_integral

Modified src/topology/metric_space/basic.lean

added theorem metric.closed_ball_mem_nhds_of_mem