ent_of_proj_le

lemma ent_of_proj_le {UH : Ω' → G} [FiniteRange UH]    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']    (hX : Measurable X) (hU : Measurable UH) {H : AddSubgroup G} (hH : Set.Finite (H : Set G))    -- TODO: infer from [FiniteRange UH]?    (hunif : IsUniform H UH μ') :    H[(QuotientAddGroup.mk' H) ∘ X; μ] ≤ 2 * d[X; μ # UH ; μ'] := by  obtain ⟨ν, X', UH', hν, hX', hUH', h_ind, h_id_X', h_id_UH', _, _⟩ :=    independent_copies_finiteRange hX hU μ μ'  replace hunif : IsUniform H UH' ν :=    IsUniform.of_identDistrib hunif h_id_UH'.symm .of_discrete  rewrite [← (h_id_X'.comp (by fun_prop)).entropy_congr, ← h_id_X'.rdist_congr h_id_UH']  let π := ⇑(QuotientAddGroup.mk' H)  let νq := Measure.map (π ∘ X') ν  have : Countable (HasQuotient.Quotient G H) := Quotient.countable  have : MeasurableSingletonClass (HasQuotient.Quotient G H) :=    { measurableSet_singleton := fun _ ↦ measurableSet_quotient.mpr .of_discrete }  have : Finite H := hH  have : H[X' - UH' | π ∘ X' ; ν] = H[UH' ; ν] := by    have h_meas_le : ∀ y ∈ FiniteRange.toFinset (π ∘ X'),        νq.real {y} * H[X' - UH' | (π ∘ X') ← y ; ν] ≤ νq.real {y} * H[UH' ; ν] := by      intro x _      gcongr      let ν' := ν[|π ∘ X' ← x]      let π' := QuotientAddGroup.mk (s := H)      have h_card : (π' ⁻¹' {x}).ncard = Nat.card H := Nat.card_congr <|        (QuotientAddGroup.preimageMkEquivAddSubgroupProdSet H _).trans <| Equiv.prodUnique H _      have : Finite (π' ⁻¹' {x}) :=        Nat.finite_of_card_ne_zero <| h_card.trans_ne <| Nat.pos_iff_ne_zero.mp (Nat.card_pos)      convert! entropy_le_log_card_of_mem_finite this (hX'.sub hUH') ?_      · simp [hunif.entropy_eq' hH hUH', h_card]        simp [← Nat.card_coe_set_eq]      let T : Set (G × G) := ((π' ∘ X') ⁻¹' {x})ᶜ      let U : Set (G × G) := UH' ⁻¹' Hᶜ      have h_subset : (X' - UH') ⁻¹' (π' ⁻¹' {x})ᶜ ⊆ T ∪ U :=        fun ω hω ↦ Classical.byContradiction fun h ↦ by simp_all [not_or, T, U, π']      refine mem_ae_iff.mpr (nonpos_iff_eq_zero.mp ?_)      calc        _ ≤ ν' T + ν' U := (measure_mono h_subset).trans (measure_union_le T U)        _ = ν' T + 0 := congrArg _ <| by          simp only [ν', ProbabilityTheory.cond, Measure.smul_apply, smul_eq_mul]          rw [nonpos_iff_eq_zero.mp <|            (restrict_apply_le _ U).trans_eq hunif.measure_preimage_compl, mul_zero]        _ = 0 := by          have : restrict ν (π ∘ X' ⁻¹' {x}) T = 0 := by            simp [restrict_apply .of_discrete, T, π', π]          simp only [ν', ProbabilityTheory.cond, Measure.smul_apply, smul_eq_mul]          simp [this]    have h_one : ∑ x ∈ FiniteRange.toFinset (π ∘ X'), νq.real {x} = 1 := by      rewrite [sum_measureReal_singleton]      apply (ENNReal.toReal_eq_one_iff _).mpr      have := isProbabilityMeasure_map (μ := ν) <| .of_discrete (f := π ∘ X')      rewrite [← measure_univ (μ := νq), ← FiniteRange.range]      let rng := Set.range (π ∘ X')      have h_compl : νq rngᶜ = 0 := ae_map_mem_range (π ∘ X') .of_discrete ν      rw [← measure_add_measure_compl (MeasurableSet.of_discrete (s := rng)),        h_compl, add_zero]    have := FiniteRange.sub X' UH'    have h_ge : H[X' - UH' | π ∘ X' ; ν] ≥ H[UH' ; ν] := calc      _ ≥ H[X' - UH' | X' ; ν] := condEntropy_comp_ge ν hX' (hX'.sub hUH') π      _ = H[UH' | X' ; ν] := condEntropy_sub_left hUH' hX'      _ = H[UH' ; ν] := h_ind.symm.condEntropy_eq_entropy hUH' hX'    have h_le : H[X' - UH' | π ∘ X' ; ν] ≤ H[UH' ; ν] := by      rewrite [condEntropy_eq_sum _ _ _ .of_discrete]      apply (Finset.sum_le_sum h_meas_le).trans      rewrite [← Finset.sum_mul, h_one, one_mul]      rfl    exact h_le.ge_iff_eq.mp h_ge  have : H[X' - UH' ; ν] = H[π ∘ X' ; ν] + H[UH' ; ν] := by calc    _ = H[⟨X' - UH', π ∘ (X' - UH')⟩ ; ν] := (entropy_prod_comp (hX'.sub hUH') ν π).symm    _ = H[⟨X' - UH', π ∘ X'⟩ ; ν] := by      apply IdentDistrib.entropy_congr <| IdentDistrib.of_ae_eq (Measurable.aemeasurable        .of_discrete) <| mem_ae_iff.mpr _      convert hunif.measure_preimage_compl      ext; simp [π]    _ = H[π ∘ X' ; ν] + H[UH' ; ν] := by      rewrite [chain_rule ν (by exact hX'.sub hUH') .of_discrete]      congr  have : d[X' ; ν # UH' ; ν] = H[π ∘ X' ; ν] + (H[UH' ; ν] - H[X' ; ν]) / 2 := by    rewrite [h_ind.rdist_eq hX' hUH']    linarith only [this]  linarith only [this, (abs_le.mp (diff_ent_le_rdist hX' hUH' (μ := ν) (μ' := ν))).2]