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

condRuzsaDist_comp_right

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:977 to 990

Mathematical statement

Exact Lean statement

lemma condRuzsaDist_comp_right {T' : Type*} [Finite T] [Finite T'] [MeasurableSpace T']
    [MeasurableSingletonClass T'] [IsFiniteMeasure μ']
    (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (e : T → T')
    (hY : Measurable Y) (hW : Measurable W) (he : Measurable e)
    (h'e : Injective e) :
    d[X ; μ # Y | e ∘ W ; μ'] = d[X ; μ # Y | W ; μ']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDist_comp_right {T' : Type*} [Finite T] [Finite T'] [MeasurableSpace T']    [MeasurableSingletonClass T'] [IsFiniteMeasure μ']    (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (e : T → T')    (hY : Measurable Y) (hW : Measurable W) (he : Measurable e)    (h'e : Injective e) :    d[X ; μ # Y | e ∘ W ; μ'] = d[X ; μ # Y | W ; μ'] := by  cases nonempty_fintype T  cases nonempty_fintype T'  rw [condRuzsaDist'_eq_sum' hY (he.comp hW), condRuzsaDist'_eq_sum' hY hW]  have A i : e ⁻¹' {e i} = {i} := by ext x; simp [h'e.eq_iff]  symm  refine Fintype.sum_of_injective e h'e _ _ (fun i hi ↦ ?_) (by simp [Set.preimage_comp, A])  suffices e ⁻¹' {i} = ∅ by simp [Set.preimage_comp, this]  simpa [Set.eq_empty_iff_forall_notMem] using hi