def Finset.«termEₘ[_,_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Finset.«termEₘ[_,_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Finset.«termE[_,_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Finset.«termE[_,_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Finset.«termEₘ[_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Finset.«termEₘ[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Finset.«termE[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Finset.«termE[_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

abbrev Finset.additiveEnergy_eq_card_filter.match_3 {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) (motive : (x : (α × α) × α × α) → x ∈ Finset.filter (fun (x : (α × α) × α × α) => Finset.additiveEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t) → Prop) : ∀ (x : (α × α) × α × α) (h : x ∈ Finset.filter (fun (x : (α × α) × α × α) => Finset.additiveEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)), (∀ (a b c d : α) (h : ((a, b), c, d) ∈ Finset.filter (fun (x : (α × α) × α × α) => Finset.additiveEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)), motive ((a, b), c, d) h) → motive x h

Equations

• ⋯ = ⋯

theorem Finset.additiveEnergy_eq_card_filter {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) : E[s, t] = (Finset.filter (fun (x : (α × α) × α × α) => Finset.additiveEnergy_eq_card_filter.match_1 (fun (x : (α × α) × α × α) => Prop) x fun (a b c d : α) => a + b = c + d) ((s ×ˢ t) ×ˢ s ×ˢ t)).card

abbrev Finset.additiveEnergy_eq_card_filter.match_1 {α : Type u_1} (motive : (α × α) × α × α → Sort u_2) : (x : (α × α) × α × α) → ((a b c d : α) → motive ((a, b), c, d)) → motive x

Equations

• One or more equations did not get rendered due to their size.

abbrev Finset.additiveEnergy_eq_card_filter.match_2 {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) (motive : (x : (α × α) × α × α) → x ∈ Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t) → Sort u_2) : (x : (α × α) × α × α) → (x_1 : x ∈ Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)) → ((a b c d : α) → (x : ((a, b), c, d) ∈ Finset.filter (fun (x : (α × α) × α × α) => x.1.1 + x.2.1 = x.1.2 + x.2.2) ((s ×ˢ s) ×ˢ t ×ˢ t)) → motive ((a, b), c, d) x) → motive x x_1

Equations

• One or more equations did not get rendered due to their size.

theorem Finset.multiplicativeEnergy_eq_card_filter {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) : Eₘ[s, t] = (Finset.filter (fun (x : (α × α) × α × α) => match x with | ((a, b), c, d) => a * b = c * d) ((s ×ˢ t) ×ˢ s ×ˢ t)).card

abbrev Finset.additiveEnergy_eq_sum_sq'.match_1 {α : Type u_1} (motive : α × α → Sort u_2) : (x : α × α) → ((x y : α) → motive (x, y)) → motive x

Equations

• Finset.additiveEnergy_eq_sum_sq'.match_1 motive x h_1 = Prod.casesOn x fun (fst snd : α) => h_1 fst snd

theorem Finset.additiveEnergy_eq_sum_sq' {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) : E[s, t] = Finset.sum (s + t) fun (a : α) => (Finset.filter (fun (x : α × α) => Finset.additiveEnergy_eq_sum_sq'.match_1 (fun (x : α × α) => Prop) x fun (x y : α) => x + y = a) (s ×ˢ t)).card ^ 2

theorem Finset.multiplicativeEnergy_eq_sum_sq' {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) : Eₘ[s, t] = Finset.sum (s * t) fun (a : α) => (Finset.filter (fun (x : α × α) => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2

theorem Finset.additiveEnergy_eq_sum_sq {α : Type u_1} [DecidableEq α] [Add α] [Fintype α] (s : Finset α) (t : Finset α) : E[s, t] = Finset.sum Finset.univ fun (a : α) => (Finset.filter (fun (x : α × α) => Finset.additiveEnergy_eq_sum_sq'.match_1 (fun (x : α × α) => Prop) x fun (x y : α) => x + y = a) (s ×ˢ t)).card ^ 2

theorem Finset.multiplicativeEnergy_eq_sum_sq {α : Type u_1} [DecidableEq α] [Mul α] [Fintype α] (s : Finset α) (t : Finset α) : Eₘ[s, t] = Finset.sum Finset.univ fun (a : α) => (Finset.filter (fun (x : α × α) => match x with | (x, y) => x * y = a) (s ×ˢ t)).card ^ 2

theorem Finset.card_sq_le_card_mul_additiveEnergy {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) (u : Finset α) : (Finset.filter (fun (x : α × α) => Finset.additiveEnergy_eq_sum_sq'.match_1 (fun (x : α × α) => Prop) x fun (a b : α) => a + b ∈ u) (s ×ˢ t)).card ^ 2 ≤ u.card * E[s, t]

theorem Finset.card_sq_le_card_mul_multiplicativeEnergy {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) (u : Finset α) : (Finset.filter (fun (x : α × α) => match x with | (a, b) => a * b ∈ u) (s ×ˢ t)).card ^ 2 ≤ u.card * Eₘ[s, t]

theorem Finset.le_card_add_mul_additiveEnergy {α : Type u_1} [DecidableEq α] [Add α] (s : Finset α) (t : Finset α) : s.card ^ 2 * t.card ^ 2 ≤ (s + t).card * E[s, t]

theorem Finset.le_card_add_mul_multiplicativeEnergy {α : Type u_1} [DecidableEq α] [Mul α] (s : Finset α) (t : Finset α) : s.card ^ 2 * t.card ^ 2 ≤ (s * t).card * Eₘ[s, t]