Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-03 21:57 de07131e

View on Github →

feat(measure_theory/integral/torus_integral): torus integral and its properties (#12892) Define a generalized torus map and prove some basic properties. Define the torus integral and the integrability of functions on a generalized torus, and prove lemmas about them.

Estimated changes

Modified src/measure_theory/integral/circle_integral.lean

added theorem circle_integral_def_Icc

added theorem circle_map_zero

Created src/measure_theory/integral/torus_integral.lean

added theorem norm_torus_integral_le_of_norm_le_const

added theorem torus_integrable.function_integrable

added theorem torus_integrable.torus_integrable_const

added theorem torus_integrable.torus_integrable_zero_radius

added def torus_integrable

added def torus_integral

added theorem torus_integral_add

added theorem torus_integral_const_mul

added theorem torus_integral_dim0

added theorem torus_integral_dim1

added theorem torus_integral_neg

added theorem torus_integral_radius_zero

added theorem torus_integral_smul

added theorem torus_integral_sub

added theorem torus_integral_succ

added theorem torus_integral_succ_above

added def torus_map

added theorem torus_map_eq_center_iff

added theorem torus_map_sub_center

added theorem torus_map_zero_radius