Project-declaredLean 4.33.0-rc1 · mathlib@79d0395a1825

Rdist le of is Uniform of card add le

rdist_le_of_isUniform_of_card_add_le

additive combinatorics entropy probability main

Plain-language statement

A uniform distribution on a set with doubling constant K has self Rusza distance at most log K.

Exact Lean statement

theorem rdist_le_of_isUniform_of_card_add_le [A_fin : Finite A] [MeasurableSpace G]
    [MeasurableSingletonClass G]
    (hA₀ : A.Nonempty) (hA : (A - A).ncard ≤ K * A.ncard)
    {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}
    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ log K

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem rdist_le_of_isUniform_of_card_add_le [A_fin : Finite A] [MeasurableSpace G]    [MeasurableSingletonClass G]    (hA₀ : A.Nonempty) (hA : (A - A).ncard ≤ K * A.ncard)    {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ log K := by  obtain ⟨A_pos, AA_pos, K_pos⟩ : (0 : ℝ) < A.ncard ∧ (0 : ℝ) < (A - A).ncard ∧ 0 < K :=    PFR_conjecture_pos_aux A.toFinite hA₀ hA  rcases independent_copies_two U₀meas U₀meas with ⟨Ω, mΩ, U, U', hP, hU, hU', UU'_indep, idU, idU'⟩  have Uunif : IsUniform A U := U₀unif.of_identDistrib idU.symm .of_discrete  have U'unif : IsUniform A U' := U₀unif.of_identDistrib idU'.symm .of_discrete  have IU : d[U # U'] ≤ log K := by    have I : H[U - U'] ≤ log (A - A).ncard := by      apply entropy_le_log_card_of_mem_finite (Set.Finite.sub A_fin A_fin) (hU.sub hU')      filter_upwards [Uunif.ae_mem, U'unif.ae_mem] with ω h1 h2      exact Set.sub_mem_sub h1 h2    have J : log (A - A).ncard ≤ log K + log A.ncard := by      rw [← log_mul K_pos.ne' A_pos.ne']; gcongr    rw [UU'_indep.rdist_eq hU hU', Uunif.entropy_eq' A_fin hU, U'unif.entropy_eq' A_fin hU']    linarith  rwa [idU.rdist_congr idU'] at IU

Project: Polynomial Freiman-Ruzsa project
License: Apache-2.0
Commit: a177b2e4abe4
Source: PFR/Main.lean:113-132

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.33.0-rc1

Approx hom pfr

approx_hom_pfr

Project documentation

An approximate-homomorphism theorem for finite elementary abelian $2$ -groups. Let $f:G\to G'$ and $K>0$ . If at least a proportion $K^{-1}$ of pairs $(x,y)\in G^2$ satisfy $f(x+y)=f(x)+f(y)$ , then there are an additive homomorphism $\varphi:G\to G'$ and a constant $c\in G'$ such that $f(x)=\varphi(x)+c$ for at least $|G|/(2^{144}K^{122})$ values of $x$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture

Plain-language statement

If $A \subset {\bf F}_2^n$ is finite non-empty with $|A+A| \leq K|A|$ , then there exists a subgroup $H$ of ${\bf F}_2^n$ with $|H| \leq |A|$ such that $A$ can be covered by at most $2K^9$ translates of $H$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture'

Project documentation

Polynomial Freiman-Ruzsa theorem with exponent $9$ , without a finite ambient-group assumption. Let $A$ be a nonempty finite subset of an elementary abelian $2$ -group. If $|A+A|\le K|A|$ , then there are a finite subspace $H$ and a finite set $c$ such that $A\subseteq c+H$ , $|c|<2K^9$ , and $|H|\le|A|$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record