Plain-language statement
A Ruzsa-distance lower bound for sums of independent copies. Let be independent copies of the -minimizers , and set . Then
Exact Lean statement
lemma rdist_of_sums_ge' : d[X₁ + X₁' # X₂ + X₂'] ≥ k - p.η * (d[X₁ # X₁] + d[X₂ # X₂]) / 2
Formal artifact
Lean source
lemma rdist_of_sums_ge' : d[X₁ + X₁' # X₂ + X₂'] ≥ k - p.η * (d[X₁ # X₁] + d[X₂ # X₂]) / 2 := by refine LE.le.ge (LE.le.trans ?_ (distance_ge_of_min p h_min (hX₁.add hX₁') (hX₂.add hX₂'))) rw [sub_sub, sub_le_sub_iff_left k, ← mul_add,mul_div_assoc] refine mul_le_mul_of_nonneg_left ?_ (by linarith [p.hη]) have h₁' := condRuzsaDist_diff_le' ℙ p.hmeas1 hX₁ hX₁' (h_indep.indepFun (show 0 ≠ 2 by decide)) have h₂' := condRuzsaDist_diff_le' ℙ p.hmeas2 hX₂ hX₂' (h_indep.indepFun (show 1 ≠ 3 by decide)) rw [h₁.entropy_congr, add_sub_cancel_right, ← (IdentDistrib.refl hX₁.aemeasurable).rdist_congr h₁] at h₁' rw [h₂.entropy_congr, add_sub_cancel_right, ← (IdentDistrib.refl hX₂.aemeasurable).rdist_congr h₂] at h₂' linarith- Project
- Polynomial Freiman-Ruzsa project
- License
- Apache-2.0
- Commit
- a177b2e4abe4
- Source
- PFR/SecondEstimate.lean:62-72
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
Approx hom pfr
approx_hom_pfr
Project documentation
An approximate-homomorphism theorem for finite elementary abelian -groups. Let and . If at least a proportion of pairs satisfy , then there are an additive homomorphism and a constant such that for at least values of .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
Better PFR conjecture
better_PFR_conjecture
Plain-language statement
If is finite non-empty with , then there exists a subgroup of with such that can be covered by at most translates of .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
Better PFR conjecture
better_PFR_conjecture'
Project documentation
Polynomial Freiman-Ruzsa theorem with exponent , without a finite ambient-group assumption. Let be a nonempty finite subset of an elementary abelian -group. If , then there are a finite subspace and a finite set such that , , and .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.