Measure-theoretic results about the additive circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The file is a place to collect measure-theoretic results about the additive circle.

Main definitions: #

add_circle.closed_ball_ae_eq_ball: open and closed balls in the additive circle are almost equal
add_circle.is_add_fundamental_domain_of_ae_ball: a ball is a fundamental domain for rational angle rotation in the additive circle

theorem add_circle.closed_ball_ae_eq_ball {T : ℝ} [hT : fact (0 < T)] {x : add_circle T} {ε : ℝ} :

metric.closed_ball x ε =ᵐ[measure_theory.measure_space.volume ] metric.ball x ε

theorem add_circle.is_add_fundamental_domain_of_ae_ball {T : ℝ} [hT : fact (0 < T)] (I : set (add_circle T)) (u x : add_circle T) (hu : is_of_fin_add_order u) (hI : I =ᵐ[measure_theory.measure_space.volume ] metric.ball x (T / (2 * ↑(add_order_of u)))) :

measure_theory.is_add_fundamental_domain ↥(add_subgroup.zmultiples u) I measure_theory.measure_space.volume

Let G be the subgroup of add_circle T generated by a point u of finite order n : ℕ. Then any set I that is almost equal to a ball of radius T / 2n is a fundamental domain for the action of G on add_circle T by left addition.

source

theorem add_circle.volume_of_add_preimage_eq {T : ℝ} [hT : fact (0 < T)] (s I : set (add_circle T)) (u x : add_circle T) (hu : is_of_fin_add_order u) (hs : u +ᵥ s =ᵐ[measure_theory.measure_space.volume ] s) (hI : I =ᵐ[measure_theory.measure_space.volume ] metric.ball x (T / (2 * ↑(add_order_of u)))) :

⇑measure_theory.measure_space.volume s = add_order_of u • ⇑measure_theory.measure_space.volume (s ∩ I)