`PFR/RhoFunctional.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

82 declarations, 0 contain sorry, 0 declared as axioms

The rho functional

Definition of the rho functional and basic facts

Imports (3)

Imported by 4 files

def 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$ line 31 source
Source documentation
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$. We also require an absolute continuity condition so that the KL divergence makes sense in ℝ.
To avoid universe issues, we express this using measures on G, but the equivalence with the above point of view follows from rhoMinus_le below.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Finset, MeasureTheory.Measure, Set, Real
Proof uses: Set.ofPred, Exists, And, MeasureTheory.IsProbabilityMeasure, Eq, ENNReal, MeasureTheory.Measure.map, Prod, HAdd.hAdd, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.uniformOn, Singleton.singleton, OfNat.ofNat, KLDiv
14 instances, coercions and auxiliary constants left out.
```
noncomputable def rhoMinusSet
    (X : Ω → G) (A : Finset G) (μ : Measure Ω) : Set ℝ :=
…
```
lemma map_prod_uniformOn_ne_zero line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, Finset, Finset.Nonempty, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, MeasureTheory.Measure.map, Prod, HAdd.hAdd, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.uniformOn
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Membership.mem, Exists, False, ProbabilityTheory.isProbabilityMeasure_uniformOn, Finset.finite_toSet, ProbabilityTheory.IndepFun, ProbabilityTheory.indepFun_fst_snd, of_eq_true, Eq.trans, Inv.inv, Finset.card, True, congrFun', congrArg, HDiv.hDiv and 34 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma nonempty_rhoMinusSet line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, Finset.Nonempty, Set.Nonempty, Real, rhoMinusSet
Proof uses: Eq, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, Exists.intro, Membership.mem, Set, And, ENNReal, MeasureTheory.Measure.map, Prod, HAdd.hAdd, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.uniformOn, Singleton.singleton, KLDiv, And.intro and 46 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma nonneg_of_mem_rhoMinusSet line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, Real, Membership.mem, Set, rhoMinusSet, LE.le, OfNat.ofNat
Proof uses: And, MeasureTheory.IsProbabilityMeasure, Eq, ENNReal, MeasureTheory.Measure.map, Prod, HAdd.hAdd, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.uniformOn, Singleton.singleton, KLDiv, KLDiv_nonneg, Eq.symm
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma bddBelow_rhoMinusSet line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, BddBelow, Real, rhoMinusSet
Proof uses: Exists.intro, Membership.mem, Set, lowerBounds, OfNat.ofNat, nonneg_of_mem_rhoMinusSet
5 instances, coercions and auxiliary constants left out.
lemma rhoMinusSet_eq_of_identDistrib line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, ProbabilityTheory.IdentDistrib, Eq, Set, Real, rhoMinusSet
Proof uses: KLDiv, Prod, HAdd.hAdd, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.uniformOn, ProbabilityTheory.IdentDistrib.KLDiv_eq, ProbabilityTheory.IdentDistrib.refl, AEMeasurable.add, AEMeasurable.fst, aemeasurable_id, AEMeasurable.snd, of_eq_true, Set.ofPred, Exists, And, MeasureTheory.IsProbabilityMeasure, ENNReal, MeasureTheory.Measure.map and 13 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def rhoMinus Documented declaration: rhoMinus line 87 source
Source documentation
For any $G$-valued random variable $X$, we define $\rho^-(X)$ to be the infimum 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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Finset, MeasureTheory.Measure, Real
Proof uses: InfSet.sInf, rhoMinusSet
1 instances, coercions and auxiliary constants left out.
```
noncomputable def rhoMinus (X : Ω → G) (A : Finset G) (μ : Measure Ω) : ℝ :=
…
```
lemma rhoMinus_eq_of_identDistrib line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, ProbabilityTheory.IdentDistrib, Eq, Real, rhoMinus
Proof uses: of_eq_true, InfSet.sInf, rhoMinusSet, Eq.trans, True, congrFun', congrArg, Set, rhoMinusSet_eq_of_identDistrib, eq_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma rhoMinus_le_def line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, MeasureTheory.IsProbabilityMeasure, Eq, ENNReal, Set, MeasureTheory.Measure.map, Prod, HAdd.hAdd, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.uniformOn, Singleton.singleton, OfNat.ofNat and 4 more
Proof uses: csInf_le, rhoMinusSet, bddBelow_rhoMinusSet, Exists.intro, And, And.intro, inferInstance, rfl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma rhoMinus_le line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, Finset.Nonempty, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IsUniform, Measurable, ProbabilityTheory.IndepFun, Eq, ENNReal, Set, MeasureTheory.Measure.map, HAdd.hAdd, Singleton.singleton, OfNat.ofNat, LE.le and 3 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, ProbabilityTheory.uniformOn, ProbabilityTheory.isProbabilityMeasure_uniformOn, Finset.finite_toSet, ProbabilityTheory.IsUniform.map_eq_uniformOn, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.ext, MeasurableSet, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, Neg.neg, id and 41 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma rhoMinus_nonneg We have $\rho^-(X) \geq 0$ line 130 source
Source documentation
We have $\rho^-(X) \geq 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Finset, LE.le, Real, OfNat.ofNat, rhoMinus
Proof uses: Real.sInf_nonneg, rhoMinusSet, nonneg_of_mem_rhoMinusSet
3 instances, coercions and auxiliary constants left out.
```
lemma rhoMinus_nonneg [IsZeroOrProbabilityMeasure μ]
    {X : Ω → G} {A : Finset G} : 0 ≤ ρ⁻[X ; μ # A] :=
…
```
lemma rhoMinus_zero_measure line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Eq, OfNat.ofNat, Finset, Real, rhoMinus
Proof uses: Exists, MeasureTheory.IsProbabilityMeasure, Exists.intro, ProbabilityTheory.uniformOn, Set.univ, ProbabilityTheory.isProbabilityMeasure_uniformOn, Set.finite_univ, Set.univ_nonempty, of_eq_true, Eq.trans, True, congrFun', congrArg, InfSet.sInf, rhoMinusSet, Singleton.singleton, Set, And, ENNReal, MeasureTheory.Measure.map and 30 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma rhoMinus_continuous_aux1 line 140 source
lemma rhoMinus_continuous_aux2 line 194 source
lemma rhoMinus_continuous_aux3 line 211 source
lemma rhoMinus_continuous line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, Finset, TopologicalSpace, DiscreteTopology, Finset.Nonempty, Continuous, MeasureTheory.ProbabilityMeasure, Real, rhoMinus, id
Proof uses: Iff.mpr, ContinuousAt, continuous_iff_continuousAt, Filter.Tendsto, nhds, And, LT.lt, Filter.Eventually, GT.gt, tendsto_order, And.intro, OfNat.ofNat, HSub.hSub, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq and 49 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def rhoPlus For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$ line 395 source
Source documentation
For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Finset, MeasureTheory.Measure, Real
Proof uses: HSub.hSub, HAdd.hAdd, rhoMinus, ProbabilityTheory.entropy, Real.log, Nat.card, Subtype, Membership.mem
8 instances, coercions and auxiliary constants left out.
```
noncomputable def rhoPlus (X : Ω → G) (A : Finset G) (μ : Measure Ω) : ℝ :=
…
```
lemma rhoPlus_continuous line 402 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, Finset, TopologicalSpace, DiscreteTopology, Finset.Nonempty, Continuous, MeasureTheory.ProbabilityMeasure, Real, rhoPlus, id
Proof uses: Continuous.add, HAdd.hAdd, rhoMinus, ProbabilityTheory.entropy, Neg.neg, Real.log, Nat.card, Subtype, Membership.mem, rhoMinus_continuous, continuous_entropy_restrict_probabilityMeasure, continuous_const
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma rhoPlus_eq_of_identDistrib line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, ProbabilityTheory.IdentDistrib, Eq, Real, rhoPlus
Proof uses: of_eq_true, Eq.trans, HSub.hSub, HAdd.hAdd, rhoMinus, ProbabilityTheory.entropy, Real.log, Finset.card, True, congr, congrArg, Nat.card, Subtype, Membership.mem, rhoMinus_eq_of_identDistrib, ProbabilityTheory.IdentDistrib.entropy_congr, Nat, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe and 1 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma bddAbove_card_inter_add line 415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, Set, BddAbove, Nat, Set.ofPred, Exists, Eq, Nat.card, Inter.inter, HVAdd.hVAdd
Proof uses: Exists.intro, Membership.mem, upperBounds, LE.le, Nat.card_mono, Set.toFinite, Set.inter_subset_left
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma exists_mem_card_inter_add line 423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, AddSubgroup, Set, Set.Nonempty, Exists, Nat, And, GT.gt, OfNat.ofNat, Membership.mem, Set.ofPred, Eq, Nat.card, Inter.inter, HVAdd.hVAdd
Proof uses: Nonempty, Set.Nonempty.to_subtype, Exists.intro, And.intro, Iff.mpr, Set.mem_vadd_set, ZeroMemClass.zero_mem, of_eq_true, Eq.trans, True, congrFun', congrArg, add_zero, eq_self, Nat.card_pos
48 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma exists_card_inter_add_eq_sSup line 434 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, AddSubgroup, Set, Set.Nonempty, Exists, And, Eq, Nat, Nat.card, Inter.inter, HVAdd.hVAdd, SupSet.sSup, Set.ofPred, LT.lt, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, rfl, GT.gt, Membership.mem, exists_mem_card_inter_add, Nat.sSup_mem, Exists.intro, bddAbove_card_inter_add, lt_of_lt_of_le, LE.le, le_csSup, And.intro
38 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma le_rhoMinus_of_subgroup line 449 source
lemma rhoMinus_le_of_subgroup line 542 source
lemma rhoMinus_of_subgroup If $H$ is a finite subgroup of $G$, then $\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|$ line 624 source
Source documentation
If $H$ is a finite subgroup of $G$, then $\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, AddSubgroup, ProbabilityTheory.IsUniform, Finset, Finset.Nonempty, Measurable, Eq, Real, rhoMinus, HSub.hSub, Real.log, Nat.card, Subtype, Membership.mem, SupSet.sSup and 6 more
Proof uses: le_antisymm, And, LT.lt, OfNat.ofNat, LE.le, exists_card_inter_add_eq_sSup, Eq.mpr, id, congrArg, Eq.symm, Nonempty, And.left, Iff.mp, Nat.card_pos_iff, Set.Nonempty.of_subtype
47 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma rhoMinus_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G}
    {U : Ω → G} (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) :
    ρ⁻[U ; μ # A] = log (Nat.card A) -
      log (sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G} : ℕ) := by
…
```
Mentions: hU
lemma rhoPlus_of_subgroup If $H$ is a finite subgroup of $G$, then $\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|$ line 636 source
Source documentation
If $H$ is a finite subgroup of $G$, then $\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, AddSubgroup, ProbabilityTheory.IsUniform, Finset, Finset.Nonempty, Measurable, Eq, Real, rhoPlus, HSub.hSub, Real.log, Set.ncard, SupSet.sSup, Nat, Set.ofPred and 5 more
Proof uses: ProbabilityTheory.entropy, ProbabilityTheory.IsUniform.entropy_eq', Set.toFinite, Membership.mem, Eq.mpr, HAdd.hAdd, rhoMinus, Subtype, id, congrArg, rhoPlus.eq_1, rhoMinus_of_subgroup
42 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma rhoPlus_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G}
    {U : Ω → G} (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) :
    ρ⁺[U ; μ # A] = log ((H : Set G).ncard) -
      log (sSup {Nat.card (A ∩ (t +ᵥ (H : Set G)) : Set G) | t : G} : ℕ) := by
…
```
Mentions: hU
def rho We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$ line 645 source
Source documentation
We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Finset, MeasureTheory.Measure, Real
Proof uses: HDiv.hDiv, HAdd.hAdd, rhoMinus, rhoPlus, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
noncomputable def rho (X : Ω → G) (A : Finset G) (μ : Measure Ω) : ℝ :=
…
```
lemma rho_eq_of_identDistrib line 653 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, ProbabilityTheory.IdentDistrib, Eq, Real, rho
Proof uses: of_eq_true, HDiv.hDiv, HAdd.hAdd, rhoMinus, rhoPlus, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, congr, rhoMinus_eq_of_identDistrib, rhoPlus_eq_of_identDistrib, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma rho_of_uniform We have $\rho(U_A) = 0$ line 658 source
Source documentation
We have $\rho(U_A) = 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Finset, ProbabilityTheory.IsUniform, Measurable, Finset.Nonempty, Eq, Real, rho, OfNat.ofNat
Proof uses: ProbabilityTheory.entropy, Real.log, Nat.card, Subtype, Membership.mem, ProbabilityTheory.IsUniform.entropy_eq', Set.toFinite, Set, Eq.mpr, rhoMinus, id, congrFun', congrArg, Eq.trans, HDiv.hDiv, HAdd.hAdd, rhoPlus, HSub.hSub, Finset.card, congr and 29 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma rho_of_uniform [IsProbabilityMeasure μ]
    {U : Ω → G} {A : Finset G} (hunif : IsUniform A U μ) (hU : Measurable U)
    (hA : A.Nonempty) : ρ[U ; μ # A] = 0 := by
…
```
Mentions: hU
lemma 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}]$ line 672 source
Source documentation
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}]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, AddSubgroup, ProbabilityTheory.IsUniform, Finset, Finset.Nonempty, Measurable, Real, LE.le, rho, Exists, And, HMul.hMul, Real.exp, Neg.neg, HPow.hPow and 10 more
Proof uses: LT.lt, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Nat.card_pos, Nonempty, Finset.Nonempty.to_subtype, Eq, SupSet.sSup, Set.ofPred, exists_card_inter_add_eq_sSup, rhoMinus, rhoMinus_nonneg, rhoPlus, Eq.mpr, HSub.hSub, Real.log and 129 more
179 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma rho_of_subgroup [IsProbabilityMeasure μ] {H : AddSubgroup G} {U : Ω → G}
    (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U)
    (r : ℝ) (hr : ρ[U ; μ # A] ≤ r) :
    ∃ t : G,
      exp (-r) * Nat.card A ^ (1/2 : ℝ) * (H : Set G).ncard ^ (1/2 : ℝ) ≤
        Nat.card ↑(↑A ∩ (t +ᵥ (H : Set G)))
      ∧ Nat.card A ≤ exp (2 * r) * (H : Set G).ncard
      ∧ (H : Set G).ncard ≤ exp (2 * r) * Nat.card A := by
…
```
Mentions: hU
lemma 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}]$ line 722 source
Source documentation
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}]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Module, ZMod, OfNat.ofNat, Nat, Submodule, ProbabilityTheory.IsUniform, Finset, Finset.Nonempty, Measurable, Real, LE.le, rho, Exists, And and 12 more
Proof uses: rho_of_subgroup, Submodule.toAddSubgroup
42 instances, coercions and auxiliary constants left out.
```
lemma rho_of_submodule [IsProbabilityMeasure μ] [Module (ZMod 2) G]
    {H : Submodule (ZMod 2) G} {U : Ω → G}
    (hunif : IsUniform H U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U)
    (r : ℝ) (hr : ρ[U ; μ # A] ≤ r) :
    ∃ t : G,
      exp (-r) * Nat.card A ^ (1 / 2 : ℝ) * (H : Set G).ncard ^ (1 / 2 : ℝ) ≤
        Nat.card ↑(↑A ∩ (t +ᵥ (H : Set G)))
      ∧ Nat.card A ≤ exp (2 * r) * (H : Set G).ncard
      ∧ (H : Set G).ncard ≤ exp (2 * r) * Nat.card A :=
…
```
Mentions: hU
lemma rho_continuous \rho(X)$ depends continuously on the distribution of $X$ line 734 source
Source documentation
\rho(X)$ depends continuously on the distribution of $X$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, TopologicalSpace, DiscreteTopology, BorelSpace, Finset, Finset.Nonempty, Continuous, MeasureTheory.ProbabilityMeasure, Real, rho, id
Proof uses: Continuous.div_const, HAdd.hAdd, rhoMinus, rhoPlus, Continuous.add, rhoMinus_continuous, rhoPlus_continuous, OfNat.ofNat
30 instances, coercions and auxiliary constants left out.
```
lemma rho_continuous [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G]
    {A : Finset G} (hA : A.Nonempty) :
    Continuous fun μ : ProbabilityMeasure G ↦ ρ[(id : G → G) ; μ # A] :=
…
```
lemma tendsto_rho_probabilityMeasure line 739 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, Finset, Filter, TopologicalSpace, BorelSpace, DiscreteTopology, Continuous, Finset.Nonempty, MeasureTheory.ProbabilityMeasure, Filter.Tendsto, nhds, Real, rho
Proof uses: Eq, id, MeasureTheory.ProbabilityMeasure.map, rho_eq_of_identDistrib, ProbabilityTheory.IdentDistrib.mk, Continuous.aemeasurable, aemeasurable_id, of_eq_true, MeasureTheory.Measure, MeasureTheory.Measure.map, Eq.trans, True, congrArg, MeasureTheory.Measure.map_id, eq_self, Eq.mpr, congr, congrFun', funext, Continuous.tendsto and 3 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma rhoMinus_of_sum If $X,Y$ are independent, one has $$ \rho^-(X+Y) \leq \rho^-(X)$$ line 756 source
Source documentation
If $X,Y$ are independent, one has $$ \rho^-(X+Y) \leq \rho^-(X)$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Finset.Nonempty, ProbabilityTheory.IndepFun, LE.le, Real, rhoMinus, HAdd.hAdd
Proof uses: Eq, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, rhoMinus_zero_measure, le_csInf, rhoMinusSet, nonempty_rhoMinusSet, ProbabilityTheory.uniformOn, ProbabilityTheory.isProbabilityMeasure_uniformOn, Finset.finite_toSet, Membership.mem, Set, And and 64 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma rhoMinus_of_sum [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y)
    (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ⁻[X + Y ; μ # A] ≤ ρ⁻[X ; μ # A] := by
…
```
lemma rhoPlus_of_sum If $X,Y$ are independent, one has $$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$ line 815 source
Source documentation
If $X,Y$ are independent, one has $$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Finset.Nonempty, ProbabilityTheory.IndepFun, LE.le, Real, rhoPlus, HAdd.hAdd, HSub.hSub, ProbabilityTheory.entropy
Proof uses: Eq.mpr, rhoMinus, Real.log, Finset.card, id, Eq, Eq.trans, congr, congrArg, Nat.card, Subtype, Membership.mem, Nat, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe, congrFun', rhoMinus_of_sum, le_of_not_gt, LT.lt and 43 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma rhoPlus_of_sum [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ⁺[X + Y ; μ # A] ≤ ρ⁺[X ; μ # A] + H[X + Y ; μ] - H[X ; μ] := by
…
```
lemma rho_of_sum If $X,Y$ are independent, one has $$\rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X]).$$ line 824 source
Source documentation
If $X,Y$ are independent, one has $$\rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X]).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Finset.Nonempty, ProbabilityTheory.IndepFun, LE.le, Real, rho, HAdd.hAdd, HDiv.hDiv, HSub.hSub, ProbabilityTheory.entropy, OfNat.ofNat, Nat
Proof uses: Eq.mpr, rhoMinus, Real.log, Finset.card, id, Eq, congr, congrArg, congrFun', rhoPlus, Nat.card, Subtype, Membership.mem, Eq.trans, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe, rhoMinus_of_sum, le_of_not_gt, LT.lt and 77 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma rho_of_sum [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ[X + Y ; μ # A] ≤ ρ[X ; μ # A] + (H[X+Y ; μ] - H[X ; μ])/2 := by
…
```
lemma rho_le_translate line 831 source
lemma rho_of_translate line 839 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Finset.Nonempty, Eq, Real, rho, HAdd.hAdd
Proof uses: le_antisymm, Eq.mp, LE.le, Neg.neg, congrFun', congrArg, funext, add_neg_cancel_right, Measurable.add_const
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def condRho We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$ line 847 source
Source documentation
We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Finset, MeasureTheory.Measure, Real
Proof uses: tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rho, ProbabilityTheory.cond, SummationFilter.unconditional
7 instances, coercions and auxiliary constants left out.
```
noncomputable def condRho {S : Type*}
    (X : Ω → G) (Y : Ω → S) (A : Finset G) (μ : Measure Ω) : ℝ :=
…
```
def condRhoMinus Average of rhoMinus along the fibers line 852 source
Source documentation
Average of rhoMinus along the fibers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Finset, MeasureTheory.Measure, Real
Proof uses: tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rhoMinus, ProbabilityTheory.cond, SummationFilter.unconditional
7 instances, coercions and auxiliary constants left out.
```
noncomputable def condRhoMinus {S : Type*}
    (X : Ω → G) (Y : Ω → S) (A : Finset G) (μ : Measure Ω) : ℝ :=
…
```
def condRhoPlus Average of rhoPlus along the fibers line 857 source
Source documentation
Average of rhoPlus along the fibers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Finset, MeasureTheory.Measure, Real
Proof uses: tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rhoPlus, ProbabilityTheory.cond, SummationFilter.unconditional
7 instances, coercions and auxiliary constants left out.
```
noncomputable def condRhoPlus {S : Type*}
    (X : Ω → G) (Y : Ω → S) (A : Finset G) (μ : Measure Ω) : ℝ :=
…
```
lemma condRho_of_translate For any $s\in G$, $\rho(X+s|Y)=\rho(X|Y)$ line 874 source
Source documentation
For any $s\in G$, $\rho(X+s|Y)=\rho(X|Y)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, Measurable, Finset.Nonempty, Eq, Real, condRho, HAdd.hAdd
Proof uses: of_eq_true, tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rho, ProbabilityTheory.cond, SummationFilter.unconditional, Eq.trans, True, congrFun', congrArg, SummationFilter, optParam, funext, MeasureTheory.IsZeroOrProbabilityMeasure, rho_of_translate, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma condRho_of_translate {S : Type*}
    {Y : Ω → S} (hX : Measurable X) (hA : A.Nonempty) (s : G) :
    ρ[fun ω ↦ X ω + s | Y ; μ # A] = ρ[X | Y ; μ # A] := by
…
```
lemma condRho_of_injective If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$ line 882 source
Source documentation
If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, MeasureTheory.Measure, Finset, Function.Injective, Eq, Real, condRho, Function.comp
Proof uses: id, Eq.mpr, tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rho, ProbabilityTheory.cond, SummationFilter.unconditional, congrArg, Eq.symm, Function.Injective.tsum_eq, Membership.mem, Function.support, Ne, EmptyCollection.emptyCollection, False.elim, False and 29 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma condRho_of_injective {S T : Type*}
    (Y : Ω → S) {A : Finset G} {f : S → T} (hf : Function.Injective f) :
    ρ[X | f ∘ Y ; μ # A] = ρ[X | Y ; μ # A] := by
…
```
lemma condRho_eq_of_identDistrib line 899 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasurableSingletonClass, Measurable, ProbabilityTheory.IdentDistrib, Prod, prod, Eq, Real, condRho
Proof uses: Eq.mpr, tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rho, ProbabilityTheory.cond, SummationFilter.unconditional, id, congrArg, condRho.eq_1, AddCommMonoid, TopologicalSpace, Eq.rec, SummationFilter, Eq.refl, funext, ENNReal and 36 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma condRhoMinus_le $$ \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]$$ line 925 source
Source documentation
$$ \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsZeroOrProbabilityMeasure, MeasurableSingletonClass, Measurable, Finset.Nonempty, LE.le, Real, condRhoMinus, HSub.hSub, HAdd.hAdd, rhoMinus, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.uniformOn, ProbabilityTheory.isProbabilityMeasure_uniformOn, Finset.finite_toSet, le_csInf, rhoMinusSet, nonempty_rhoMinusSet, Membership.mem, Set, And, ENNReal, MeasureTheory.Measure.map, Prod, Prod.fst, Prod.snd and 76 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma condRhoMinus_le [IsZeroOrProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Finite S] [MeasurableSingletonClass S]
    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :
    ρ⁻[X | Z ; μ # A] ≤ ρ⁻[X ; μ # A] + H[X ; μ] - H[X | Z ; μ] := by
…
```
lemma condRhoPlus_le $$ \rho^+(X|Z) \leq \rho^+(X)$$ line 953 source
Source documentation
$$ \rho^+(X|Z) \leq \rho^+(X)$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsProbabilityMeasure, MeasurableSingletonClass, Measurable, Finset.Nonempty, LE.le, Real, condRhoPlus, rhoPlus
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, condRhoMinus, HSub.hSub, HAdd.hAdd, rhoMinus, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy, condRhoMinus_le, id, tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.cond and 80 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma condRhoPlus_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Finite S] [MeasurableSingletonClass S]
    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :
    ρ⁺[X | Z ; μ # A] ≤ ρ⁺[X ; μ # A] := by
…
```
lemma condRho_eq line 970 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, MeasureTheory.Measure, Finset, Finite, Eq, Real, condRho, HDiv.hDiv, HAdd.hAdd, condRhoMinus, condRhoPlus, OfNat.ofNat, Nat
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, id, tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rho, ProbabilityTheory.cond, SummationFilter.unconditional, Eq.mpr, rhoMinus, rhoPlus, congrFun', congrArg, SummationFilter and 14 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma condRho_le $$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z])$$ line 978 source
Source documentation
$$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z])$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsProbabilityMeasure, MeasurableSingletonClass, Measurable, Finset.Nonempty, LE.le, Real, condRho, HAdd.hAdd, rho, HDiv.hDiv, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy, OfNat.ofNat and 1 more
Proof uses: Eq.mpr, condRhoMinus, condRhoPlus, id, Eq, congrArg, condRho_eq, rhoMinus, rhoPlus, rho.eq_1, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow and 66 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condRho_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Finite S] [MeasurableSingletonClass S]
    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :
    ρ[X | Z ; μ # A] ≤ ρ[X ; μ # A] + (H[X ; μ] - H[X | Z ; μ]) / 2 := by
…
```
lemma condRho_prod_eq_sum line 986 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsProbabilityMeasure, Fintype, MeasurableSingletonClass, Measurable, Eq, Real, condRho, Prod, prod, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set and 1 more
Proof uses: Eq.mpr, tsum, rho, SummationFilter.unconditional, id, congrArg, condRho.eq_1, tsum_fintype, SProd.sprod, Eq.symm, Finset.univ_product_univ, Prod.mk, Finset.sum_product_right, AddCommMonoid, Eq.rec, Eq.refl, funext, Eq.trans, Finset.mul_sum, mul_assoc and 41 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma condRho_prod_le $$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z])$$, conditional version line 1012 source
Source documentation
$$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z])$$, conditional version

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsProbabilityMeasure, MeasurableSingletonClass, Measurable, Finset.Nonempty, LE.le, Real, condRho, Prod, prod, HAdd.hAdd, HDiv.hDiv, HSub.hSub, ProbabilityTheory.condEntropy, OfNat.ofNat and 1 more
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.cond, id, congrArg, condRho_prod_eq_sum, rho, ProbabilityTheory.entropy, Finset.sum_le_sum and 30 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma condRho_prod_le [IsProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]
    [Finite S] [MeasurableSingletonClass S]
    {Z T : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hT : Measurable T) (hA : A.Nonempty) :
    ρ[X | ⟨Z, T⟩ ; μ # A] ≤ ρ[X | T ; μ # A] + (H[X | T ; μ] - H[X | ⟨Z, T⟩ ; μ]) / 2 := by
…
```
lemma condRho_prod_eq_of_indepFun line 1032 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, MeasureTheory.IsProbabilityMeasure, MeasurableSingletonClass, Measurable, ProbabilityTheory.IndepFun, Prod, prod, Eq, Real, condRho
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.cond, id, congrArg, condRho_prod_eq_sum, Eq.symm, Finset.sum_mul, Membership.mem, MeasurableSet and 34 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma rho_of_sum_le If $X,Y$ are independent, then $$ \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$ line 1056 source
Source documentation
If $X,Y$ are independent, then $$ \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Finset.Nonempty, ProbabilityTheory.IndepFun, LE.le, Real, rho, HAdd.hAdd, HDiv.hDiv, rdist
Proof uses: HSub.hSub, ProbabilityTheory.entropy, rho_of_sum, ProbabilityTheory.IndepFun.symm, Eq, ZModModule.sub_eq_add, Eq.mpr, id, congrArg, ProbabilityTheory.IndepFun.rdist_eq, Neg.neg, sub_eq_add_neg, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 72 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma rho_of_sum_le [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ[X + Y ; μ # A] ≤ (ρ[X ; μ # A] + ρ[Y ; μ # A] + d[ X ; μ # Y ; μ]) / 2 := by
…
```
lemma 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]).$$ line 1071 source
Source documentation
If $X,Y$ are independent, then $$ \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, Finset, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Measurable, Finset.Nonempty, ProbabilityTheory.IndepFun, LE.le, Real, condRho, HAdd.hAdd, HDiv.hDiv, rho and 1 more
Proof uses: HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy, condRho_le, Measurable.add, Prod, Eq, Eq.mpr, prod, id, congrArg, ProbabilityTheory.chain_rule'', ProbabilityTheory.entropy_add_right, ProbabilityTheory.IndepFun.entropy_pair_eq_add, ProbabilityTheory.IndepFun.symm, AddCommMonoid, TopologicalSpace, Eq.rec, SummationFilter, tsum and 114 more
148 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma condRho_of_sum_le [IsProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ[X | X + Y ; μ # A] ≤ (ρ[X ; μ # A] + ρ[Y ; μ # A] + d[ X ; μ # Y ; μ ]) / 2 := by
…
```
def phi Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$ line 1118 source
Source documentation
Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Real, Finset, MeasureTheory.Measure
Proof uses: HAdd.hAdd, rdist, HMul.hMul, rho
4 instances, coercions and auxiliary constants left out.
```
noncomputable def phi {Ω : Type*} [MeasurableSpace Ω]
    (X Y : Ω → G) (η : ℝ) (A : Finset G) (μ : Measure Ω) : ℝ :=
…
```
def phiMinimizes Documented declaration: phiMinimizes line 1126 source
Source documentation
Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$ and define a \emph{$\phi$-minimizer} to be a pair of random variables $X,Y$ which minimizes $\phi[X;Y]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Real, Finset, MeasureTheory.Measure
Proof uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, LE.le, phi
2 instances, coercions and auxiliary constants left out.
```
def phiMinimizes {Ω : Type*} [MeasurableSpace Ω] (X Y : Ω → G) (η : ℝ) (A : Finset G)
    (μ : Measure Ω) : Prop :=
…
```
lemma phiMinimizes_of_identDistrib line 1132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Real, Finset, phiMinimizes, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IdentDistrib
Proof uses: Eq, phi, id, Eq.mpr, HAdd.hAdd, rdist, HMul.hMul, rho, congrArg, ProbabilityTheory.IdentDistrib.rdist_congr, rho_eq_of_identDistrib, Eq.refl, Eq.mp, MeasureTheory.IsProbabilityMeasure, Measurable, LE.le, forall_congr, implies_congr, congrFun'
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma phiMinimizes_comm line 1141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Real, Finset, phiMinimizes
Proof uses: Eq, phi, id, Eq.mpr, HAdd.hAdd, rdist, HMul.hMul, rho, congrArg, rdist_symm, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, HPow.hPow and 49 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma phi_min_exists There exists a $\phi$-minimizer line 1152 source
Source documentation
There exists a $\phi$-minimizer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, Finset, Real, Finset.Nonempty, Exists, MeasureTheory.Measure, Prod, And, MeasureTheory.IsProbabilityMeasure, phiMinimizes, Prod.fst, Prod.snd
Proof uses: TopologicalSpace, Bot.bot, DiscreteTopology, DiscreteTopology.mk, rfl, Inhabited, Inhabited.mk, OfNat.ofNat, Continuous, MeasureTheory.ProbabilityMeasure, phi, Iff.mpr, ContinuousAt, continuous_iff_continuousAt, Filter.Tendsto.add, rdist, HMul.hMul, HAdd.hAdd, rho, nhds and 48 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma phi_min_exists (hA : A.Nonempty) : ∃ (μ : Measure (G × G)), IsProbabilityMeasure μ ∧
    phiMinimizes Prod.fst Prod.snd η A μ := by
…
```
Mentions: phiMinimizes
lemma le_rdist_of_phiMinimizes line 1198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, phiMinimizes, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, LE.le, HSub.hSub, rdist, HMul.hMul, rho
Proof uses: Prod, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, inferInstance, MeasureTheory.MeasureSpace.mk, Eq, rfl, Prod.fst, Prod.snd, phi, measurable_fst, measurable_snd, ProbabilityTheory.IdentDistrib, ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, of_eq_true, Eq.trans, True, congrFun', congrArg and 69 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma le_rdist_of_phiMinimizes' line 1223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, phiMinimizes, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, LE.le, rdist, HAdd.hAdd, HMul.hMul, HSub.hSub, rho
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 41 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma condRho_le_condRuzsaDist_of_phiMinimizes line 1234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, MeasurableSingletonClass, phiMinimizes, Measurable, LE.le, HSub.hSub, rdist, HMul.hMul, condRho, rho, condRuzsaDist
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Finset.sum, Finset.univ, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, Eq.mpr, id, congrArg, MeasureTheory.Measure.map, congrFun', Finset.sum_congr, Eq.refl, Membership.mem, MeasureTheory.Measure and 79 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma I_one_le $I_1\le 2\eta d[X_1;X_2]$ line 1288 source
Source documentation
$I_1\le 2\eta d[X_1;X_2]$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, LT.lt, OfNat.ofNat, phiMinimizes, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, MeasureTheory.IsProbabilityMeasure and 8 more
Proof uses: Eq, condRuzsaDist, rdist_add_rdist_add_condMutual_eq, ProbabilityTheory.iIndepFun.reindex_four_abdc, HSub.hSub, condRho, rho, condRho_le_condRuzsaDist_of_phiMinimizes, Measurable.add, Prod, le_rdist_of_phiMinimizes, HDiv.hDiv, Eq.mpr, id, congrArg, rho_eq_of_identDistrib, ProbabilityTheory.IdentDistrib.rdist_congr_right, Measurable.aemeasurable, rho_of_sum_le, ProbabilityTheory.iIndepFun.indepFun and 96 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma I_one_le (hA : A.Nonempty) : I₁ ≤ 2 * η * d[ X₁ # X₂ ] := by
…
```
lemma I_two_aux line 1324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, MeasureTheory.IsProbabilityMeasure, Module, ZMod, Eq, Real and 4 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, sum_of_rdist_eq_char_2', ProbabilityTheory.iIndepFun.reindex_four_cadb, ProbabilityTheory.IdentDistrib.rdist_congr_left, Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.add, Prod, ProbabilityTheory.IdentDistrib.refl, ProbabilityTheory.iIndepFun.indepFun, Ne, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true and 49 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
lemma rdist_add_rdist_eq $d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$ line 1375 source
Source documentation
$d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, MeasureTheory.IsProbabilityMeasure, Module, ZMod, Eq, Real and 5 more
Proof uses: condRuzsaDist, rdist_add_rdist_add_condMutual_eq, ProbabilityTheory.iIndepFun.reindex_four_abdc, I_two_aux, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 46 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_add_rdist_eq :
    d[ X₁ # X₁ ] + d[ X₂ # X₂ ] = 2 * k + (I₂ - I₁) := by
…
```
lemma I_two_aux' line 1385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, MeasureTheory.IsProbabilityMeasure, Module, ZMod, Eq, Real and 5 more
Proof uses: sum_of_rdist_eq_char_2', ProbabilityTheory.iIndepFun.reindex_four_badc, rdist_symm, Eq.mpr, id, congrArg, ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.symm, condRuzsaDist_symm, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 52 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma 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)$ line 1402 source
Source documentation
$I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, LT.lt, OfNat.ofNat, phiMinimizes, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, MeasureTheory.IsProbabilityMeasure and 10 more
Proof uses: rho, le_rdist_of_phiMinimizes, Measurable.add, Prod, condRho, condRuzsaDist, condRho_le_condRuzsaDist_of_phiMinimizes, Eq, I_two_aux', LE.le.trans_eq, rho_of_sum_le, ProbabilityTheory.iIndepFun.indepFun, Ne, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr and 135 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma I_two_le (hA : A.Nonempty) (h'η : η < 1) :
    I₂ ≤ 2 * η * k + (η / (1 - η)) * (2 * η * k - I₁) := by
…
```
lemma dist_le_of_sum_zero Documented declaration: dist_le_of_sum_zero line 1446 source
Source documentation
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2]\le 3\bbI[T_1:T_2\mid T_3] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2]) + \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, phiMinimizes, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Eq, HAdd.hAdd, Measurable, LE.le, rdist and 6 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, MeasureTheory.MeasureSpace.mk, rfl, Eq.mpr, id, congrArg, congr, congrFun', Finset.sum, Finset.univ, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.cond, Finset.sum_le_sum, Membership.mem and 102 more
179 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma dist_le_of_sum_zero {Ω' : Type*} [MeasurableSpace Ω'] {μ : Measure Ω'}
    [IsProbabilityMeasure μ] {T₁ T₂ T₃ : Ω' → G}
    (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :
    k ≤ 3 * I[T₁ : T₂ ; μ] + (2 * H[T₃ ; μ] - H[T₁ ; μ] - H[T₂ ; μ])
      + η * (ρ[T₁ | T₃ ; μ # A] + ρ[T₂ | T₃ ; μ #  A] - ρ[X₁ # A] - ρ[X₂ # A]) := by
…
```
lemma dist_le_of_sum_zero_cond Documented declaration: dist_le_of_sum_zero_cond line 1487 source
Source documentation
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2]\le 3\bbI[T_1:T_2\mid T_3] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2])+ \eta(\rho(T_1|T_3) +\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, phiMinimizes, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Eq, HAdd.hAdd, Measurable, LE.le, rdist, HMul.hMul and 7 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Finset.sum, Finset.univ, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, Eq.mpr, id, congrArg, MeasureTheory.Measure.map, congrFun', Finset.sum_congr, Eq.refl, Membership.mem, MeasureTheory.Measure, Eq.symm and 86 more
144 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma dist_le_of_sum_zero_cond {Ω' : Type*} [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ S : Ω' → G}
    (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃)
    (hS : Measurable S) :
    k ≤ 3 * I[T₁ : T₂ | S] + (2 * H[T₃ | S] - H[T₁ | S] - H[T₂ | S])
      + η * (ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₂ | ⟨T₃, S⟩ #  A] - ρ[X₁ # A] - ρ[X₂ # A]) := by
…
```
lemma dist_le_of_sum_zero' Documented declaration: dist_le_of_sum_zero' line 1517 source
Source documentation
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2] \leq \sum_{1 \leq i < j \leq 3} \bbI[T_i:T_j] + \frac{\eta}{3} \sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, phiMinimizes, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Eq, HAdd.hAdd, Measurable, LE.le, rdist, ProbabilityTheory.mutualInfo and 5 more
Proof uses: ProbabilityTheory.entropy, dist_le_of_sum_zero, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 68 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma dist_le_of_sum_zero' {Ω' : Type*} [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ : Ω' → G} (hsum : T₁ + T₂ + T₃ = 0)
    (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :
    k ≤ I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃]
      + (η / 3) * ((ρ[T₁ | T₂ # A] + ρ[T₂ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₁ | T₃ # A] + ρ[T₃ | T₁ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₂ | T₃ # A] + ρ[T₃ | T₂ # A] - ρ[X₁ # A] - ρ[X₂ # A])) := by
…
```
lemma dist_le_of_sum_zero_cond' Documented declaration: dist_le_of_sum_zero_cond' line 1537 source
Source documentation
If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2] \leq \sum_{1 \leq i < j \leq 3} \bbI[T_i:T_j] + \frac{\eta}{3} \sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, phiMinimizes, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Eq, HAdd.hAdd, Measurable, LE.le, rdist, ProbabilityTheory.condMutualInfo and 7 more
Proof uses: ProbabilityTheory.condEntropy, dist_le_of_sum_zero_cond, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 68 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma dist_le_of_sum_zero_cond' {Ω' : Type*} [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω')] {T₁ T₂ T₃ : Ω' → G} (S : Ω' → G)
    (hsum : T₁ + T₂ + T₃ = 0)
    (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) (hS : Measurable S) :
    k ≤ I[T₁ : T₂ | S] + I[T₁ : T₃| S] + I[T₂ : T₃ | S]
      + (η / 3) * ((ρ[T₁ | ⟨T₂, S⟩ # A] + ρ[T₂ | ⟨T₁, S⟩ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₁ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₁, S⟩ # A] - ρ[X₁ # A] - ρ[X₂ # A])
                 + (ρ[T₂ | ⟨T₃, S⟩ # A] + ρ[T₃ | ⟨T₂, S⟩ # A] - ρ[X₁ # A] - ρ[X₂ # A])) := by
…
```
lemma new_gen_ineq_aux1 line 1552 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Finset.Nonempty, LE.le and 9 more
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, HSub.hSub, ProbabilityTheory.condEntropy, ProbabilityTheory.condMutualInfo_eq', Measurable.add, condRho_prod_le, condRho_of_sum_le, ProbabilityTheory.iIndepFun.indepFun_add_add, List, List.Mem, List.finRange, HEq, Membership.mem, Fintype.elems, Fintype.complete, List.cons and 92 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma new_gen_ineq_aux2 line 1579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Finset.Nonempty, LE.le and 9 more
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Eq.mpr, id, congrArg, rfl, ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk, List, List.Mem, List.finRange, HEq, Membership.mem, Fintype.elems, Fintype.complete, List.cons, List.Mem.head and 142 more
169 instances, coercions and auxiliary constants left out.

Tactic trace: 109 steps
Open to load the checked before-and-after goal states.
lemma new_gen_ineq line 1680 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Finset.Nonempty, LE.le and 10 more
Proof uses: new_gen_ineq_aux1, new_gen_ineq_aux2, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 65 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma 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$ line 1696 source
Source documentation
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$. Then $$\rho(T_1|T_2,S)+\rho(T_2|T_1,S) - \frac{1}{2}\sum_{i} \rho(Y_i) \le \frac{1}{2}(d[Y_1;Y_2]+d[Y_3;Y_4]+d[Y_1;Y_3]+d[Y_2;Y_4]).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Finset.Nonempty, LE.le and 9 more
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, ProbabilityTheory.condMutualInfo, condRuzsaDist, new_gen_ineq, ProbabilityTheory.iIndepFun.reindex_four_acbd, Measurable.add, ProbabilityTheory.condMutualInfo_comm, ProbabilityTheory.condMutualInfo_of_inj_map, sub_right_injective, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, autoParam, MeasureTheory.Measure and 87 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma condRho_sum_le {Y₁ Y₂ Y₃ Y₄ : Ω → G}
    (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄)
    (h_indep : iIndepFun ![Y₁, Y₂, Y₃, Y₄]) (hA : A.Nonempty) :
    ρ[Y₁ + Y₂ | ⟨Y₁ + Y₃, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] + ρ[Y₁ + Y₃ | ⟨Y₁ + Y₂, Y₁ + Y₂ + Y₃ + Y₄⟩ # A] -
      (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 2 ≤
        (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 2 := by
…
```
lemma 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$ line 1750 source
Source documentation
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$. Then $$\sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) - \frac{1}{2}\sum_{i} \rho(Y_i))\le \sum_{1\leq i < j \leq 4}d[Y_i;Y_j]$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Module, ZMod, OfNat.ofNat, Nat, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Finset.Nonempty, HAdd.hAdd and 10 more
Proof uses: condRho_sum_le, ProbabilityTheory.iIndepFun.reindex_four_bacd, Eq, rdist_symm, ProbabilityTheory.iIndepFun.reindex_four_cabd, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, Ring, Int.negOfNat and 66 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma condRho_sum_le' {Y₁ Y₂ Y₃ Y₄ : Ω → G}
      (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄)
      (h_indep : iIndepFun ![Y₁, Y₂, Y₃, Y₄]) (hA : A.Nonempty) :
    let S := Y₁ + Y₂ + Y₃ + Y₄
…
```
lemma dist_of_min_eq_zero' If $X_1, X_2$ is a $\phi$-minimizer, then $d[X_1;X_2] = 0$ line 1777 source
Source documentation
If $X_1, X_2$ is a $\phi$-minimizer, then $d[X_1;X_2] = 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, LT.lt, OfNat.ofNat, phiMinimizes, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, MeasureTheory.IsProbabilityMeasure and 6 more
Proof uses: HAdd.hAdd, HSMul.hSMul, id, Eq.mp, congrArg, ZModModule.char_nsmul_eq_zero, LE.le, ProbabilityTheory.condMutualInfo, HMul.hMul, HSub.hSub, condRho, Prod, prod, rho, dist_le_of_sum_zero_cond', Measurable.add, Eq.mpr, ProbabilityTheory.condMutualInfo_comm, eq_of_heq, HEq and 185 more
183 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
```
lemma dist_of_min_eq_zero' (hA : A.Nonempty) (hη' : η < 1 / 8) : d[X₁ # X₂] = 0 := by
…
```
theorem dist_of_min_eq_zero line 1842 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.MeasureSpace, Finset, Real, LT.lt, OfNat.ofNat, phiMinimizes, MeasureTheory.MeasureSpace.volume, Measurable, MeasureTheory.IsProbabilityMeasure, Module, ZMod, Nat, Finset.Nonempty, HDiv.hDiv, Eq, rdist
Proof uses: Exists, MeasureTheory.Measure, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies4_nondep, Eq.mpr, id, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.rdist_congr, MeasureTheory.MeasureSpace.mk, phiMinimizes_of_identDistrib, ProbabilityTheory.IdentDistrib.symm, dist_of_min_eq_zero', ProbabilityTheory.IdentDistrib.trans
37 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma phiMinimizer_exists_rdist_eq_zero For η ≤ 1/8, there exist phi-minimizers X₁, X₂ at zero Rusza distance line 1858 source
Source documentation
For η ≤ 1/8, there exist phi-minimizers X₁, X₂ at zero Rusza distance. For η < 1/8, all minimizers are fine, by dist_of_min_eq_zero. For η = 1/8, we use a limit of minimizers for η < 1/8, which exists by compactness.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, DiscreteMeasurableSpace, Finset, Module, ZMod, OfNat.ofNat, Nat, Finset.Nonempty, Exists, MeasureTheory.MeasureSpace, And, Measurable, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, phiMinimizes, HDiv.hDiv, Real, Eq and 1 more
Proof uses: StrictMono, Membership.mem, Set, Set.Ioo, Filter.Tendsto, Filter.atTop, nhds, exists_seq_strictMono_tendsto', Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo and 53 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma phiMinimizer_exists_rdist_eq_zero (hA : A.Nonempty) :
    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),
      Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω)
      ∧ phiMinimizes X₁ X₂ (1/8 : ℝ) A ℙ ∧ d[X₁ # X₂] = 0 := by
…
```
Mentions: phiMinimizes
theorem 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].$$ line 1918 source
Source documentation
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].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, MeasurableSpace, DiscreteMeasurableSpace, Measurable, Finset, Finset.Nonempty, Exists, Submodule, And, ProbabilityTheory.IsUniform, LE.le, Real and 4 more
Proof uses: phiMinimizes, HDiv.hDiv, Eq, phiMinimizer_exists_rdist_eq_zero, Classical.byCases, Ne, ENNReal, MeasureTheory.Measure, Set, Set.preimage, Singleton.singleton, Classical.byContradiction, Not, MeasureTheory.Measure.map, Eq.mpr, id, congrArg, MeasureTheory.Measure.map_apply, MeasurableSet.of_discrete, Eq.mp and 123 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
theorem rho_PFR_conjecture [MeasurableSpace G] [DiscreteMeasurableSpace G]
    (Y₁ Y₂ : Ω → G) (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (A : Finset G) (hA : A.Nonempty) :
    ∃ (H : Submodule (ZMod 2) G) (Ω' : Type uG) (mΩ' : MeasureSpace Ω') (U : Ω' → G),
    IsProbabilityMeasure (ℙ : Measure Ω') ∧ Measurable U ∧
    IsUniform H U ∧ 2 * ρ[U # A] ≤ ρ[Y₁ # A] + ρ[Y₂ # A] + 8 * d[Y₁ # Y₂] := by
…
```
lemma 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]$ line 1956 source
Source documentation
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]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, Module, ZMod, OfNat.ofNat, Nat, Set, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, Submodule, And, HPow.hPow, Int, Neg.neg, HDiv.hDiv and 3 more
Proof uses: inferInstance, Membership.mem, MeasurableSpace, Top.top, MeasurableSingletonClass, MeasurableSingletonClass.mk, trivial, LT.lt, PFR_conjecture_pos_aux', Set.toFinite, Finset, Set.Finite.toFinset, Finset.Nonempty, Eq.mpr, id, Eq, congrArg, funext, Set.Finite.coe_toFinset, MeasureTheory.MeasureSpace and 115 more
178 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma better_PFR_conjecture_aux0 {A : Set G} (h₀A : A.Nonempty) {K : ℝ}
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (t : G),
      K ^ (-4 : ℤ) * Nat.card A ^ (1 / 2 : ℝ) * (H : Set G).ncard ^ (1 / 2 : ℝ)
        ≤ Nat.card ↑(A ∩ (H + {t})) ∧
      Nat.card A ≤ K ^ 8 * (H : Set G).ncard ∧ (H : Set G).ncard ≤ K ^ 8 * Nat.card A := by
…
```
lemma better_PFR_conjecture_aux Documented declaration: better_PFR_conjecture_aux line 2006 source
Source documentation
Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup $H$ such that $A$ can be covered by at most $K^5 |A|^{1/2} / |H|^{1/2}$ cosets of $H$, and $H$ has the same cardinality as $A$ up to a multiplicative factor $K^8$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, Module, ZMod, OfNat.ofNat, Nat, Set, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, Submodule, And, HPow.hPow, HDiv.hDiv, Set.ncard, Neg.neg
Proof uses: LT.lt, PFR_conjecture_pos_aux', Set.toFinite, Membership.mem, Int, Inter.inter, Singleton.singleton, better_PFR_conjecture_aux0, Nat.card_pos, Iff.mpr, Nat.cast_pos', Classical.byContradiction, Not, lt_of_lt_of_le, mul_pos, zpow_pos, Real.rpow_pos_of_pos, inferInstance, PartialOrder, False.elim and 92 more
181 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma better_PFR_conjecture_aux {A : Set G} (h₀A : A.Nonempty) {K : ℝ}
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c ≤ K ^ 5 * Nat.card A ^ (1 / 2 : ℝ) * ((H : Set G).ncard : ℝ) ^ (-1 / 2 : ℝ)
      ∧ (H : Set G).ncard ≤ K ^ 8 * Nat.card A
      ∧ Nat.card A ≤ K ^ 8 * (H : Set G).ncard ∧ A ⊆ c + H := by
…
```
theorem better_PFR_conjecture Documented declaration: better_PFR_conjecture line 2053 source
Source documentation
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$.
The ambient group need not be finite, in which case H and c are finite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Set, Real, Set.Nonempty, Set.Finite, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, Submodule, And, LT.lt, HPow.hPow, Set.ncard
Proof uses: Classical.byCases, Finite, PFR_conjecture_pos_aux', Set.toFinite, Membership.mem, HDiv.hDiv, Neg.neg, better_PFR_conjecture_aux, Nat.card_pos, Iff.mpr, Nat.cast_pos', Or, le_or_gt, Exists.intro, And.intro, Trans.trans, Eq, mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, Real.rpow_le_rpow and 220 more
221 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
theorem better_PFR_conjecture {G : Type*} [AddCommGroup G] [Module (ZMod 2) G]
    {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (Afin : A.Finite)
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
      Nat.card c < 2 * K ^ 9 ∧ (H : Set G).ncard ≤ Nat.card A ∧ A ⊆ c + H := by
…
```