Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 17:28 f6dfea67

View on Github →

feat(measure_theory/integral): Cauchy integral formula for a circle (#10000)

Estimated changes

Modified src/analysis/box_integral/box/basic.lean

added theorem box_integral.box.Ioo_subset_coe

added theorem box_integral.box.Union_Ioo_of_tendsto

added theorem box_integral.box.exists_seq_mono_tendsto

modified def box_integral.box.face

added theorem box_integral.box.monotone_face

Modified src/analysis/box_integral/partition/measure.lean

added theorem box_integral.box.Ioo_ae_eq_Icc

added theorem box_integral.box.coe_ae_eq_Icc

modified theorem box_integral.box.measurable_set_Icc

added theorem box_integral.box.measurable_set_Ioo

modified theorem box_integral.box.measurable_set_coe

modified theorem box_integral.box.measure_Icc_lt_top

modified theorem box_integral.box.measure_coe_lt_top

Created src/analysis/complex/cauchy_integral.lean

added theorem complex.circle_integral_div_sub_of_differentiable_on_off_countable

added theorem complex.circle_integral_eq_zero_of_differentiable_on_off_countable

added theorem complex.circle_integral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable

added theorem complex.circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable

added theorem complex.circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto

added theorem complex.circle_integral_sub_inv_smul_of_differentiable_on_off_countable

added theorem complex.circle_integral_sub_inv_smul_of_differentiable_on_off_countable_aux

added theorem complex.has_fpower_series_on_ball_of_differentiable_off_countable

added theorem complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable

added theorem complex.integral_boundary_rect_of_has_fderiv_within_at_real_off_countable

added theorem complex.two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable

Modified src/measure_theory/constructions/pi.lean

added theorem measure_theory.measure.pi_Ioo_ae_eq_pi_Ioc

Modified src/measure_theory/integral/divergence_theorem.lean

added theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_aux₁

added theorem measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable_aux₂

Modified src/topology/separation.lean

added theorem tendsto_nhds_unique_of_frequently_eq