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

multidist_ruzsa_III

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:1265 to 1283

Source documentation

Let I be an indexing set of size m ≥ 2, and let X_[m] be a tuple of G-valued random variables. If the X_i all have the same distribution, then D[X_[m]] ≤ m d[X_i;X_i] for any 1 ≤ i ≤ m.

Exact Lean statement

lemma multidist_ruzsa_III {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (X : ∀ i, Ω i → G) (hident : ∀ j k, IdentDistrib (X j) (X k)) (hmes : ∀ i, Measurable (X i))
    (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume) (hfin : ∀ i, FiniteRange (X i)) (i₀ : Fin m) :
    D[X; hΩ] ≤ m * d[X i₀ # X i₀]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma multidist_ruzsa_III {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))    (X : ∀ i, Ω i → G) (hident : ∀ j k, IdentDistrib (X j) (X k)) (hmes : ∀ i, Measurable (X i))    (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume) (hfin : ∀ i, FiniteRange (X i)) (i₀ : Fin m) :    D[X; hΩ] ≤ m * d[X i₀ # X i₀] := by    have hmnon: NeZero m := by rw [neZero_iff]; linarith    obtain ⟨Ω', mΩ', μ', X', hμ', h_indep, hX'⟩      := independent_copies'_finiteRange (fun (i : Fin (m + 1)) ↦ X 0) (fun _ ↦ hmes 0) (fun i => ℙ)    letI hΩ' : MeasureSpace Ω' := ⟨μ'⟩    have hident' (j k : Fin (m + 1)) : IdentDistrib (X' j) (X' k) :=      (hX' j).2.1.trans (hX' k).2.1.symm    have hfin' (j : Fin (m + 1)) : FiniteRange (X' j) := (hX' j).2.2    have hmes' (j : Fin (m + 1)) : Measurable (X' j) := (hX' j).1    convert multidist_ruzsa_III' hm hmes' hident' h_indep hfin' i₀ using 1    · apply multiDist_copy      intro i      exact (hident i 0).trans (hX' _).2.1.symm    congr 1    apply IdentDistrib.rdist_congr    all_goals exact (hident i₀ 0).trans (hX' _).2.1.symm