Documentation

LeanAPAP.Extras.BSG

theorem quadruple_bound_c {α : Type u_1} [DecidableEq α] {X : Finset α} {a b : α} {H : Finset (α × α)} (ha : a oneOfPair H X) (hb : b oneOfPair H X) (hH : H X ×ˢ X) :
X.card / 2 (Finset.filter (fun (c : α) => (a, c) H (b, c) H) X).card
theorem quadruple_bound_right {α : Type u_1} [DecidableEq α] {B : Finset α} {x : α} [AddCommGroup α] {a b : α} (H : Finset (α × α)) (X : Finset α) (h : x = a - b) :
((Finset.filter (fun (c : α) => (a, c) H (b, c) H) X).sigma fun (c : α) => Finset.filter (fun (x : (α × α) × α × α) => match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ = a - c a₃ - a₄ = b - c) ((B ×ˢ B) ×ˢ B ×ˢ B)).card (Finset.filter (fun (x : (α × α) × α × α) => match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ - (a₃ - a₄) = a - b) ((B ×ˢ B) ×ˢ B ×ˢ B)).card
theorem thing_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} {x : G} :
(𝟭 B 𝟭 A) x = y : G, 𝟭 A y * 𝟭 B (x + y)
theorem thing_one_right {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} {x : G} :
(𝟭 A 𝟭 B) x = (A (x +ᵥ B)).card
theorem thing_two {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} :
s : G, (𝟭 A 𝟭 B) s = A.card * B.card
theorem thing_three {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} :
s : G, (𝟭 A 𝟭 B) s ^ 2 = (A.addEnergy B)
theorem claim_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {R : Type u_2} [CommSemiring R] [StarRing R] {A B : Finset G} :
s : G, (𝟭 A 𝟭 B) s * (A (s +ᵥ B)).card = (A.addEnergy B)
theorem claim_two {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} :
(A.addEnergy B) ^ 2 / (A.card * B.card) s : G, (𝟭 A 𝟭 B) s * (A (s +ᵥ B)).card ^ 2
theorem claim_three {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} (hH : H A ×ˢ A) :
s : G, (𝟭 A 𝟭 B) s * ((A (s +ᵥ B)) ×ˢ (A (s +ᵥ B)) H).card = abH, s : G, (𝟭 A 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s))
theorem claim_four {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} (ab : G × G) :
s : G, (𝟭 A 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s)) B.card * (𝟭 B 𝟭 B) (ab.1 - ab.2)
theorem claim_five {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} (hH : H A ×ˢ A) :
s : G, (𝟭 A 𝟭 B) s * ((A (s +ᵥ B)) ×ˢ (A (s +ᵥ B)) H).card B.card * abH, (𝟭 B 𝟭 B) (ab.1 - ab.2)
noncomputable def H_choice {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (A B : Finset G) (c : ) :
Finset (G × G)
Equations
Instances For
    theorem claim_six {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} (c : ) (hc : 0 c) :
    s : G, (𝟭 A 𝟭 B) s * ((A (s +ᵥ B)) ×ˢ (A (s +ᵥ B)) H_choice A B c).card c / 2 * ((A.addEnergy B) ^ 2 / (A.card * B.card))
    theorem claim_seven {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} (c : ) (hc : 0 c) (hA : 0 < A.card) (hB : 0 < B.card) :
    s : G, (𝟭 A 𝟭 B) s * (c / 2 * ((A.addEnergy B) ^ 2 / (A.card ^ 2 * B.card ^ 2)) + ((A (s +ᵥ B)) ×ˢ (A (s +ᵥ B)) H_choice A B c).card) s : G, (𝟭 A 𝟭 B) s * (c * (A (s +ᵥ B)).card ^ 2)
    theorem claim_eight {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} (c : ) (hc : 0 c) (hA : 0 < A.card) (hB : 0 < B.card) :
    ∃ (s : G), c / 2 * ((A.addEnergy B) ^ 2 / (A.card ^ 2 * B.card ^ 2)) + ((A (s +ᵥ B)) ×ˢ (A (s +ᵥ B)) H_choice A B c).card c * (A (s +ᵥ B)).card ^ 2
    theorem test_case {E A B : } {K : } (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B) E) (hA : 0 < A) (hB : 0 < B) :
    A / (2 * K) 2⁻¹ * (E / (A * B))
    theorem lemma_one {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {c K : } (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (A.card ^ 2 * B.card) (A.addEnergy B)) (hA : 0 < A.card) (hB : 0 < B.card) :
    ∃ (s : G), XA (s +ᵥ B), A.card / (2 * K) X.card (1 - c) * X.card ^ 2 (Finset.filter (fun (x : G × G) => match x with | (a, b) => c / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) (a - b)) (X ×ˢ X)).card
    theorem lemma_one' {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {c K : } (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (A.card ^ 2 * B.card) (A.addEnergy B)) (hA : 0 < A.card) (hB : 0 < B.card) :
    ∃ (s : G), XA (s +ᵥ B), A.card / (2 * K) X.card (1 - c) * X.card ^ 2 (Finset.filter (fun (x : G × G) => match x with | (a, b) => c / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) (a - b)) (X ×ˢ X)).card
    theorem many_pairs {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : } {x : G} (hab : 1 / 8 / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) x) :
    A.card / (2 ^ 4 * K ^ 2) (Finset.filter (fun (x_1 : G × G) => match x_1 with | (c, d) => c - d = x) (B ×ˢ B)).card
    theorem quadruple_bound_part {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : } (a c : G) (hac : 1 / 8 / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) (a - c)) :
    A.card / (2 ^ 4 * K ^ 2) (Finset.filter (fun (x : G × G) => match x with | (a₁, a₂) => a₁ - a₂ = a - c) (B ×ˢ B)).card
    theorem quadruple_bound_other {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {a b c : G} {K : } {H : Finset (G × G)} (hac : (a, c) H) (hbc : (b, c) H) (hH : xH, 1 / 8 / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) (x.1 - x.2)) :
    (A.card / (2 ^ 4 * K ^ 2)) ^ 2 (Finset.filter (fun (x : (G × G) × G × G) => match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ = a - c a₃ - a₄ = b - c) ((B ×ˢ B) ×ˢ B ×ˢ B)).card
    theorem quadruple_bound_left {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B X : Finset G} {a b : G} {K : } {H : Finset (G × G)} (ha : a oneOfPair H X) (hb : b oneOfPair H X) (hH : xH, 1 / 8 / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) (x.1 - x.2)) (hH' : H X ×ˢ X) :
    X.card / 2 * (A.card / (2 ^ 4 * K ^ 2)) ^ 2 ((Finset.filter (fun (c : G) => (a, c) H (b, c) H) X).sigma fun (c : G) => Finset.filter (fun (x : (G × G) × G × G) => match x with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ = a - c a₃ - a₄ = b - c) ((B ×ˢ B) ×ˢ B ×ˢ B)).card
    theorem quadruple_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} {X : Finset G} {K : } {x : G} (hx : x oneOfPair H X - oneOfPair H X) (hH : xH, 1 / 8 / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) (x.1 - x.2)) (hH' : H X ×ˢ X) :
    A.card ^ 2 * X.card / (2 ^ 9 * K ^ 4) (Finset.filter (fun (x_1 : (G × G) × G × G) => match x_1 with | ((a₁, a₂), a₃, a₄) => a₁ - a₂ - (a₃ - a₄) = x) ((B ×ˢ B) ×ˢ B ×ˢ B)).card
    theorem big_quadruple_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {H : Finset (G × G)} {X : Finset G} {K : } (hH : xH, 1 / 8 / 2 * (K ^ 2)⁻¹ * A.card (𝟭 B 𝟭 B) (x.1 - x.2)) (hH' : H X ×ˢ X) (hX : A.card / (2 * K) X.card) :
    (oneOfPair H X - oneOfPair H X).card * (A.card ^ 3 / (2 ^ 10 * K ^ 5)) B.card ^ 4
    theorem BSG_aux {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : } (hK : 0 < K) (hA : 0 < A.card) (hB : 0 < B.card) (hAB : K⁻¹ * (A.card ^ 2 * B.card) (A.addEnergy B)) :
    ∃ (s : G), A'A (s +ᵥ B), (2 ^ 4)⁻¹ * K⁻¹ * A.card A'.card (A' - A').card 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3
    theorem BSG {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : } (hK : 0 K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) (A.addEnergy B)) :
    A'A, (2 ^ 4)⁻¹ * K⁻¹ * A.card A'.card (A' - A').card 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3
    theorem BSG₂ {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A B : Finset G} {K : } (hK : 0 K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) (A.addEnergy B)) :
    A'A, B'B, (2 ^ 4)⁻¹ * K⁻¹ * A.card A'.card (2 ^ 4)⁻¹ * K⁻¹ * A.card B'.card (A' - B').card 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3
    theorem BSG_self {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {K : } (hK : 0 K) (hA : A.Nonempty) (hAK : K⁻¹ * A.card ^ 3 (A.addEnergy A)) :
    A'A, (2 ^ 4)⁻¹ * K⁻¹ * A.card A'.card (A' - A').card 2 ^ 10 * K ^ 5 * A.card
    theorem BSG_self' {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Finset G} {K : } (hK : 0 K) (hA : A.Nonempty) (hAK : K⁻¹ * A.card ^ 3 (A.addEnergy A)) :
    A'A, (2 ^ 4)⁻¹ * K⁻¹ * A.card A'.card (A' - A').card 2 ^ 14 * K ^ 6 * A'.card