Source indexedlemma · leanprover/lean4:v4.32.0

AddCircle.volume_preimage_equivIoc

Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:114 to 123

Mathematical statement

Exact Lean statement

lemma volume_preimage_equivIoc {T : ℝ} [hT : Fact (0 < T)] {s : Set ℝ} (hs : MeasurableSet s) :
    volume ((fun x ↦ (equivIoc T 0 x : ℝ)) ⁻¹' s) = volume (s ∩ Set.Ioc 0 T)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma volume_preimage_equivIoc {T : ℝ} [hT : Fact (0 < T)] {s : Set ℝ} (hs : MeasurableSet s) :    volume ((fun x ↦ (equivIoc T 0 x : ℝ)) ⁻¹' s) = volume (s ∩ Set.Ioc 0 T) := by  rw [← Measure.restrict_apply' measurableSet_Ioc,    ← (AddCircle.measurePreserving_mk T 0).measure_preimage      ((measurable_equivIoc T 0).subtype_coe.nullMeasurable hs),    Measure.restrict_apply' measurableSet_Ioc, Measure.restrict_apply' measurableSet_Ioc]  congr 1 with x  simp only [zero_add, Set.mem_inter_iff, Set.mem_preimage, and_congr_left_iff]  intro hx  rw [equivIoc_coe_of_mem (by simp [hx])]