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

ProbabilityTheory.setRuzsaDist_le

PFR.ForMathlib.Entropy.RuzsaSetDist · PFR/ForMathlib/Entropy/RuzsaSetDist.lean:110 to 128

Source documentation

Ruzsa distance between sets is controlled by the doubling constant.

Exact Lean statement

lemma setRuzsaDist_le (A B : Set G) [h'A : Finite A] [h'B : Finite B]
    (hA : A.Nonempty) (hB : B.Nonempty) :
    dᵤ[A # B] ≤ log (Nat.card (A-B)) - log (Nat.card A) / 2 - log (Nat.card B) / 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma setRuzsaDist_le (A B : Set G) [h'A : Finite A] [h'B : Finite B]    (hA : A.Nonempty) (hB : B.Nonempty) :    dᵤ[A # B] ≤ log (Nat.card (A-B)) - log (Nat.card A) / 2 - log (Nat.card B) / 2 := by  have : Finite (A - B) := Set.Finite.sub h'A h'B  have := hA.to_subtype  have := hB.to_subtype  simp_rw [setRuzsaDist, Kernel.rdistm, ProbabilityTheory.entropy_of_uniformOn]  gcongr  convert measureEntropy_le_card_aux (A-B).toFinite.toFinset ?_  · rw [Nat.card_coe_set_eq]    exact Set.ncard_eq_toFinset_card (A - B)  · exact Measure.isProbabilityMeasure_map (Measurable.aemeasurable measurable_sub)  rw [Measure.map_apply measurable_sub .of_discrete]  apply measure_mono_null (t := (Aᶜ ×ˢ Set.univ) ∪ (Set.univ ×ˢ Bᶜ))  · intro (x, y)    contrapose!    aesop (add unsafe Set.sub_mem_sub, simp not_or)  apply measure_union_null  all_goals simp [uniformOn_apply ‹Finite A›, uniformOn_apply ‹Finite B›]