Mathlib Changelog
Changelog
About
Github
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