Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.IsUniform.restrict

PFR.ForMathlib.Uniform · PFR/ForMathlib/Uniform.lean:219 to 237

Source documentation

If $X$ is uniform w.r.t. $\mu$ on $H$ , then $X$ is uniform w.r.t. $\mu$ conditioned by $H'$ on $H' \cap H$ .

Exact Lean statement

lemma IsUniform.restrict {H : Set S} (h : IsUniform H X μ) (hX : Measurable X) (H' : Set S) :
    IsUniform (H' ∩ H) X (μ[|X ⁻¹' H']) where
  eq_of_mem

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma IsUniform.restrict {H : Set S} (h : IsUniform H X μ) (hX : Measurable X) (H' : Set S) :    IsUniform (H' ∩ H) X (μ[|X ⁻¹' H']) where  eq_of_mem := fun x hx y hy ↦ by    simp only [cond, Measure.smul_apply, smul_eq_mul]    rw [μ.restrict_eq_self (preimage_mono (singleton_subset_iff.mpr hx.1)),      μ.restrict_eq_self (preimage_mono (singleton_subset_iff.mpr hy.1)), h.eq_of_mem hx.2 hy.2]  measure_preimage_compl := by    rewrite [← nonpos_iff_eq_zero, Set.compl_inter, Set.preimage_union]    calc      _ ≤ (μ[|X ⁻¹' H']) (X ⁻¹' H'ᶜ) + (μ[|X ⁻¹' H']) (X ⁻¹' Hᶜ) := measure_union_le _ _      _ = (μ[|X ⁻¹' H']) (X ⁻¹' H'ᶜ) + 0 := congrArg _ <| by        simp only [cond, Measure.smul_apply, smul_eq_mul]        convert mul_zero _        exact eq_bot_mono (Measure.restrict_apply_le _ _) h.measure_preimage_compl      _ = 0 := by        simp only [cond, Measure.smul_apply, smul_eq_mul]        rw [add_zero, Set.preimage_compl, Measure.restrict_apply <|          MeasurableSet.compl (measurableSet_preimage hX .of_discrete),          compl_inter_self, measure_empty, mul_zero]