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

sum_prob_preimage

PFR.WeakPFR · PFR/WeakPFR.lean:409 to 424

Mathematical statement

Exact Lean statement

lemma sum_prob_preimage {G H : Type*} {X : Finset H} {A : Set G} [Finite A] {φ : A → X}
    {A_ : H → Set G} (hA : A.Nonempty) (hφ : ∀ x : X, A_ x = Subtype.val '' (φ ⁻¹' {x})) :
    ∑ x ∈ X, (Nat.card (A_ x) : ℝ) / Nat.card A = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_prob_preimage {G H : Type*} {X : Finset H} {A : Set G} [Finite A] {φ : A → X}    {A_ : H → Set G} (hA : A.Nonempty) (hφ : ∀ x : X, A_ x = Subtype.val '' (φ ⁻¹' {x})) :    ∑ x ∈ X, (Nat.card (A_ x) : ℝ) / Nat.card A = 1 := by  rw [← Finset.sum_div]  apply (div_eq_one_iff_eq <| Nat.cast_ne_zero.mpr    <| Nat.pos_iff_ne_zero.mp (@Nat.card_pos _ hA.to_subtype _)).mpr  classical  have := Fintype.ofFinite A  rewrite [Nat.card_eq_fintype_card, ← Finset.card_univ, Finset.card_eq_sum_card_fiberwise    <| fun a _ ↦ Finset.mem_univ (φ a), ← Finset.sum_coe_sort]  norm_cast  congr with x  rewrite [← Set.Finite.toFinset_setOf, (Set.toFinite _).card_toFinset, ← Nat.card_eq_fintype_card,    hφ, Nat.card_image_of_injective Subtype.val_injective]  · rfl  · exact toFinite {x_1 | φ x_1 = x}