Documentation

AddCombi.Mathlib.Combinatorics.Additive.Energy

Additive energy #

This file defines the additive energy of two finsets of a group. This is a central quantity in additive combinatorics.

Main declarations #

Notation #

The following notations are defined in the Combinatorics.Additive scope:

TODO #

It's possibly interesting to have (s ×ˢ s) ×ˢ t ×ˢ t).filter (fun x : (M × M) × M × M ↦ x.1.1 * x.2.1 = x.1.2 * x.2.2) (whose density in G × G × G is mulEnergy' s t) as a standalone definition.

source
def Finset.mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :
ℚ≥0

The multiplicative energy Eₘ[s, t] of two finsets s and t in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × t × t such that a₁ * b₁ = a₂ * b₂.

The notation Eₘ[s, t] is available in scope Combinatorics.Additive.

Equations
Instances For
    source
    def Finset.addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :
    ℚ≥0

    The additive energy E[s, t] of two finsets s and t in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × t × t such that a₁ + b₁ = a₂ + b₂.

    The notation E[s, t] is available in scope Combinatorics.Additive.

    Equations
    Instances For
      source
      def Combinatorics.Additive'.«termEₘ[_,_]» :
      Lean.ParserDescr

      The multiplicative energy of two finsets s and t in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × t × t such that a₁ * b₁ = a₂ * b₂.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Combinatorics.Additive'.«termE[_,_]» :
        Lean.ParserDescr

        The additive energy of two finsets s and t in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × t × t such that a₁ + b₁ = a₂ + b₂.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Combinatorics.Additive'.«termEₘ[_]» :
          Lean.ParserDescr

          The multiplicative energy of a finset s in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × s × s such that a₁ * b₁ = a₂ * b₂.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Combinatorics.Additive'.«termE[_]» :
            Lean.ParserDescr

            The additive energy of a finset s in a group is the number of quadruples (a₁, a₂, b₁, b₂) ∈ s × s × s × s such that a₁ + b₁ = a₂ + b₂.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Finset.mulEnergy'_mono {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s₁ s₂ t₁ t₂ : Finset M} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
              s₁.mulEnergy' t₁ ≤ s₂.mulEnergy' t₂
              source
              theorem Finset.addEnergy'_mono {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s₁ s₂ t₁ t₂ : Finset M} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
              s₁.addEnergy' t₁ ≤ s₂.addEnergy' t₂
              source
              theorem Finset.mulEnergy'_mono_left {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s₁ s₂ t : Finset M} (hs : s₁ ⊆ s₂) :
              s₁.mulEnergy' t ≤ s₂.mulEnergy' t
              source
              theorem Finset.addEnergy'_mono_left {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s₁ s₂ t : Finset M} (hs : s₁ ⊆ s₂) :
              s₁.addEnergy' t ≤ s₂.addEnergy' t
              source
              theorem Finset.mulEnergy'_mono_right {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t₁ t₂ : Finset M} (ht : t₁ ⊆ t₂) :
              s.mulEnergy' t₁ ≤ s.mulEnergy' t₂
              source
              theorem Finset.addEnergy'_mono_right {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t₁ t₂ : Finset M} (ht : t₁ ⊆ t₂) :
              s.addEnergy' t₁ ≤ s.addEnergy' t₂
              source
              theorem Finset.dens_mul_dens_le_mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} :
              s.dens * t.dens / ↑(Fintype.card M) ≤ s.mulEnergy' t
              source
              theorem Finset.dens_add_dens_le_addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} :
              s.dens * t.dens / ↑(Fintype.card M) ≤ s.addEnergy' t
              source
              theorem Finset.dens_sq_le_mulEnergy'_self {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} :
              s.dens ^ 2 / ↑(Fintype.card M) ≤ s.mulEnergy' s
              source
              theorem Finset.dens_sq_le_addEnergy'_self {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} :
              s.dens ^ 2 / ↑(Fintype.card M) ≤ s.addEnergy' s
              source
              theorem Finset.mulEnergy'_pos {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} (hs : s.Nonempty) (ht : t.Nonempty) :
              0 < s.mulEnergy' t
              source
              theorem Finset.addEnergy'_pos {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} (hs : s.Nonempty) (ht : t.Nonempty) :
              0 < s.addEnergy' t
              source
              theorem Finset.mulEnergy'_self_pos {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} (hs : s.Nonempty) :
              0 < s.mulEnergy' s
              source
              theorem Finset.addEnergy'_self_pos {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} (hs : s.Nonempty) :
              0 < s.addEnergy' s
              source
              @[simp]
              theorem Finset.mulEnergy'_empty_left {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (t : Finset M) :
              ∅.mulEnergy' t = 0
              source
              @[simp]
              theorem Finset.addEnergy'_empty_left {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (t : Finset M) :
              ∅.addEnergy' t = 0
              source
              @[simp]
              theorem Finset.mulEnergy'_empty_right {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s : Finset M) :
              s.mulEnergy' ∅ = 0
              source
              @[simp]
              theorem Finset.addEnergy'_empty_right {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s : Finset M) :
              s.addEnergy' ∅ = 0
              source
              @[simp]
              theorem Finset.mulEnergy'_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} :
              0 < s.mulEnergy' t ↔ s.Nonempty ∧ t.Nonempty
              source
              @[simp]
              theorem Finset.addEnergy'_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} :
              0 < s.addEnergy' t ↔ s.Nonempty ∧ t.Nonempty
              source
              @[simp]
              theorem Finset.mulEnergy'_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s t : Finset M} :
              s.mulEnergy' t = 0 ↔ s = ∅ ∨ t = ∅
              source
              @[simp]
              theorem Finset.addEnergy'_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s t : Finset M} :
              s.addEnergy' t = 0 ↔ s = ∅ ∨ t = ∅
              source
              theorem Finset.mulEnergy'_self_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} :
              0 < s.mulEnergy' s ↔ s.Nonempty
              source
              theorem Finset.addEnergy'_self_pos_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} :
              0 < s.addEnergy' s ↔ s.Nonempty
              source
              theorem Finset.mulEnergy'_self_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] {s : Finset M} :
              s.mulEnergy' s = 0 ↔ s = ∅
              source
              theorem Finset.addEnergy'_self_eq_zero_iff {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] {s : Finset M} :
              s.addEnergy' s = 0 ↔ s = ∅
              source
              theorem Finset.addEnergy'_eq_card_filter {M : Type u_2} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :
              s.addEnergy' t = ↑{x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 + x.1.2 = x.2.1 + x.2.2}.card / ↑(Fintype.card M) ^ 3
              source
              theorem Finset.mulEnergy'_eq_card_filter {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :
              s.mulEnergy' t = ↑{x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}.card / ↑(Fintype.card M) ^ 3
              source
              theorem Finset.addEnergy'_eq_sum_sq' {M : Type u_2} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :
              s.addEnergy' t = ↑(∑ a ∈ s + t, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3
              source
              theorem Finset.mulEnergy'_eq_sum_sq' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :
              s.mulEnergy' t = ↑(∑ a ∈ s * t, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3
              source
              theorem Finset.addEnergy'_eq_sum_sq {M : Type u_2} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :
              s.addEnergy' t = ↑(∑ a : M, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3
              source
              theorem Finset.mulEnergy'_eq_sum_sq {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :
              s.mulEnergy' t = ↑(∑ a : M, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2) / ↑(Fintype.card M) ^ 3
              source
              theorem Finset.card_sq_le_card_mul_mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t u : Finset M) :
              {xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}.dens ^ 2 ≤ u.dens * s.mulEnergy' t
              source
              theorem Finset.card_sq_le_card_mul_addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s t u : Finset M) :
              {xy ∈ s ×ˢ t | xy.1 + xy.2 ∈ u}.dens ^ 2 ≤ u.dens * s.addEnergy' t
              source
              theorem Finset.le_card_mul_mul_mulEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [Monoid M] (s t : Finset M) :
              s.dens ^ 2 * t.dens ^ 2 ≤ (s * t).dens * s.mulEnergy' t
              source
              theorem Finset.le_card_add_mul_addEnergy' {M : Type u_1} [Fintype M] [DecidableEq M] [AddMonoid M] (s t : Finset M) :
              s.dens ^ 2 * t.dens ^ 2 ≤ (s + t).dens * s.addEnergy' t
              source
              theorem Finset.mulEnergy'_comm {M : Type u_1} [Fintype M] [DecidableEq M] [CommMonoid M] (s t : Finset M) :
              s.mulEnergy' t = t.mulEnergy' s
              source
              theorem Finset.addEnergy'_comm {M : Type u_1} [Fintype M] [DecidableEq M] [AddCommMonoid M] (s t : Finset M) :
              s.addEnergy' t = t.addEnergy' s
              source
              @[simp]
              theorem Finset.mulEnergy'_univ_left {M : Type u_1} [Fintype M] [DecidableEq M] [CommGroup M] (t : Finset M) :
              univ.mulEnergy' t = t.dens ^ 2
              source
              @[simp]
              theorem Finset.addEnergy'_univ_left {M : Type u_1} [Fintype M] [DecidableEq M] [AddCommGroup M] (t : Finset M) :
              univ.addEnergy' t = t.dens ^ 2
              source
              @[simp]
              theorem Finset.mulEnergy'_univ_right {M : Type u_1} [Fintype M] [DecidableEq M] [CommGroup M] (s : Finset M) :
              s.mulEnergy' univ = s.dens ^ 2
              source
              @[simp]
              theorem Finset.addEnergy'_univ_right {M : Type u_1} [Fintype M] [DecidableEq M] [AddCommGroup M] (s : Finset M) :
              s.addEnergy' univ = s.dens ^ 2