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

multidist_ruzsa_I

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:1140 to 1153

Source documentation

Let m ≥ 1, and let X_[m] be a tuple of G-valued random variables. Then ∑ (1 ≤ j, k ≤ m, j ≠ k), d[X_j; -X_k] ≤ m(m - 1) D[X_[m]].

Exact Lean statement

lemma multidist_ruzsa_I {m : ℕ} (hm : m ≥ 1) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    {X : ∀ i, Ω i → G} (hmes : ∀ j, Measurable (X j))
    (hprob : ∀ j, IsProbabilityMeasure (hΩ j).volume) (hfin : ∀ j, FiniteRange (X j)) :
    ∑ j, ∑ k, (if j = k then (0:ℝ) else d[X j # -X k]) ≤ m * (m - 1) * D[X; hΩ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma multidist_ruzsa_I {m : ℕ} (hm : m ≥ 1) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))    {X : ∀ i, Ω i → G} (hmes : ∀ j, Measurable (X j))    (hprob : ∀ j, IsProbabilityMeasure (hΩ j).volume) (hfin : ∀ j, FiniteRange (X j)) :    ∑ j, ∑ k, (if j = k then (0:ℝ) else d[X j # -X k]) ≤ m * (m - 1) * D[X; hΩ] := by  obtain ⟨Ω', mΩ', μ', X', hμ', h_indep, hX'⟩    := independent_copies'_finiteRange X hmes (fun i => ℙ)  convert multidist_ruzsa_I_indep hm ⟨μ'⟩ X' h_indep (fun i ↦ (hX' i).1) (fun i ↦ (hX' i).2.2)    using 1  · congr! with j hj k hk    exact (hX' j).2.1.symm.rdist_congr <| (hX' k).2.1.symm.comp measurable_neg  congr 1  apply multiDist_copy  intro i  exact (hX' i).2.1.symm