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

exists_isUniform_of_rdist_eq_zero

PFR.HundredPercent · PFR/HundredPercent.lean:162 to 177

Source documentation

If $d[X_1;X_2]=0$ , then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$ . Follows from the preceding claim by the triangle inequality.

Exact Lean statement

theorem exists_isUniform_of_rdist_eq_zero
    {Ω' : Type*} [MeasureSpace Ω'] [IsProbabilityMeasure (ℙ : Measure Ω')] {X' : Ω' → G}
    (hX : Measurable X) (hX' : Measurable X') (hdist : d[X # X'] = 0) :
    ∃ H : AddSubgroup G, ∃ U : Ω → G,
      Measurable U ∧ IsUniform H U ∧ d[X # U] = 0 ∧ d[X' # U] = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem exists_isUniform_of_rdist_eq_zero    {Ω' : Type*} [MeasureSpace Ω'] [IsProbabilityMeasure (ℙ : Measure Ω')] {X' : Ω' → G}    (hX : Measurable X) (hX' : Measurable X') (hdist : d[X # X'] = 0) :    ∃ H : AddSubgroup G, ∃ U : Ω → G,      Measurable U ∧ IsUniform H U ∧ d[X # U] = 0 ∧ d[X' # U] = 0 := by  have h' : d[X # X] = 0 := by    apply le_antisymm _ (rdist_nonneg hX hX)    calc      d[X # X] ≤ d[X # X'] + d[X' # X] := rdist_triangle hX hX' hX      _ = 0 := by rw [hdist, rdist_symm, hdist, zero_add]  rcases exists_isUniform_of_rdist_self_eq_zero hX h' with ⟨H, U, hmeas, hunif, hd⟩  refine ⟨H, U, hmeas, hunif, hd, ?_⟩  apply le_antisymm _ (rdist_nonneg hX' hmeas)  calc    d[X' # U] ≤ d[X' # X] + d[X # U] := rdist_triangle hX' hX hmeas    _ = 0 := by rw [hd, rdist_symm, hdist, zero_add]