Learning path

Each declaration appears after its prerequisites.

approx_hom_pfr Let $G, G'$ be finite abelian $2$-groups
dual_iso Non canonical isomorphism between a finite 2-torsion group and its dual into ZMod 2
ProbabilityTheory.iIndepFun.sum_elim For Mathlib?
mutual_information_le Documented declaration: mutual_information_le
hmeas2 (Mantas) this times out in the proof below
I₃_eq The quantity I_3 = I[V:W|S] is equal to I_2
sum_condMutual_le I[U : V | S] + I[V : W | S] + I[W : U | S] is less than or equal to 6 * η * k - (1 - 5 * η) / (1 - η) * (2 * η * k - I₁)
sum_dist_diff_le $$ \sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \big(d[X^0_i;A|S] - d[X^0_i;X_i]\big)$$ is less than or equal to $$ \leq (6 - 3\eta) k + 3(2 \eta k - I_1).$$
sum_uvw_eq_zero U + V + W = 0
construct_good_prelim Documented declaration: construct_good_prelim
construct_good Documented declaration: construct_good
tau_strictly_decreases_aux If d[X₁ ; X₂] > 0 then there are G-valued random variables X₁', X₂' such that Phrased in the contrapositive form for convenience of proof
tau_strictly_decreases If $d[X_1;X_2] > 0$ then there are $G$-valued random variables $X'_1, X'_2$ such that $\tau[X'_1;X'_2] < \tau[X_1;X_2]$
rdist_of_indep_eq_sum_fibre Documented declaration: rdist_of_indep_eq_sum_fibre
rdist_of_hom_le \[d[X;Y]\geq d[\pi(X);\pi(Y)].\]
sum_of_rdist_eq_step_condRuzsaDist The conditional Ruzsa Distance step of sum_of_rdist_eq
sum_of_rdist_eq_step_condMutualInfo The conditional mutual information step of sum_of_rdist_eq
sum_of_rdist_eq Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables
sum_of_rdist_eq_char_2 Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables
rdist_add_rdist_add_condMutual_eq Documented declaration: rdist_add_rdist_add_condMutual_eq
rdist_of_sums_ge The distance $d[X_1+\tilde X_2; X_2+\tilde X_1]$ is at least $$k - \eta (d[X^0_1; X_1+\tilde X_2] - d[X^0_1; X_1]) - \eta (d[X^0_2; X_2+\tilde X_1] - d[X^0_2; X_2]).$$
condRuzsaDist_of_sums_ge Documented declaration: condRuzsaDist_of_sums_ge
diff_rdist_le_1 d[X₀₁ # X₁ + X₂'] - d[X₀₁ # X₁] ≤ k/2 + H[X₂]/4 - H[X₁]/4
diff_rdist_le_2 $$ d[X^0_2;X_2+\tilde X_1] - d[X^0_2; X_2] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$
diff_rdist_le_3 $$ d[X_1^0;X_1|X_1+\tilde X_2] - d[X_1^0;X_1] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$
diff_rdist_le_4 $$ d[X_2^0; X_2|X_2+\tilde X_1] - d[X_2^0; X_2] \leq \tfrac{1}{2}k + \tfrac{1}{4} \mathbb{H}[X_2] - \tfrac{1}{4} \mathbb{H}[X_1].$$
first_estimate We have $I_1 \leq 2 \eta k$
ent_ofsum_le $$\mathbb{H}[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} \mathbb{H}[X_1]+\tfrac{1}{2} \mathbb{H}[X_2] + (2 + \eta) k - I_1.$$
AffineSpace.finrank The dimension of the affine span over ℤ of a subset of an additive group
ProbabilityTheory.IndepFun.identDistrib_cond If A is independent from B, then conditioning on an event given by B does not change the distribution of A
ProbabilityTheory.IndepFun.cond_left If A is independent of B, then they remain independent when conditioning on an event of the form A ∈ s of positive probability
ProbabilityTheory.IndepFun.cond_right If A is independent of B, then they remain independent when conditioning on an event of the form B ∈ t of positive probability
ProbabilityTheory.IndepFun.cond If A is independent of B, then they remain independent when conditioning on an event of the form A ∈ s ∩ B ∈ t of positive probability
ProbabilityTheory.CondIndepFun The assertion that f and g are conditionally independent relative to h
ProbabilityTheory.CondIndepFun.comp_right Composing independent functions with a measurable embedding of conull range gives independent functions
ProbabilityTheory.condIndep_copies For X, Y random variables, there exist conditionally independent trials X_1, X_2, Y'
ProbabilityTheory.condIndep_copies' For X, Y random variables, there exist conditionally independent trials X₁, X₂, Y'
ProbabilityTheory.entropy_def Entropy of a random variable agrees with entropy of its distribution
ProbabilityTheory.entropy_eq_kernel_entropy Entropy of a random variable is also the kernel entropy of the distribution over a Dirac mass
ProbabilityTheory.entropy_zero_measure Any variable on a zero measure space has zero entropy
ProbabilityTheory.entropy_congr Two variables that agree almost everywhere, have the same entropy
ProbabilityTheory.entropy_nonneg Entropy is always non-negative
ProbabilityTheory.IdentDistrib.entropy_congr Two variables that have the same distribution, have the same entropy
ProbabilityTheory.entropy_le_log_card Entropy is at most the logarithm of the cardinality of the range
ProbabilityTheory.entropy_le_log_card_of_mem Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in
ProbabilityTheory.entropy_le_log_card_of_mem_finite Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in
ProbabilityTheory.entropy_eq_sum H[X] = ∑ₛ P[X=s] log 1 / P[X=s]
ProbabilityTheory.entropy_cond_eq_sum H[X | Y=y] = ∑_s P[X=s | Y=y] log 1/(P[X=s | Y=y])
ProbabilityTheory.entropy_comp_of_injective If X, Y are S-valued and T-valued random variables, and Y = f(X) for some injection f : S \to T, then H[Y] = H[X]
ProbabilityTheory.entropy_const The entropy of any constant is zero
ProbabilityTheory.IsUniform.entropy_eq If X is uniformly distributed on H, then H[X] = log |H|
ProbabilityTheory.IsUniform.entropy_eq' Variant of IsUniform.entropy_congr where H is a finite Set rather than Finset
ProbabilityTheory.entropy_eq_log_card If X is S-valued random variable, then H[X] = log |S| if and only if X is uniformly distributed
ProbabilityTheory.prob_ge_exp_neg_entropy If X is an S-valued random variable, then there exists s ∈ S such that P[X = s] ≥ \exp(- H[X])
ProbabilityTheory.prob_ge_exp_neg_entropy' If X is an S-valued random variable, then there exists s ∈ S such that P[X=s] ≥ \exp(-H[X])
ProbabilityTheory.const_of_nonpos_entropy If X is an S-valued random variable of non-positive entropy, then X is almost surely constant
ProbabilityTheory.entropy_prod_comp H[X, f(X)] = H[X]
ProbabilityTheory.entropy_comm H[X, Y] = H[Y, X]
ProbabilityTheory.entropy_assoc H[(X, Y), Z] = H[X, (Y, Z)]
ProbabilityTheory.condEntropy_eq_kernel_entropy Conditional entropy of a random variable is equal to the entropy of its conditional kernel
ProbabilityTheory.condEntropy_zero_measure Any random variable on a zero measure space has zero conditional entropy
ProbabilityTheory.condEntropy_nonneg Conditional entropy is non-negative
ProbabilityTheory.condEntropy_le_log_card Conditional entropy is at most the logarithm of the cardinality of the range
ProbabilityTheory.condEntropy_eq_sum H[X|Y] = ∑_y P[Y=y] H[X|Y=y]
ProbabilityTheory.condEntropy_eq_sum_fintype H[X|Y] = ∑_y P[Y=y] H[X|Y=y]
ProbabilityTheory.condEntropy_eq_sum_sum H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$
ProbabilityTheory.condEntropy_eq_sum_sum_fintype H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$
ProbabilityTheory.condEntropy_eq_sum_prod Same as previous lemma, but with a sum over a product space rather than a double sum
ProbabilityTheory.condEntropy_of_injective If X : Ω → S, Y : Ω → T are random variables, and f : T × S → U is injective for each fixed t ∈ T, then H[f(Y, X) | Y] = H[X | Y]
ProbabilityTheory.condEntropy_comp_of_injective A weaker version of the above lemma in which f is independent of Y
ProbabilityTheory.condEntropy_comm H[X, Y| Z] = H[Y, X| Z]
ProbabilityTheory.chain_rule' One form of the chain rule : H[X, Y] = H[X] + H[Y | X]
ProbabilityTheory.chain_rule Another form of the chain rule : H[X, Y] = H[Y] + H[X | Y]
ProbabilityTheory.chain_rule'' Another form of the chain rule : H[X | Y] = H[X, Y] - H[Y]
ProbabilityTheory.IdentDistrib.condEntropy_eq Two pairs of variables that have the same joint distribution, have the same conditional entropy
ProbabilityTheory.condEntropy_of_injective' If X : Ω → S and Y : Ω → T are random variables, and f : T → U is an injection then H[X | f(Y)] = H[X | Y]
ProbabilityTheory.condEntropy_comp_self H[X | f(X)] = H[X] - H[f(X)]
ProbabilityTheory.cond_chain_rule' If X : Ω → S, Y : Ω → T, Z : Ω → U are random variables, then H[X, Y | Z] = H[X | Z] + H[Y|X, Z]
ProbabilityTheory.cond_chain_rule H[X, Y | Z] = H[Y | Z] + H[X | Y, Z]
ProbabilityTheory.entropy_comp_le Data-processing inequality for the entropy: H[f(X)] ≤ H[X]
ProbabilityTheory.entropy_of_comp_eq_of_comp A Schroder-Bernstein type theorem for entropy : if two random variables are functions of each other, then they have the same entropy
ProbabilityTheory.IdentDistrib.mutualInfo_eq Substituting variables for ones with the same distributions doesn't change the mutual information
ProbabilityTheory.mutualInfo_nonneg Mutual information is non-negative
ProbabilityTheory.entropy_pair_le_add Subadditivity of entropy
ProbabilityTheory.mutualInfo_eq_zero I[X : Y] = 0 iff X, Y are independent
ProbabilityTheory.mutualInfo_const The mutual information with a constant is always zero
ProbabilityTheory.entropy_pair_eq_add H[X, Y] = H[X] + H[Y] if and only if X, Y are independent
ProbabilityTheory.mutualInfo_comm I[X : Y] = I[Y : X]
ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy I[X : Y] = H[X] - H[X|Y]
ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy' I[X : Y] = H[Y] - H[Y | X]
ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy H[X] - I[X : Y] = H[X | Y]
ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy' H[Y] - I[X : Y] = H[Y | X]
ProbabilityTheory.condMutualInfo_eq_kernel_mutualInfo The conditional mutual information agrees with the information of the conditional kernel
ProbabilityTheory.condMutualInfo_eq_sum' A variant of condMutualInfo_eq_sum when Z has finite codomain
ProbabilityTheory.condMutualInfo_nonneg Conditional information is non-nonegative
ProbabilityTheory.condMutualInfo_comm I[X : Y | Z] = I[Y : X | Z]
ProbabilityTheory.condMutualInfo_eq I[X : Y| Z] = H[X| Z] + H[Y| Z] - H[X, Y| Z]
ProbabilityTheory.condMutualInfo_eq' I[X : Y| Z] = H[X| Z] - H[X|Y, Z]
ProbabilityTheory.condMutualInfo_of_inj_map If f(Z, X) is injective for each fixed Z, then I[f(Z, X) : Y| Z] = I[X : Y| Z]
ProbabilityTheory.condMutualInfo_eq_zero I[X : Y| Z]=0 iff X, Y are conditionally independent over Z
ProbabilityTheory.ent_of_cond_indep If X, Y are conditionally independent over Z, then H[X, Y, Z] = H[X, Z] + H[Y, Z] - H[Z]
ProbabilityTheory.entropy_sub_condEntropy H[X] - H[X|Y] = I[X : Y]
ProbabilityTheory.condEntropy_le_entropy H[X | Y] ≤ H[X]
ProbabilityTheory.entropy_submodular H[X | Y, Z] ≤ H[X | Z]
ProbabilityTheory.condEntropy_comp_ge Data-processing inequality for the conditional entropy: H[Y|f(X)] ≥ H[Y|X] To upgrade this to equality, see condEntropy_of_injective'
ProbabilityTheory.entropy_triple_add_entropy_le The submodularity inequality: H[X, Y, Z] + H[Z] ≤ H[X, Z] + H[Y, Z]
ProbabilityTheory.mutual_comp_le Let X, Ybe random variables
ProbabilityTheory.mutual_comp_comp_le Let X, Y be random variables
ProbabilityTheory.condMutual_comp_comp_le Let X, Y, Z
ProbabilityTheory.entropy_mul_right H[X, X + Y] = H[X, Y]
ProbabilityTheory.entropy_mul_right' H[X, Y + X] = H[X, Y]
ProbabilityTheory.entropy_mul_left H[Y + X, Y] = H[X, Y]
ProbabilityTheory.entropy_mul_left' H[X + Y, Y] = H[X, Y]
ProbabilityTheory.entropy_inv_right H[X, -Y] = H[X, Y]
ProbabilityTheory.entropy_inv_left H[-X, Y] = H[X, Y]
ProbabilityTheory.entropy_div_right H[X, X - Y] = H[X, Y]
ProbabilityTheory.entropy_div_right' H[X, Y - X] = H[X, Y]
ProbabilityTheory.entropy_div_left H[Y - X, Y] = H[X, Y]
ProbabilityTheory.entropy_div_left' H[X - Y, Y] = H[X, Y]
ProbabilityTheory.entropy_inv If X is G-valued, then H[-X]=H[X]
ProbabilityTheory.entropy_div_comm H[X - Y] = H[Y - X]
ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_div max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X - Y | Z]
ProbabilityTheory.condEntropy_mul_left H[Y + X | Y] = H[X | Y]
ProbabilityTheory.condEntropy_mul_right H[X + Y | Y] = H[X | Y]
ProbabilityTheory.condEntropy_div_left H[Y - X | Y] = H[X | Y]
ProbabilityTheory.condEntropy_div_right H[X - Y | Y] = H[X | Y]
ProbabilityTheory.mutualInfo_mul_right I[X : X + Y] = H[X + Y] - H[Y] iff X, Y are independent
ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul H[X] - I[X : Y] ≤ H[X + Y]
ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul' H[Y] - I[X : Y] ≤ H[X + Y]
ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div H[X] - I[X : Y] ≤ H[X - Y]
ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div' H[Y] - I[X : Y] ≤ H[X - Y]
ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_mul max(H[X], H[Y]) - I[X : Y] ≤ H[X + Y]
ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_div max(H[X], H[Y]) - I[X : Y] ≤ H[X - Y]
ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_mul max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X + Y | Z]
ProbabilityTheory.max_entropy_le_entropy_mul If X, Y are independent, then max(H[X], H[Y]) ≤ H[X + Y]
ProbabilityTheory.max_entropy_le_entropy_div If X, Y are independent, then max(H[X], H[Y]) ≤ H[X - Y]
ProbabilityTheory.Kernel.finiteKernelSupport_of_const Constant kernels with finite support, have finite kernel support
ProbabilityTheory.Kernel.finiteSupport_of_compProd' Composing a finitely supported measure with a finitely supported kernel gives a finitely supported kernel
ProbabilityTheory.Kernel.entropy_snd_compProd_deterministic_of_injective entropy_map_of_injective is a special case of this (see def of map)
ProbabilityTheory.Kernel.entropy_map_le Data-processing inequality for the kernel entropy
ProbabilityTheory.Kernel.entropy_snd_sub_mutualInfo_le_entropy_map_of_injective TODO: extract lemma(s) from this:
ProbabilityTheory.Kernel.entropy_submodular_compProd from kernel (T × S × U) V ; Measure (T × S × U) to kernel (T × S) V ; Measure (T × S)
ProbabilityTheory.Kernel.entropy_compProd_triple_add_entropy_le $$ H[X,Y,Z] + H[X] \leq H[Z,X] + H[Y,X].$$
ProbabilityTheory.Kernel.entropy_triple_add_entropy_le' The submodularity inequality: $$ H[X,Y,Z] + H[X] \leq H[X,Z] + H[X,Y].$$
ProbabilityTheory.Kernel.entropy_triple_add_entropy_le The submodularity inequality: $$ H[X,Y,Z] + H[Z] \leq H[X,Z] + H[Y,Z].$$
ProbabilityTheory.Kernel.ent_of_diff_le The improved entropic Ruzsa triangle inequality
ProbabilityTheory.FiniteSupport A measure has finite support if there exists a finite set whose complement has zero measure
ProbabilityTheory.FiniteEntropy TODO: replace FiniteSupport hypotheses ∈ these files with FiniteEntropy hypotheses
ProbabilityTheory.full_measure_of_finiteRange duplicate of FiniteRange.null_of_compl
ProbabilityTheory.integrable_of_finiteSupport Every function is integrable against a finite measure with finite support
ProbabilityTheory.Measure.ext_iff_singleton_finiteSupport This generalizes Measure.ext_iff_singleton ∈ MeasureReal
ProbabilityTheory.measureEntropy_le_card_aux Auxiliary lemma for measureEntropy_le_log_card_of_mem, which removes the probability measure assumption
ProbabilityTheory.entropy_of_uniformOn The entropy of a uniform measure is the log of the cardinality of its support
ProbabilityTheory.measureEntropy_prod An ambitious goal would be to replace FiniteSupport with finite entropy
ProbabilityTheory.measureMutualInfo_nonneg_aux An ambitious goal would be to replace FiniteSupport with finite entropy
continuous_measureEntropy_probabilityMeasure Entropy depends continuously on the measure
rdist
rdist_def Explicit formula for the Ruzsa distance
rdist_eq_rdistm Ruzsa distance of random variables equals Ruzsa distance of the kernels
continuous_rdist_restrict_probabilityMeasure Ruzsa distance depends continuously on the measure
rdist_eq_rdist_id_map Ruzsa distance between random variables equals Ruzsa distance between their distributions
continuous_rdist_restrict_probabilityMeasure₁' Ruzsa distance depends continuously on the second measure
ProbabilityTheory.IdentDistrib.rdist_congr If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y]
ProbabilityTheory.IdentDistrib.rdist_congr_left If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y]
ProbabilityTheory.IdentDistrib.rdist_congr_right If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y]
ProbabilityTheory.IndepFun.rdist_eq If X, Y are independent G-random variables then d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2
rdist_le_avg_ent d[X ; Y] ≤ H[X]/2 + H[Y]/2
rdist_of_inj Applying an injective homomorphism does not affect Ruzsa distance
rdist_zero_eq_half_ent d[X ; 0] = H[X] / 2
rdist_symm d[X ; Y] = d[Y ; X]
continuous_rdist_restrict_probabilityMeasure₁_left Ruzsa distance depends continuously on the first measure
diff_ent_le_rdist |H[X] - H[Y]| ≤ 2 d[X ; Y]
diff_ent_le_rdist' H[X - Y] - H[X] ≤ 2d[X ; Y]
diff_ent_le_rdist'' H[X - Y] - H[Y] ≤ 2d[X ; Y]
rdist_nonneg d[X ; Y] ≥ 0
ent_of_proj_le Documented declaration: ent_of_proj_le
rdist_add_const Adding a constant to a random variable does not change the Rusza distance
rdist_add_const' A variant of rdist_add_const where one adds constants to both variables
ent_of_diff_le The improved entropic Ruzsa triangle inequality
rdist_triangle The entropic Ruzsa triangle inequality
condRuzsaDist_eq_sum' Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ in a fintype
condRuzsaDist_eq_sum Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$
condRuzsaDist_symm $$ d[X|Z; Y|W] = d[Y|W; X|Z]$$
condRuzsaDist'_def Conditional Ruzsa distance equals Ruzsa distance of associated kernels
condRuzsaDist'_eq_sum Explicit formula for conditional Ruzsa distance d[X ; Y | W]
condRuzsaDist'_eq_sum' Alternate formula for conditional Ruzsa distance d[X ; Y | W] when T is a Fintype
condRuzsaDist'_prod_eq_sum' Version of condRuzsaDist'_prod_eq_sum when W has finite codomain
condRuzsaDist'_eq_integral Explicit formula for conditional Ruzsa distance d[X ; Y | W], in integral form
condRuzsaDist_of_const Conditioning by a constant does not affect Ruzsa distance
condRuzsaDist_of_indep If $(X,Z)$ and $(Y,W)$ are independent, then d[X | Z ; Y | W] = H[X'- Y' | Z', W'] - H[X'|Z']/2 - H[Y'|W']/2
condRuzsaDist'_of_indep Formula for conditional Ruzsa distance for independent sets of variables
condRuzsaDist_of_copy The conditional Ruzsa distance is unchanged if the sets of random variables are replaced with copies
kaimanovich_vershik The Kaimanovich-Vershik inequality
kaimanovich_vershik' A version of the Kaimanovich-Vershik inequality with some variables negated
ent_bsg The entropic Balog-Szemerédi-Gowers inequality
condRuzsaDist_le Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group
condRuzsaDist_diff_le Let X, Y, Z be random variables taking values in some abelian group, and with Y, Z independent
ProbabilityTheory.setRuzsaDist The Ruzsa distance between two subsets A, B of a group G is defined to be the Ruzsa distance between their uniform probability distributions
ProbabilityTheory.setRuzsaDist_eq_rdist Relating Ruzsa distance between sets to Ruzsa distance between random variables
ProbabilityTheory.setRuzsaDist_nonneg Ruzsa distance between sets is nonnegative
ProbabilityTheory.setRuzsaDist_symm Ruzsa distance between sets is symmetric
ProbabilityTheory.setRuzsaDist_triangle Ruzsa distance between sets obeys the triangle inequality
ProbabilityTheory.setRuzsaDist_add_const Ruzsa distance between sets is translation invariant
ProbabilityTheory.setRuzsaDist_of_inj Ruzsa distance between sets is preserved by injective homomorphisms
ProbabilityTheory.setRuzsaDist_le Ruzsa distance between sets is controlled by the doubling constant
ProbabilityTheory.sum_meas_smul_cond_fiber' Documented declaration: sum_meas_smul_cond_fiber'
FiniteRange The property of having a finite range
FiniteRange.fintype fintype structure on the range of a finite range map
FiniteRange.toFinset The range of a finite range map, as a finset
finiteRange_of_finset Functions ranging in a Finset have finite range
FiniteRange.mul The sum of functions of finite range, has finite range
FiniteRange.mul' The sum of functions of finite range, has finite range
FiniteRange.div The difference of functions of finite range, has finite range
FiniteRange.div' The sum of functions of finite range, has finite range
FiniteRange.inv The negation of a function of finite range, has finite range
FiniteRange.inv' The sum of functions of finite range, has finite range
FiniteRange.zpow The multiple of a function of finite range by a constant, has finite range
FiniteRange.zpow' The multiple of a function of finite range by a constant, has finite range
FiniteRange.finprod The sum of a finite number of functions with finite range, has finite range
ProbabilityTheory.identDistrib_of_finiteRange If X has identical distribution to X₀, and X₀ has finite range, then X is almost everywhere equivalent to a random variable of finite range
ProbabilityTheory.independent_copies_finiteRange A version of independent_copies that guarantees that the copies have FiniteRange if the original variables do
ProbabilityTheory.independent_copies3_nondep_finiteRange A version of independent_copies3_nondep that guarantees that the copies have FiniteRange if the original variables do
ProbabilityTheory.independent_copies4_nondep_finiteRange A version of independent_copies4_nondep that guarantees that the copies have FiniteRange if the original variables do
ProbabilityTheory.independent_copies'_finiteRange A version of independent_copies' that guarantees that the copies have FiniteRange if the original variables do
ProbabilityTheory.iIndepFun.apply_two_last If (Z₁, Z₂, Z₃, Z₄) are independent, so are (Z₁, Z₂, φ Z₃ Z₄) for any measurable φ
prod The pair of two random variables
ProbabilityTheory.IsUniform The assertion that the law of $X$ is the uniform probability measure on a finite set $H$
ProbabilityTheory.exists_isUniform Uniform distributions exist
ProbabilityTheory.IsUniform.comp The image of a uniform random variable under an injective map is uniform on the image
ProbabilityTheory.exists_isUniform_measureSpace Uniform distributions exist, version giving a measure space
ProbabilityTheory.exists_isUniform_measureSpace' Uniform distributions exist, version with a Finite set rather than a Finset and giving a measure space
ProbabilityTheory.IsUniform.ae_mem A uniform random variable on H almost surely takes values in H
ProbabilityTheory.IsUniform.nonempty Uniform random variables only exist for non-empty sets H
ProbabilityTheory.IsUniform.measure_preimage_of_nmem A "unit test" for the definition of uniform distribution
ProbabilityTheory.IsUniform.measureReal_preimage_of_nmem Another "unit test" for the definition of uniform distribution
ProbabilityTheory.IsUniform.measure_preimage_of_mem A "unit test" for the definition of uniform distribution
ProbabilityTheory.IsUniform.measureReal_preimage_of_mem A "unit test" for the definition of uniform distribution
ProbabilityTheory.IsUniform.measure_preimage $\mathbb{P}(U_H \in H') = \dfrac{|H' \cap H|}{|H|}$
ProbabilityTheory.IsUniform.measureReal_preimage $\mathbb{P}(U_H \in H') = \dfrac{|H' \cap H|}{|H|}$
ProbabilityTheory.IsUniform.of_identDistrib A copy of a uniform random variable is also uniform
ProbabilityTheory.IsUniform.measure_preimage_ne_zero $\mathbb{P}(U_H \in H') \neq 0$ if $H'$ intersects $H$ and the measure is non-zero
ProbabilityTheory.IsUniform.restrict If $X$ is uniform w.r.t
ProbabilityTheory.isUniform_iff_map_eq_uniformOn A random variable is uniform iff its distribution is
hahn_banach Let $H_0$ be a subgroup of $G$
goursat Let $H$ be a subgroup of $G \times G'$
homomorphism_pfr Homomorphism PFR after goursat
symmGroup The symmetry group Sym of $X$: the set of all $h ∈ G$ such that $X + h$ has an identical distribution to $X$
sub_mem_symmGroup If $d[X ;X]=0$, and $x,y \in G$ are such that $P[X=x], P[X=y]>0$, then $x-y \in \mathrm{Sym}[X]$
isUniform_sub_const_of_rdist_eq_zero If d[X # X] = 0, then X - x₀ is the uniform distribution on the subgroup of G stabilizing the distribution of X, for any x₀ of positive probability
exists_isUniform_of_rdist_self_eq_zero If $d[X ;X]=0$, then there exists a subgroup $H \leq G$ such that $d[X ;U_H] = 0$
exists_isUniform_of_rdist_eq_zero If $d[X_1;X_2]=0$, then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$
gen_ineq_00 Let Z₁, Z₂, Z₃, Z₄ be independent G-valued random variables, and let Y be another G-valued random variable
gen_ineq_01 Other version of gen_ineq_00, in which we switch to the complement in the second term
gen_ineq_10 Other version of gen_ineq_00, in which we switch to the complement in the first term
construct_good_prelim' Documented declaration: construct_good_prelim'
construct_good_improved' In fact $k$ is at most $$ \delta + \frac{\eta}{6} \sum_{i=1}^2 \sum_{1 \leq j,l \leq 3; j \neq l} (d[X^0_i;T_j|T_l] - d[X^0_i; X_i]).$$
construct_good_improved'' Rephrase construct_good_improved' with an explicit probability measure, as we will apply it to (varying) conditional measures
averaged_construct_good Documented declaration: averaged_construct_good
tau_strictly_decreases_aux' Suppose $0 < \eta < 1/8$
tau_minimizer_exists_rdist_eq_zero For p.η ≤ 1/8, there exist τ-minimizers X₁, X₂ at zero Rusza distance
entropic_PFR_conjecture_improv Entropic PFR, improved constants (10 and 11/2) after tau_minimizer_exists_rdist_eq_zero, rdist_triangle, exists_isUniform_of_rdist_eq_zero
PFR_conjecture_improv_aux Documented declaration: PFR_conjecture_improv_aux
PFR_conjecture_improv PFR with exponent 11 after PFR_conjecture_improv_aux, entropic_PFR_conjecture_improv
KLDiv If X, Y are two G-valued random variables, the Kullback--Leibler divergence is defined as KL(X ‖ Y) := ∑ₓ 𝐏(X = x) log (𝐏(X = x) / 𝐏(Y = x))
ProbabilityTheory.IdentDistrib.KLDiv_eq If X' is a copy of X, and Y' is a copy of Y, then KL(X' ‖ Y') = KL(X ‖ Y)
KLDiv_nonneg KL(X ‖ Y) ≥ 0
KLDiv_eq_zero_iff_identDistrib KL(X ‖ Y) = 0 if and only if Y is a copy of X
KLDiv_of_convex Documented declaration: KLDiv_of_convex
KLDiv_of_comp_inj If $f:G \to H$ is an injection, then $D_{KL}(f(X)\Vert f(Y)) = D_{KL}(X\Vert Y)$
ProbabilityTheory.IndepFun.map_add_eq_sum The distribution of X + Z is the convolution of the distributions of Z and X when these random variables are independent
ProbabilityTheory.IndepFun.map_add_singleton_eq_sum The distribution of X + Z is the convolution of the distributions of Z and X when these random variables are independent
KLDiv_add_le_KLDiv_of_indep If $X, Y, Z$ are independent $G$-valued random variables, then $$D_{KL}(X+Z\Vert Y+Z) \leq D_{KL}(X\Vert Y).$$
condKLDiv If $X,Y,Z$ are random variables, with $X,Z$ defined on the same sample space, we define $$ D_{KL}(X|Z \Vert Y) := \sum_z \mathbf{P}(Z=z) D_{KL}( (X|Z=z) \Vert Y).$$
condKLDiv_eq Documented declaration: condKLDiv_eq
condKLDiv_nonneg KL(X|Z ‖ Y) ≥ 0
ProbabilityTheory.IsUniform.measureReal_preimage_sub_zero Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V with probability #(A ∩ B) / #A ⬝ #B
ProbabilityTheory.IsUniform.measureReal_preimage_sub Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V + x with probability # (A ∩ (B + x)) / #A ⬝ #B
PFR_conjecture_pos_aux Record positivity results that are useful in the proof of PFR
PFR_conjecture_pos_aux'
rdist_le_of_isUniform_of_card_sub_le Small doubling gives small self Ruzsa distance after rdist
rdist_le_of_isUniform_of_doubling In characteristic 2, a uniform distribution on a set with doubling constant K has self Rusza distance at most log K
Fin.sum_univ_castSucc' TODO: Rename Fin.sum_univ_castSucc to Fin.sum_univ_eq_castSucc
Real.sum_mul_log_div_leq Documented declaration: sum_mul_log_div_leq
Real.sum_mul_log_div_eq_iff_aux If equality holds in the previous bound, then $a_s=r\cdot b_s$ for every $s\in S$, for some constant $r\in \mathbb{R}$
Real.sum_mul_log_div_eq_iff If equality holds in the previous bound, then $a_s=r\cdot b_s$ for every $s\in S$, for some constant $r\in \mathbb{R}$
Submodule.exists_equiv_fst_sndModFst Given a submodule $E$ of $B \times F$, there is an equivalence $f : E \to B' \times F'$ given by the projections $E \to B$ and $E \to F$ "modulo" some $φ : B \to F$
Submodule.finrank The dimension of a submodule
MeasureTheory.lintegral_eq_sum TODO: Change RHS of lintegral_fintype
MeasureTheory.setLIntegral_eq_sum TODO: Change RHS of lintegral_finset
continuous_finiteMeasure_apply_of_isClopen The measure of any connected component depends continuously on the FiniteMeasure
continuous_probabilityMeasure_apply_of_isClopen The probability of any connected component depends continuously on the ProbabilityMeasure
ProbabilityMeasure.tendsto_iff_forall_apply_tendsto Probability measures on a finite space tend to a limit if and only if the probability masses of all points tend to the corresponding limits
ProbabilityMeasure.tendsto_iff_forall_apply_tendsto_ennreal Probability measures on a finite space tend to a limit if and only if the probability masses of all points tend to the corresponding limits
MeasureTheory.Measure.map_prod_comap_swap The law of $(X, Z)$ is the image of the law of $(Z,X)$
ProbabilityTheory.cond_real_apply The axiomatic definition of conditional probability derived from a measure-theoretic one
ProbabilityTheory.cond_isProbabilityMeasure_of_real The conditional probability measure of any finite measure on any set of positive measure is a probability measure
ProbabilityTheory.IdentDistrib.fst_id The first projection in a product space with measure μ.prod ν is distributed like μ
ProbabilityTheory.IdentDistrib.snd_id The second projection in a product space with measure μ.prod ν is distributed like ν
ProbabilityTheory.identDistrib_comp_left A function is identically distributed to itself composed with a measurable embedding of conull range
ProbabilityTheory.identDistrib_comp_right A function is identically distributed to itself composed with a measurable embedding of conull range
ProbabilityTheory.IdentDistrib.comp_left Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions
ProbabilityTheory.IdentDistrib.comp_right Composing identically distributed functions with a measurable embedding of conull range gives identically distributed functions
ProbabilityTheory.AEMeasurable.piMk Move to a different section?
ProbabilityTheory.identDistrib_map A random variable is identically distributed to its pullbacks
ProbabilityTheory.identDistrib_of_sum To show identical distribution of two random variables on a mixture of probability measures, it suffices to do so on each non-trivial component
ProbabilityTheory.identDistrib_comp_fst A random variable is identically distributed to its lift to a product space (in the first factor)
ProbabilityTheory.identDistrib_comp_snd A random variable is identically distributed to its lift to a product space (in the second factor)
ProbabilityTheory.independent_copies For X, Y random variables, one can find independent copies X', Y' of X, Y
ProbabilityTheory.independent_copies_two For X, Y random variables, one can find independent copies X', Y' of X, Y
ProbabilityTheory.independent_copies' Let Xᵢ : Ωᵢ → Sᵢ be random variables for i = 1,...,k
ProbabilityTheory.independent_copies3_nondep A version with exactly 3 random variables that have the same codomain
ProbabilityTheory.independent_copies4_nondep A version with exactly 4 random variables that have the same codomain
ProbabilityTheory.iIndepFun.finsets Documented declaration: finsets
ProbabilityTheory.iIndepFun.finsets_comp Documented declaration: finsets_comp
ProbabilityTheory.iIndepFun.finsets_comp' A variant of iIndepFun.finsets_comp where we conclude the independence of just two functions rather than an entire family
ProbabilityTheory.indepFun_const Random variables are always independent of constants
ProbabilityTheory.IndepFun.comp_right Composing independent functions with a measurable embedding of conull range gives independent functions
ProbabilityTheory.iIndepFun_iff' Same as iIndepFun_iff except that the function f' returns measurable sets even on junk values
ProbabilityTheory.iIndepFun.pi If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples i ↦ (f i j)ⱼ is independent
ProbabilityTheory.iIndepFun.pi' If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples i ↦ (f i j)ⱼ is independent
ProbabilityTheory.iIndepFun.ae_eq TODO: a kernel version of this theorem
ProbabilityTheory.Kernel.iIndepFun.finsets Documented declaration: finsets
ProbabilityTheory.Kernel.iIndepFun.finsets_comp Documented declaration: finsets_comp
ProbabilityTheory.Kernel.FiniteKernelSupport.reverse Reversing preserves finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport The analogue of FiniteSupport for probability kernels
ProbabilityTheory.Kernel.AEFiniteKernelSupport A kernel κ has almost everywhere finite support wrt a measure μ if, for almost every point t, then κ t has finite support
ProbabilityTheory.Kernel.local_support_of_finiteKernelSupport Finite kernel support locally implies uniform finite kernel support
ProbabilityTheory.Kernel.finiteKernelSupport_of_finite_range Finite range implies finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.deterministic Deterministic kernels have finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.map maps preserve finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.comap comaps preserve finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.fst Projecting a kernel to first coordinate preserves finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.snd Projecting a kernel to second coordinate preserves finite kernel support
ProbabilityTheory.Kernel.aefiniteKernelSupport_of_cond Conditioning a kernel preserves finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.swapRight Swapping a kernel right preserves finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.prod Products preserve finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.compProd Composition-product preserves finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.prodMkRight prodMkRight preserves finite kernel support
ProbabilityTheory.Kernel.FiniteKernelSupport.prodMkLeft prodMkLeft preserves finite kernel support
rdist_of_neg_le If X, Y are G-valued, then d[X;-Y] ≤ 3 d[X;Y]
kvm_ineq_I If n ≥ 0 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then H[Y i₀ + ∑ i ∈ s, Y i; μ] - H[Y i₀; μ] ≤ ∑ i ∈ s, (H[Y i₀ + Y i; μ] - H[Y i₀; μ])
kvm_ineq_II If n ≥ 1 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ 2 * ∑ i ∈ s, d[Y i₀; μ # Y i; μ]
kvm_ineq_III_aux' strengthen the above lemma by not requiring X to be independent of Y, Z
kvm_ineq_III If n ≥ 1 and X, Y₁, ..., Yₙ$ are jointly independent G-valued random variables, then d[Y i₀, ∑ i, Y i] ≤ d[Y i₀, Y i₁] + 2⁻¹ * (H[∑ i, Y i] - H[Y i₁])
ent_of_sum_le_ent_of_sum Let X₁, ..., Xₘ and Y₁, ..., Yₗ be tuples of jointly independent random variables (so the X's and Y's are also independent of each other), and let `f : {1,..., l} → {1,
ent_sub_zsmul_le Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer
ent_sub_nsmul_le Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer
ent_of_sub_smul' Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer
ent_sub_zsmul_sub_ent_le Let X,Y be independent G-valued random variables, and let a be an integer
ent_sub_nsmul_sub_ent_le Let X,Y be independent G-valued random variables, and let a be a natural number
ent_add_nsmul_sub_ent_le Let X,Y be independent G-valued random variables, and let a be a natural number
multiDist Let X_[m] = (X₁, ..., Xₘ) be a non-empty finite tuple of G-valued random variables X_i
multiDist_copy If X_i has the same distribution as Y_i for each i, then D[X_[m]] = D[Y_[m]]
MeasureTheory.Measure.map_of_pi Move to Mathlib?
multiDist_indep If X_i are independent, then D[X_{[m]}] = H[∑_{i=1}^m X_i] - \frac{1}{m} \sum_{i=1}^m H[X_i]
multiDist_nonneg We have D[X_[m]] ≥ 0
multiDist_of_perm If φ : {1, ..., m} → {1, ...,m} is a bijection, then D[X_[m]] = D[(X_φ(1), ..., X_φ(m))]
offDiag_sum The sum of f away from the diagonal
multidist_ruzsa_I_indep To prove multidist_ruzsa_I, we first establish a special case when the random variables are defined on the same space and are jointly independent
multidist_ruzsa_I Let m ≥ 1, and let X_[m] be a tuple of G-valued random variables
multidist_ruzsa_II Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables
multidist_ruzsa_III' A version of multidist_ruzsa_III assuming independence
multidist_ruzsa_III Let I be an indexing set of size m ≥ 2, and let X_[m] be a tuple of G-valued random variables
multidist_ruzsa_IV Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables
multidist_eq_zero If D[X_[m]]=0, then for each i ∈ I there is a finite subgroup H_i ≤ G such that d[X_i; U_{H_i}] = 0
condMultiDist_of_inj Conditional multidistance is unchanged if we apply an injection to the conditioned variables
condMultiDist_of_const Conditional multidistance against a constant is just multidistance
condMultiDist_nonneg Conditional multidistance is nonnegative
Finset.prod_mul A technical lemma: can push a constant into a product at a specific term
ident_of_cond_of_indep A technical lemma: two different ways of conditioning independent variables gives identical distributions
prob_nonzero_of_prod_prob_nonzero A technical lemma: if a product of probabilities is nonzero, then each probability is individually non-zero
condMultiDist_eq If (X_i, Y_i), 1 ≤ i ≤ m are independent, then D[X_[m] | Y_[m]] = H[∑ i, X_i | (Y_1, ..., Y_m)] - 1/m * ∑ i, H[X_i | Y_i]
condMultiDist_eq' If (X_i, Y_i), 1 ≤ i ≤ m are independent, then D[X_[m] | Y_[m]] = ∑_{(y_i)_{1 ≤ i ≤ m}} P(Y_i=y_i ∀ i) D[(X_i | Y_i=y_i ∀ i)_{i=1}^m]
multiDist_chainRule Let π : G → H be a homomorphism of abelian groups and let X_[m] be a tuple of jointly independent G-valued random variables
cond_multiDist_chainRule Let π : G → H be a homomorphism of abelian groups
iter_multiDist_chainRule Let m be a positive integer
iter_multiDist_chainRule' Under the preceding hypotheses, D[X_[m]] ≥ ∑ d, D[π_d(X_[m])| π_(d-1})(X_[m])] + I[∑ i, X_i : π_1(X_[m]) | π_1(∑ i, X_i)]
cor_multiDist_chainRule Let G be an abelian group and let m ≥ 2
MeasurableFinGroup We will frequently be working with finite additive groups with the discrete sigma-algebra
multiRefPackage A structure that packages all the fixed information in the main argument
multiTau If $(X_i)_{1 \leq i \leq m}$ is a tuple, we define its $\tau$-functional $$ \tau[ (X_i)_{1 \leq i \leq m}] := D[(X_i)_{1 \leq i \leq m}] + \eta \sum_{i=1}^m d[X_i; X^0].$$
multiTauMinimizes A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional among all tuples of $G$-valued random variables
multiTau_continuous If $G$ is finite, then $\tau$ is continuous
multiTau_min_exists_measure If $G$ is finite, then a $\tau$-minimizer exists
multiTau_min_exists If $G$ is finite, then a $\tau$-minimizer exists
multiTau_min_sum_le If $(X_i)_{1 \leq i \leq m}$ is a $\tau$-minimizer, then $\sum_{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]$
sub_multiDistance_le Documented declaration: sub_multiDistance_le
sub_condMultiDistance_le Documented declaration: sub_condMultiDistance_le
sub_condMultiDistance_le' Documented declaration: sub_condMultiDistance_le'
rhoMinusSet The set of possible values of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and $T$ ranges over $G$-valued random variables independent of $U_A$
rhoMinus Documented declaration: rhoMinus
rhoMinus_nonneg We have $\rho^-(X) \geq 0$
rhoPlus For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$
rhoMinus_of_subgroup If $H$ is a finite subgroup of $G$, then $\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|$
rhoPlus_of_subgroup If $H$ is a finite subgroup of $G$, then $\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|$
rho We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$
rho_of_uniform We have $\rho(U_A) = 0$
rho_of_subgroup If $H$ is a finite subgroup of $G$, and $\rho(U_H) \leq r$, then there exists $t$ such that $|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}$, and $|H|/|A| \in [e^{-2r}, e^{2r}]$
rho_of_submodule If $H$ is a finite subgroup of $G$, and $\rho(U_H) \leq r$, then there exists $t$ such that $|A \cap (H+t)| \geq e^{-r} \sqrt{|A||H|}$, and $|H|/|A| \in [e^{-2r}, e^{2r}]$
rho_continuous \rho(X)$ depends continuously on the distribution of $X$
rhoMinus_of_sum If $X,Y$ are independent, one has $$ \rho^-(X+Y) \leq \rho^-(X)$$
rhoPlus_of_sum If $X,Y$ are independent, one has $$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$
rho_of_sum If $X,Y$ are independent, one has $$\rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X]).$$
condRho We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$
condRhoMinus Average of rhoMinus along the fibers
condRhoPlus Average of rhoPlus along the fibers
condRho_of_translate For any $s\in G$, $\rho(X+s|Y)=\rho(X|Y)$
condRho_of_injective If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$
condRhoMinus_le $$ \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]$$
condRhoPlus_le $$ \rho^+(X|Z) \leq \rho^+(X)$$
condRho_le $$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z])$$
condRho_prod_le $$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z])$$, conditional version
rho_of_sum_le If $X,Y$ are independent, then $$ \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$
condRho_of_sum_le If $X,Y$ are independent, then $$ \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$
phi Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$
phiMinimizes Documented declaration: phiMinimizes
phi_min_exists There exists a $\phi$-minimizer
I_one_le $I_1\le 2\eta d[X_1;X_2]$
rdist_add_rdist_eq $d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$
I_two_le $I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1)$
dist_le_of_sum_zero Documented declaration: dist_le_of_sum_zero
dist_le_of_sum_zero_cond Documented declaration: dist_le_of_sum_zero_cond
dist_le_of_sum_zero' Documented declaration: dist_le_of_sum_zero'
dist_le_of_sum_zero_cond' Documented declaration: dist_le_of_sum_zero_cond'
condRho_sum_le For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $S:=Y_1+Y_2+Y_3+Y_4$, $T_1:=Y_1+Y_2$, $T_2:=Y_1+Y_3$
condRho_sum_le' For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $T_1:=Y_1+Y_2, T_2:=Y_1+Y_3, T_3:=Y_2+Y_3$ and $S:=Y_1+Y_2+Y_3+Y_4$
dist_of_min_eq_zero' If $X_1, X_2$ is a $\phi$-minimizer, then $d[X_1;X_2] = 0$
phiMinimizer_exists_rdist_eq_zero For η ≤ 1/8, there exist phi-minimizers X₁, X₂ at zero Rusza distance
rho_PFR_conjecture For any random variables $Y_1,Y_2$, there exist a subgroup $H$ such that $$ 2\rho(U_H) \leq \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2].$$
better_PFR_conjecture_aux0 If $|A+A| \leq K|A|$, then there exists a subgroup $H$ and $t\in G$ such that $|A \cap (H+t)| \geq K^{-4} \sqrt{|A||V|}$, and $|H|/|A|\in[K^{-8},K^8]$
better_PFR_conjecture_aux Documented declaration: better_PFR_conjecture_aux
better_PFR_conjecture Documented declaration: better_PFR_conjecture
rdist_of_sums_ge' $$ d[X_1+\tilde X_1; X_2+\tilde X_2] \geq k - \frac{\eta}{2} ( d[X_1; X_1] + d[X_2;X_2] ).$$
second_estimate $$ I_2 \leq 2 \eta k + \frac{2 \eta (2 \eta k - I_1)}{1 - \eta}.$$
Mathlib.Tactic.RPowRing.Context The read-only state of the RPowRing monad
Mathlib.Tactic.RPowRing.Config Configuration for ring_nf
Mathlib.Tactic.RPowRing.M Documented declaration: M
Mathlib.Tactic.RPowRing.ExBase A monomial, which is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient
Mathlib.Tactic.RPowRing.ExProd A monomial, which is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient
Mathlib.Tactic.RPowRing.ExBase.toProd Embed an exponent (an ExBase, ExProd pair) as an ExProd by multiplying by 1
Mathlib.Tactic.RPowRing.evalAtom Evaluates an atom, an expression where ring can find no additional structure
Mathlib.Tactic.RPowRing.evalMul Multiplies two monomials va, vb together to get a normalized result monomial
Mathlib.Tactic.RPowRing.M.run Runs a tactic in the RingNF.M monad, given initial data: * s: a reference to the mutable state of ring, for persisting across calls
Mathlib.Tactic.RPowRing.rpowRingTarget Use rpow_ring to rewrite the main goal
Mathlib.Tactic.RPowRing.rpowRingLocalDecl Use rpow_ring to rewrite hypothesis h
Mathlib.Tactic.RPowRing.elabRPowRingConv Elaborator for the rpow_ring tactic
refPackage A structure that packages all the fixed information in the main argument
tau Documented declaration: tau
ProbabilityTheory.IdentDistrib.tau_eq If $X'_1, X'_2$ are copies of $X_1,X_2$, then $\tau[X'_1;X'_2] = \tau[X_1;X_2]$
TauMinimizes Property recording the fact that two random variables minimize the tau functional
ProbabilityTheory.IdentDistrib.tauMinimizes If $X'_1, X'_2$ are copies of $X_1,X_2$, then $X_1, X_2$ minimize $\tau$ iff $X_1', X_2'$ do
tau_min_exists_measure A pair of measures minimizing $\tau$ exists
tau_minimizer_exists A pair of random variables minimizing $τ$ exists
entropic_PFR_conjecture Entropic PFR (constants 11 and 6) after tau_minimizer_exists, tau_strictly_decreases, rdist_triangle, exists_isUniform_of_rdist_eq_zero
PFR_conjecture_aux Covering lemma behind PFR after entropic_PFR_conjecture, rdist_le_of_isUniform_of_card_sub_le
PFR_conjecture Polynomial Freiman-Ruzsa conjecture (characteristic 2) after PFR_conjecture_aux, PFR_conjecture_pos_aux'
distance_ge_of_min Documented declaration: distance_ge_of_min
distance_ge_of_min' Version of distance_ge_of_min with the measures made explicit
condRuzsaDistance_ge_of_min Documented declaration: condRuzsaDistance_ge_of_min
sum_of_z_eq_zero Z_1+Z_2+Z_3= 0
mutual_information_le_t_12 We have I[Z_1 : Z_2 | W], I[Z_2 : Z_3 | W], I[Z_1 : Z_3 | W] ≤ 4m^2 η k
entropy_of_W_le We have $\bbH[W] \leq (2m-1)k + \frac1m \sum_{i=1}^m \bbH[X_i]$
entropy_of_Z_two_le We have $\bbH[Z_2] \leq (8m^2-16m+1) k + \frac{1}{m} \sum_{i=1}^m \bbH[X_i]$
mutual_of_W_Z_two_le We have $\bbI[W : Z_2] \leq 2(m-1) k$
sum_of_conditional_distance_le We have $\sum_{i=1}^m d[X_i;Z_2|W] \leq 4(m^3-m^2) k$
dist_of_U_add_le Documented declaration: dist_of_U_add_le
k_eq_zero We have $k = 0$
dist_of_X_U_H_le Suppose that $G$ is a finite abelian group of torsion $m$
rdist_le_of_isUniform_of_card_add_le' A uniform distribution on a set with doubling constant K has self Rusza distance at most log K
torsion_PFR_conjecture_aux Suppose that $G$ is a finite abelian group of torsion $m$
torsion_exists_subgroup_subset_card_le Every subgroup H of a finite m-torsion abelian group G contains a subgroup H' of order between k and mk, if 0 < k < |H|
torsion_PFR Suppose that $G$ is an abelian group of torsion $m$ (not necessarily finite)
IsShift A set A is a shift of a set B if it can be written as x + B
NotInCoset The property of two sets A, B of a group G not being contained in cosets of the same proper subgroup
wlog_notInCoset Without loss of generality, one can move (up to translation and embedding) any pair A, B of non-empty sets into a subgroup where they are not in a coset
torsion_free_doubling If G is torsion-free and X, Y are G-valued random variables then d[X; 2Y] ≤ 5d[X; Y]
torsion_dist_shrinking If G is a torsion-free group and X, Y are G-valued random variables and φ : G → 𝔽₂^d is a homomorphism then H[φ ∘ X; μ] ≤ 10 * d[X; μ # Y; μ']
app_ent_PFR' Let $G=\mathbb{F}_2^n$ and X, Y be G-valued random variables such that \[\mathbb{H}(X)+\mathbb{H}(Y)> (20/\alpha) d[X;Y],\] for some $\alpha > 0$
PFR_projection' Documented declaration: PFR_projection'
PFR_projection Documented declaration: PFR_projection
single_fibres Let $\phi : G\to H$ be a homomorphism and $A,B\subseteq G$ be finite subsets
third_iso A version of the third isomorphism theorem: if G₂ ≤ G and H' is a subgroup of G⧸G₂, then there is a canonical isomorphism between H⧸H' and G⧸N, where N is the preimage of H' in G
weak_PFR_asymm_prelim Documented declaration: weak_PFR_asymm_prelim
WeakPFRAsymmConclusion Separating out the conclusion of weak_PFR_asymm for convenience of induction arguments
not_in_coset The property of two sets A,B of a group G not being contained in cosets of the same proper subgroup
dimension_of_shift In fact one has equality here, but this is trickier to prove and not needed for the argument
weak_PFR_asymm Documented declaration: weak_PFR_asymm
weak_PFR Documented declaration: weak_PFR
weak_PFR_int Weak PFR over the integers after weak_PFR, weak_PFR_asymm, ProbabilityTheory.setRuzsaDist_le
weak_PFR_int_sumset Weak PFR from a sumset hypothesis after weak_PFR_int
Marton.pfr_conjecture@PFRPalomar/Challenge.lean Marton's conjecture in characteristic 2, [GGMT], Theorem 1.2
Marton.pfr_conjecture_nine@PFRPalomar/Challenge.lean Marton's conjecture in characteristic 2 with exponent 9, [L], main theorem
Marton.torsion_pfr_conjecture@PFRPalomar/Challenge.lean Marton's conjecture in abelian groups of bounded torsion, [GGMT2], Theorem 1.1
Marton.weak_pfr_int@PFRPalomar/Challenge.lean Weak Marton's conjecture over the integers, [GGMT], Theorem 1.3
Marton.homomorphism_pfr@PFRPalomar/Challenge.lean The homomorphism form of Marton's conjecture, [GGMT], Corollary 1.4
Marton.approx_hom_pfr@PFRPalomar/Challenge.lean The approximate homomorphism form of Marton's conjecture, [GGMT], Corollary 1.5