CircleNullImage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Null images of local circle-valued traces

Projection modulo one preserves real outer-null sets. A countable family of null real branches therefore gives a null image in the circle with its Haar measure of total mass one.

theorem OAI.CircleDomainRigidity.volume_addCircle_image_eq_zero line 18

theorem OAI.CircleDomainRigidity.volume_eq_zero_of_countable_real_branches line 55

Source documentation

A circle-valued image covered by countably many null real branch images is Haar-null, with no measurability assumption on the image.

theorem volume_eq_zero_of_countable_real_branches
    {X : Type*} (F : Set X) (w : X → AddCircle (1 : ℝ))
    (V : ℕ → Set X) (v : ℕ → X → ℝ)
    (hcover : F ⊆ ⋃ n, V n)
    (hbranch : ∀ n, ∀ x ∈ F ∩ V n, (v n x : AddCircle (1 : ℝ)) = w x)
    (hnull : ∀ n, volume (v n '' (F ∩ V n)) = 0) :
    volume (w '' F) = 0 := by
…