Project-declaredLean 4.33.0-rc1 · mathlib@79d0395a1825

Ent ofsum le

ent_ofsum_le

additive combinatorics entropy probability first estimate

Plain-language statement

Let $X_1',X_2'$ be independent copies of the $\tau$ -minimizers $X_1,X_2$ . Write $k=d[X_1;X_2]$ and $I_1=I[X_1+X_2:X_1'+X_2\mid X_1+X_2+X_1'+X_2']$ . Then the entropy of the four-variable sum obeys $H[X_1+X_2+X_1'+X_2']\le\tfrac12H[X_1]+\tfrac12H[X_2]+(2+\eta)k-I_1$ .

Exact Lean statement

lemma ent_ofsum_le
    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
    H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁]/2 + H[X₂]/2 + (2+p.η)*k - I₁

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma ent_ofsum_le    [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :    H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁]/2 + H[X₂]/2 + (2+p.η)*k - I₁ := by  let D := d[X₁ + X₂' # X₂ + X₁']  let Dcc := d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁']  let D1 := d[p.X₀₁ # X₁]  let Dc1 := d[p.X₀₁ # X₁ | X₁ + X₂']  let D2 := d[p.X₀₂ # X₂]  let Dc2 := d[p.X₀₂ # X₂ | X₂ + X₁']  have lem68 : D + Dcc + I₁ = 2 * k :=    rdist_add_rdist_add_condMutual_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep  have lem610 : Dcc ≥ k - p.η * (Dc1 - D1) - p.η * (Dc2 - D2) :=    condRuzsaDist_of_sums_ge p X₁ X₂ X₁' X₂' hX₁ hX₂ (by fun_prop) (by aesop) h_min  have lem611c : Dc1 - D1 ≤ k / 2 + H[X₁] / 4 - H[X₂] / 4 :=    diff_rdist_le_3 p X₁ X₂ X₁' X₂' hX₁ hX₂' h₂ h_indep  have lem611d : Dc2 - D2 ≤ k / 2 + H[X₂] / 4 - H[X₁] / 4 :=    diff_rdist_le_4 p X₁ X₂ X₁' X₂' hX₂ hX₁' h₁ h_indep  have aux : D + I₁ ≤ (1 + p.η) * k := by    calc D + I₁       ≤ k + p.η * (Dc1 - D1) + p.η * (Dc2 - D2) := ?_     _ ≤ k + p.η * (k / 2 + H[X₁] / 4 - H[X₂] / 4) + p.η * (k / 2 + H[X₂] / 4 - H[X₁] / 4) := ?_     _ = (1 + p.η) * k := by ring    · linarith    · gcongr <;> exact p.hη.le  have ent_sub_eq_ent_add : H[X₁ + X₂' - (X₂ + X₁')] = H[X₁ + X₂' + (X₂ + X₁')] := by    simp [ZModModule.sub_eq_add]  have rw₁ : X₁ + X₂' + (X₂ + X₁') = X₁ + X₂ + X₁' + X₂' := by abel  have ind_aux : IndepFun (X₁ + X₂') (X₂ + X₁') := by    exact iIndepFun.indepFun_add_add h_indep (fun i ↦ by fin_cases i <;> assumption) 0 2 1 3      (by decide) (by decide) (by decide) (by decide)  have ind : D = H[X₁ + X₂' - (X₂ + X₁')] - H[X₁ + X₂'] / 2 - H[X₂ + X₁'] / 2 :=    ind_aux.rdist_eq (by fun_prop) (by fun_prop)  rw [ind, ent_sub_eq_ent_add, rw₁] at aux  have obs : H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁ := by    linarith  have rw₂ : H[X₁ + X₂'] = k + H[X₁]/2 + H[X₂]/2 := by    have HX₂_eq : H[X₂] = H[X₂'] :=      congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₂.map_eq    have k_eq : k = H[X₁ - X₂'] - H[X₁] / 2 - H[X₂'] / 2 := by      have k_eq_aux : k = d[X₁ # X₂'] := h₂.rdist_congr_right hX₁.aemeasurable      rw [k_eq_aux]      exact (h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide)).rdist_eq hX₁ hX₂'    rw [k_eq, ← ZModModule.sub_eq_add, ← HX₂_eq]    ring  have rw₃ : H[X₂ + X₁'] = k + H[X₁]/2 + H[X₂]/2 := by    have HX₁_eq : H[X₁] = H[X₁'] :=      congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₁.map_eq    have k_eq' : k = H[X₁' - X₂] - H[X₁'] / 2 - H[X₂] / 2 := by      have k_eq_aux : k = d[X₁' # X₂] := h₁.rdist_congr_left hX₂.aemeasurable      rw [k_eq_aux]      exact (h_indep.indepFun (show (3 : Fin 4) ≠ 1 by decide)).rdist_eq hX₁' hX₂    rw [add_comm X₂ X₁', k_eq', ← ZModModule.sub_eq_add, ← HX₁_eq]    ring  calc H[X₁ + X₂ + X₁' + X₂']      ≤ H[X₁ + X₂'] / 2 + H[X₂ + X₁'] / 2 + (1 + p.η) * k - I₁  := obs    _ = (k + H[X₁] / 2 + H[X₂] / 2) / 2        + (k + H[X₁] / 2 + H[X₂] / 2) / 2 + (1 + p.η) * k - I₁  := by rw [rw₂, rw₃]    _ = H[X₁] / 2 + H[X₂] / 2 + (2 + p.η) * k - I₁              := by ring

Project: Polynomial Freiman-Ruzsa project
License: Apache-2.0
Commit: a177b2e4abe4
Source: PFR/FirstEstimate.lean:158-215

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