Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 83 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

83 results

Clear filters
Project-declaredLean 4.33.0-rc1

Second estimate

second_estimate

Plain-language statement

The second information estimate for τ\tau-minimizers. Let X1,X2X_1',X_2' be independent copies of X1,X2X_1,X_2, set k=d[X1;X2]k=d[X_1;X_2], I1=I[X1+X2:X1+X2X1+X2+X1+X2]I_1=I[X_1+X_2:X_1'+X_2\mid X_1+X_2+X_1'+X_2'], and I2=I[X1+X2:X1+X1X1+X2+X1+X2]I_2=I[X_1+X_2:X_1'+X_1\mid X_1+X_2+X_1'+X_2']. Then I22ηk+2η(2ηkI1)1ηI_2\le2\eta k+\dfrac{2\eta(2\eta k-I_1)}{1-\eta}.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Sifting cor

sifting_cor

Plain-language statement

A dependent-random-choice corollary. Let AA be nonempty, let 0<ε10<\varepsilon\le 1 and δ>0\delta>0, and let pp be a nonzero even integer satisfying ε1log(2/δ)p\varepsilon^{-1}\log(2/\delta)\le p. Then there are sets A1,A2A_1,A_2 such that the normalized difference distribution μA1μA2\mu_{A_1}\mathbin{\circleddash}\mu_{A_2} assigns mass at least 1δ1-\delta to the source's sifted set sp,ε(A)s_{p,\varepsilon}(A). Both sets retain explicit density: dens(Ai)14dens(A)2p\operatorname{dens}(A_i)\ge \tfrac14\operatorname{dens}(A)^{2p} for i=1,2i=1,2.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Sub cond Multi Distance le

sub_condMultiDistance_le

Project documentation

If (Xi)1im(X_i)_{1 \leq i \leq m} is a τ\tau-minimizer, and k:=D[(Xi)1im]k := D[(X_i)_{1 \leq i \leq m}], then for any other tuples (Xi)1im(X'_i)_{1 \leq i \leq m} and (Yi)1im(Y_i)_{1 \leq i \leq m} with the XiX'_i G$-valued, one has kD[(Xi)1im(Yi)1im]ηi=1md[Xi;XiYi]. k - D[(X'_i)_{1 \leq i \leq m} | (Y_i)_{1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i|Y_i].

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Sum dist diff le

sum_dist_diff_le

Plain-language statement

In the τ\tau-minimizer endgame, let X1,X2X_1',X_2' be independent copies of X1,X2X_1,X_2, set k=d[X1;X2]k=d[X_1;X_2], U=X1+X2U=X_1+X_2, V=X1+X2V=X_1'+X_2, W=X1+X1W=X_1'+X_1, S=X1+X2+X1+X2S=X_1+X_2+X_1'+X_2', and I1=I[U:VS]I_1=I[U:V\mid S]. If c[AS#AS]=i=12(d[Xi0;AS]d[Xi0;Xi])c[A\mid S\#A\mid S]=\sum_{i=1}^2\bigl(d[X_i^0;A\mid S]-d[X_i^0;X_i]\bigr), then c[US#US]+c[VS#VS]+c[WS#WS](63η)k+3(2ηkI1)c[U\mid S\#U\mid S]+c[V\mid S\#V\mid S]+c[W\mid S\#W\mid S]\le(6-3\eta)k+3(2\eta k-I_1).

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Sum of rdist eq

sum_of_rdist_eq

Plain-language statement

Let Y1,Y2,Y3Y_1,Y_2,Y_3 and Y4Y_4 be independent GG-valued random variables. Then d[Y1Y3;Y2Y4]+d[Y1Y1Y3;Y2Y2Y4]d[Y_1-Y_3; Y_2-Y_4] + d[Y_1|Y_1-Y_3; Y_2|Y_2-Y_4] +I[Y1Y2:Y2Y4Y1Y2Y3+Y4]=d[Y1;Y2]+d[Y3;Y4]. + I[Y_1-Y_2 : Y_2 - Y_4 | Y_1-Y_2-Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Sum of rdist eq step cond Mutual Info

sum_of_rdist_eq_step_condMutualInfo

Plain-language statement

For four measurable random variables Y0,Y1,Y2,Y3Y_0,Y_1,Y_2,Y_3 in a finite abelian group, the conditional mutual-information term used in the fibring identity can be reduced to I ⁣[(Y0Y1,Y2Y3):(Y0Y2,Y1Y3)|Y0Y1Y2+Y3]=I[Y0Y1:Y1Y3Y0Y1Y2+Y3].I\!\left[(Y_0-Y_1,Y_2-Y_3):(Y_0-Y_2,Y_1-Y_3)\,\middle|\,Y_0-Y_1-Y_2+Y_3\right]=I[Y_0-Y_1:Y_1-Y_3\mid Y_0-Y_1-Y_2+Y_3].

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record