Project-declaredLean 4.33.0-rc1 · mathlib@79d0395a1825

Second estimate

second_estimate

additive combinatorics entropy probability second estimate

Plain-language statement

The second information estimate for $\tau$ -minimizers. Let $X_1',X_2'$ be independent copies of $X_1,X_2$ , set $k=d[X_1;X_2]$ , $I_1=I[X_1+X_2:X_1'+X_2\mid X_1+X_2+X_1'+X_2']$ , and $I_2=I[X_1+X_2:X_1'+X_1\mid X_1+X_2+X_1'+X_2']$ . Then $I_2\le2\eta k+\dfrac{2\eta(2\eta k-I_1)}{1-\eta}$ .

Exact Lean statement

lemma second_estimate : I₂ ≤ 2 * p.η * k + (2 * p.η * (2 * p.η * k - I₁)) / (1 - p.η)

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma second_estimate : I₂ ≤ 2 * p.η * k + (2 * p.η * (2 * p.η * k - I₁)) / (1 - p.η) := by  have hX₁_indep : IndepFun X₁ X₁' (μ := ℙ) := h_indep.indepFun (show 0 ≠ 2 by decide)  have hX₂_indep : IndepFun X₂ X₂' (μ := ℙ) := h_indep.indepFun (show 1 ≠ 3 by decide)  let Y : Fin 4 → Ω → G := ![X₂, X₁, X₂', X₁']  have hY : ∀ i, Measurable (Y i) := fun i => by fin_cases i <;> assumption  have hY_indep : iIndepFun Y := by exact h_indep.reindex_four_badc  have h := sum_of_rdist_eq_char_2 Y hY_indep hY  rw [show Y 0 = X₂ by rfl, show Y 1 = X₁ by rfl, show Y 2 = X₂' by rfl, show Y 3 = X₁' by rfl] at h  rw [← h₂.rdist_congr h₁, rdist_symm, rdist_symm (X := X₂ + X₂'),    condRuzsaDist_symm (Z := X₂ + X₂') (W := X₁ + X₁') (hX₂.add hX₂') (hX₁.add hX₁'),    ← two_mul] at h  replace h : 2 * k = d[X₁ + X₁' # X₂ + X₂'] + d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂']      + I[X₁ + X₂ : X₁ + X₁'|X₁ + X₂ + X₁' + X₂'] := by    convert h using 3 <;> abel  have h' := condRuzsaDistance_ge_of_min p h_min hX₁ hX₂ (X₁ + X₁') (X₂ + X₂') (hX₁.add hX₁')    (hX₂.add hX₂')  have h₁' := condRuzsaDist_diff_le''' ℙ p.hmeas1 hX₁ hX₁' hX₁_indep  have h₂' := condRuzsaDist_diff_le''' ℙ p.hmeas2 hX₂ hX₂' hX₂_indep  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₂'  have h'' : I₂ ≤ p.η * (d[X₁ # X₁] + d[X₂ # X₂]) := by    simp_rw [← add_comm X₁ X₁']    have h₁'' := mul_le_mul_of_nonneg_left h₁' (show 0 ≤ p.η by linarith [p.hη])    have h₂'' := mul_le_mul_of_nonneg_left h₂' (show 0 ≤ p.η by linarith [p.hη])    have := rdist_of_sums_ge' p _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min    linarith  nth_rewrite 1 [mul_div_assoc, ← mul_add, mul_assoc, mul_left_comm]  refine h''.trans (mul_le_mul_of_nonneg_left ?_ (show 0 ≤ p.η by linarith [p.hη]))  exact second_estimate_aux p X₁ X₂ X₁' X₂' hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min

Project: Polynomial Freiman-Ruzsa project
License: Apache-2.0
Commit: a177b2e4abe4
Source: PFR/SecondEstimate.lean:103-133

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