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

multidist_eq_zero

PFR.MoreRuzsaDist · PFR/MoreRuzsaDist.lean:1507 to 1524

Source documentation

If D[X_[m]]=0, then for each i ∈ I there is a finite subgroup H_i ≤ G such that d[X_i; U_{H_i}] = 0.

Exact Lean statement

lemma multidist_eq_zero [Finite G] {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*}
    (hΩ : ∀ i, MeasureSpace (Ω i)) (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)
    (X : ∀ i, Ω i → G) (hvanish : D[X; hΩ] = 0) (hmes : ∀ i, Measurable (X i))
    (hfin : ∀ i, FiniteRange (X i)) (i) :
    ∃ (H : AddSubgroup G) (U : Ω i → G), Measurable U ∧ IsUniform H U ∧ d[X i # U] = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma multidist_eq_zero [Finite G] {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*}    (hΩ : ∀ i, MeasureSpace (Ω i)) (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)    (X : ∀ i, Ω i → G) (hvanish : D[X; hΩ] = 0) (hmes : ∀ i, Measurable (X i))    (hfin : ∀ i, FiniteRange (X i)) (i) :    ∃ (H : AddSubgroup G) (U : Ω i → G), Measurable U ∧ IsUniform H U ∧ d[X i # U] = 0 := by  have vanish : ∑ j, d[X j # X j] = 0 := by    apply le_antisymm    · have := multidist_ruzsa_II hm hΩ hprob X hmes hfin      simpa [hvanish] using this    apply Finset.sum_nonneg    intro j _; exact rdist_nonneg (hmes j) (hmes j)  rw [Finset.sum_eq_zero_iff_of_nonneg ?_] at vanish  swap  · intro j _; exact rdist_nonneg (hmes j) (hmes j)  replace vanish :=    exists_isUniform_of_rdist_eq_zero (hmes i) (hmes i) <| vanish i <| Finset.mem_univ i  obtain ⟨H, U, U_mes, U_unif, hdist, hdist'⟩ := vanish  exact ⟨H, U, U_mes, U_unif, hdist⟩