Project-declaredLean 4.33.0-rc1 · mathlib@79d0395a1825

I₃ eq

I₃_eq

additive combinatorics entropy probability endgame

Plain-language statement

A symmetry identity in the $\tau$ -minimizer endgame. Let $X_1',X_2'$ be independent copies of $X_1,X_2$ , and set $U=X_1+X_2$ , $V=X_1'+X_2$ , $W=X_1'+X_1$ , and $S=X_1+X_2+X_1'+X_2'$ . Then the conditional mutual informations agree: $I[V:W\mid S]=I[U:W\mid S]$ .

Exact Lean statement

lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂ := by  have h_indep2 : iIndepFun ![X₁', X₂, X₁, X₂'] := by    exact h_indep.reindex_four_cbad  have hident : IdentDistrib (fun a (i : Fin 4) => ![X₁, X₂, X₁', X₂'] i a)    (fun a (j : Fin 4) => ![X₁', X₂, X₁, X₂'] j a) := by    exact { aemeasurable_fst := by              apply Measurable.aemeasurable              rw [measurable_pi_iff]              intro x              fin_cases x;              all_goals aesop            aemeasurable_snd := by              apply Measurable.aemeasurable              rw [measurable_pi_iff]              intro x              fin_cases x;              all_goals aesop            map_eq := by              rw [(ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map                (Fin.cases hX₁.aemeasurable <| Fin.cases hX₂.aemeasurable <|                Fin.cases hX₁'.aemeasurable <| Fin.cases hX₂'.aemeasurable Fin.rec0)).mp h_indep,                (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map                (Fin.cases hX₁'.aemeasurable <| Fin.cases hX₂.aemeasurable <|                Fin.cases hX₁.aemeasurable <| Fin.cases hX₂'.aemeasurable Fin.rec0)).mp h_indep2]              congr              ext i              fin_cases i              all_goals simp [h₁.map_eq] }  have hmeas1 : Measurable (fun p : Fin 4 → G => (p 0 + p 1, p 0 + p 1 + p 2 + p 3)) := by    fun_prop  have hUVS : IdentDistrib (prod U S) (prod V S) := by    convert! hident.comp hmeas1; simp; abel  have hUVWS : IdentDistrib (prod (prod U W) S) (prod (prod V W) S) := by    convert (hident.comp hmeas2) <;> simp <;> abel  have hU : Measurable U := Measurable.add hX₁ hX₂  have hV : Measurable V := Measurable.add hX₁' hX₂  have hW : Measurable W := Measurable.add hX₁' hX₁  have hS : Measurable S := by fun_prop  rw [condMutualInfo_eq hV hW hS, condMutualInfo_eq hU hW hS, chain_rule'' ℙ hU hS,    chain_rule'' ℙ hV hS, chain_rule'' ℙ hW hS, chain_rule'' ℙ _ hS, chain_rule'' ℙ _ hS,    hUVS.entropy_congr, hUVWS.entropy_congr]  · exact Measurable.prod hU hW  · exact Measurable.prod hV hW

Project: Polynomial Freiman-Ruzsa project
License: Apache-2.0
Commit: a177b2e4abe4
Source: PFR/Endgame.lean:87-129

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