PFR/ForMathlib/Entropy/RuzsaSetDist.lean

GitHub source file

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

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

8 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. def 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 line 17 source

    Source documentation

    The Ruzsa distance between two subsets A, B of a group G is defined to be the Ruzsa distance between their uniform probability distributions. Is only intended for use when A, B are finite and non-empty.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasurableSpace, AddCommGroup, Set, Real

    Proof uses: ProbabilityTheory.Kernel.rdistm, ProbabilityTheory.uniformOn

    noncomputable def setRuzsaDist (A B : Set G) : ℝ := Kernel.rdistm (uniformOn A) (uniformOn B)
…

    Mentions: ProbabilityTheory.Kernel.rdistm

  2. lemma ProbabilityTheory.setRuzsaDist_eq_rdist Relating Ruzsa distance between sets to Ruzsa distance between random variables line 23 source

    Source documentation

    Relating Ruzsa distance between sets to Ruzsa distance between random variables

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Set, Finite, MeasureTheory.MeasureSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IsUniform, Measurable, Eq, Real, ProbabilityTheory.setRuzsaDist, rdist

    Proof uses: Eq.mpr, ProbabilityTheory.Kernel.rdistm, MeasureTheory.Measure.map, id, congrArg, rdist_eq_rdistm, ProbabilityTheory.uniformOn, Iff.mp, ProbabilityTheory.isUniform_iff_map_eq_uniformOn, Eq.refl

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    lemma setRuzsaDist_eq_rdist {A B : Set G} [Finite A] [Finite B]
    {Ω Ω' : Type*} [mΩ : MeasureSpace Ω] [mΩ' : MeasureSpace Ω']
    {μ : Measure Ω} {μ' : Measure Ω'}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    {UA : Ω → G} {UB : Ω' → G} (hUA : IsUniform A UA μ) (hUB : IsUniform B UB μ')
    (hUA_mes : Measurable UA) (hUB_mes : Measurable UB) :
    dᵤ[A # B] = d[UA ; μ # UB ; μ'] := by
…

    Mentions: ProbabilityTheory.IsUniform

  3. lemma ProbabilityTheory.setRuzsaDist_nonneg Ruzsa distance between sets is nonnegative line 34 source

    Source documentation

    Ruzsa distance between sets is nonnegative.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Set, Finite, Nonempty, LE.le, Real, OfNat.ofNat, ProbabilityTheory.setRuzsaDist

    Proof uses: Exists, MeasureTheory.MeasureSpace, And, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange, ProbabilityTheory.exists_isUniform_measureSpace', Set.Nonempty.of_subtype, Eq.mpr, rdist, id, Eq, congrArg, ProbabilityTheory.setRuzsaDist_eq_rdist, rdist_nonneg

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    lemma setRuzsaDist_nonneg (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B] :
    0 ≤ dᵤ[A # B] := by
…
  4. lemma ProbabilityTheory.setRuzsaDist_symm Ruzsa distance between sets is symmetric line 44 source

    Source documentation

    Ruzsa distance between sets is symmetric.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Set, Finite, Nonempty, Eq, Real, ProbabilityTheory.setRuzsaDist

    Proof uses: Exists, MeasureTheory.MeasureSpace, And, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange, ProbabilityTheory.exists_isUniform_measureSpace', Set.Nonempty.of_subtype, Eq.mpr, rdist, id, congrArg, ProbabilityTheory.setRuzsaDist_eq_rdist, rdist_symm

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    lemma setRuzsaDist_symm (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B] :
    dᵤ[A # B] = dᵤ[B # A] := by
…
  5. lemma ProbabilityTheory.setRuzsaDist_triangle Ruzsa distance between sets obeys the triangle inequality line 55 source

    Source documentation

    Ruzsa distance between sets obeys the triangle inequality.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Set, Finite, Nonempty, LE.le, Real, ProbabilityTheory.setRuzsaDist, HAdd.hAdd

    Proof uses: Exists, MeasureTheory.MeasureSpace, And, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange, ProbabilityTheory.exists_isUniform_measureSpace', Set.Nonempty.of_subtype, Eq.mpr, rdist, id, Eq, congrArg, ProbabilityTheory.setRuzsaDist_eq_rdist, rdist_triangle

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

    lemma setRuzsaDist_triangle (A B C : Set G) [hA : Finite A] [hB : Finite B] [hC : Finite C]
    [Nonempty A] [Nonempty B] [Nonempty C] : dᵤ[A # C] ≤ dᵤ[A # B] + dᵤ[B # C] := by
…
  6. lemma ProbabilityTheory.setRuzsaDist_add_const Ruzsa distance between sets is translation invariant line 69 source

    Source documentation

    Ruzsa distance between sets is translation invariant.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Set, Finite, Nonempty, Eq, Real, ProbabilityTheory.setRuzsaDist, HAdd.hAdd, Singleton.singleton

    Proof uses: Exists, MeasureTheory.MeasureSpace, And, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange, ProbabilityTheory.exists_isUniform_measureSpace', Set.Nonempty.of_subtype, Eq.mpr, rdist, id, congrArg, ProbabilityTheory.setRuzsaDist_eq_rdist, Eq.symm, rdist_add_const', Set.Finite.add, Set.finite_singleton and 33 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

    Open to load the checked before-and-after goal states.

    lemma setRuzsaDist_add_const (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B]
    (c c' : G) : dᵤ[A + {c} # B + {c'}] = dᵤ[A # B] := by
…
  7. lemma ProbabilityTheory.setRuzsaDist_of_inj Ruzsa distance between sets is preserved by injective homomorphisms line 90 source

    Source documentation

    Ruzsa distance between sets is preserved by injective homomorphisms.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Set, Finite, Nonempty, AddMonoidHom, Function.Injective, Eq, Real, ProbabilityTheory.setRuzsaDist, Set.image

    Proof uses: Exists, MeasureTheory.MeasureSpace, And, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform, Membership.mem, FiniteRange, ProbabilityTheory.exists_isUniform_measureSpace', Set.Nonempty.of_subtype, Eq.mpr, rdist, id, congrArg, ProbabilityTheory.setRuzsaDist_eq_rdist, Function.comp, Eq.symm, rdist_of_inj, Eq.refl and 24 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

    Open to load the checked before-and-after goal states.

    lemma setRuzsaDist_of_inj (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B]
    {H : Type*} [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H]
    [Countable H] {φ : G →+ H} (hφ : Function.Injective φ) :
    dᵤ[φ '' A # φ '' B] = dᵤ[A # B] := by
…
  8. lemma ProbabilityTheory.setRuzsaDist_le Ruzsa distance between sets is controlled by the doubling constant line 110 source

    Source documentation

    Ruzsa distance between sets is controlled by the doubling constant.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Countable, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Set, Finite, Set.Nonempty, LE.le, Real, ProbabilityTheory.setRuzsaDist, HSub.hSub, Real.log, Nat.card, HDiv.hDiv, OfNat.ofNat, Nat

    Proof uses: Set.Finite.sub, Nonempty, Set.Nonempty.to_subtype, id, ProbabilityTheory.Kernel.rdistm, ProbabilityTheory.uniformOn, Eq.mpr, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, Eq, congrFun', congrArg, congr, ProbabilityTheory.entropy_of_uniformOn, sub_le_sub_right, Finset.card and 58 more

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

    Open to load the checked before-and-after goal states.

    lemma setRuzsaDist_le (A B : Set G) [h'A : Finite A] [h'B : Finite B]
    (hA : A.Nonempty) (hB : B.Nonempty) :
    dᵤ[A # B] ≤ log (Nat.card (A-B)) - log (Nat.card A) / 2 - log (Nat.card B) / 2 := by
…