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

ProbabilityTheory.setRuzsaDist_triangle

PFR.ForMathlib.Entropy.RuzsaSetDist · PFR/ForMathlib/Entropy/RuzsaSetDist.lean:55 to 66

Source documentation

Ruzsa distance between sets obeys the triangle inequality.

Exact Lean statement

lemma setRuzsaDist_triangle (A B C : Set G) [hA : Finite A] [hB : Finite B] [hC : Finite C]
    [Nonempty A] [Nonempty B] [Nonempty C] : dᵤ[A # C] ≤ dᵤ[A # B] + dᵤ[B # C]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma setRuzsaDist_triangle (A B C : Set G) [hA : Finite A] [hB : Finite B] [hC : Finite C]    [Nonempty A] [Nonempty B] [Nonempty C] : dᵤ[A # C] ≤ dᵤ[A # B] + dᵤ[B # C] := by  obtain ⟨ Ω, mΩ, UA, hμ, hUA_mes, hUA_unif, -, hUA_fin ⟩ :=    exists_isUniform_measureSpace' A hA .of_subtype  obtain ⟨ Ω', mΩ', UB, hμ', hUB_mes, hUB_unif, -, hUB_fin ⟩ :=    exists_isUniform_measureSpace' B hB .of_subtype  obtain ⟨ Ω'', mΩ'', UC, hμ'', hUC_mes, hUC_unif, -, hUC_fin ⟩ :=    exists_isUniform_measureSpace' C hC .of_subtype  rw [setRuzsaDist_eq_rdist hUA_unif hUB_unif hUA_mes hUB_mes,    setRuzsaDist_eq_rdist hUB_unif hUC_unif hUB_mes hUC_mes,    setRuzsaDist_eq_rdist hUA_unif hUC_unif hUA_mes hUC_mes]  exact rdist_triangle hUA_mes hUB_mes hUC_mes