Documentation
Pseudorandom
.
Additive
.
Stab
Search
Google site search
return to top
source
Imports
Init
Mathlib.Tactic.Rify
Pseudorandom.Additive.Constants
Pseudorandom.Additive.Growth
Mathlib.Combinatorics.SetFamily.CauchyDavenport
Imported by
Stab
Stab_inv'
one_le_of_mem
Stab_neg'
Stab_add'
Stab_mul'
Stab_le'
Stab_le
Stab_le₂
Stab_add
Stab_neg
Stab_sub
Stab_mul
Stab_nsmul
Stab_subset
Stab_card_inc
Stab_card_inc'
Stab_card_inc_rep
Stab_full'
Stab_full
Stab_no_full
Stab_small
source
noncomputable def
Stab
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(K :
ℝ
)
(A :
Finset
α
)
:
Finset
α
Equations
Stab
K
A
=
Finset.filter
(
fun (
a
:
α
) =>
↑
(
A
+
a
•
A
)
.card
≤
K
*
↑
A
.card
)
Finset.univ
Instances For
source
theorem
Stab_inv'
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
{a :
α
}
(h :
a
∈
Stab
K
A
)
:
1
/
a
∈
Stab
K
A
source
theorem
one_le_of_mem
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
{a :
α
}
(hA :
A
.Nonempty
)
(h :
a
∈
Stab
K
A
)
:
1
≤
K
source
theorem
Stab_neg'
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
{a :
α
}
(h :
a
∈
Stab
K
A
)
:
-
a
∈
Stab
(
K
^
3
)
A
source
theorem
Stab_add'
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K₁ :
ℝ
}
{K₂ :
ℝ
}
{a :
α
}
{b :
α
}
(h₁ :
a
∈
Stab
K₁
A
)
(h₂ :
b
∈
Stab
K₂
A
)
:
a
+
b
∈
Stab
(
K₁
^
8
*
K₂
)
A
source
theorem
Stab_mul'
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K₁ :
ℝ
}
{K₂ :
ℝ
}
{a :
α
}
{b :
α
}
(h₁ :
a
∈
Stab
K₁
A
)
(h₂ :
b
∈
Stab
K₂
A
)
:
a
*
b
∈
Stab
(
K₁
*
K₂
)
A
source
theorem
Stab_le'
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
{K₂ :
ℝ
}
{a :
α
}
(h₁ :
a
∈
Stab
K
A
)
(h₂ :
K
≤
K₂
)
:
a
∈
Stab
K₂
A
source
theorem
Stab_le
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
{K₂ :
ℝ
}
(h₂ :
K
≤
K₂
)
:
Stab
K
A
⊆
Stab
K₂
A
source
theorem
Stab_le₂
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
{K₂ :
ℝ
}
(h₂ :
1
≤
K
→
K
≤
K₂
)
:
Stab
K
A
⊆
Stab
K₂
A
source
theorem
Stab_add
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K₁ :
ℝ
}
{K₂ :
ℝ
}
:
Stab
K₁
A
+
Stab
K₂
A
⊆
Stab
(
K₁
^
8
*
K₂
)
A
source
theorem
Stab_neg
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
:
-
Stab
K
A
⊆
Stab
(
K
^
3
)
A
source
theorem
Stab_sub
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K₁ :
ℝ
}
{K₂ :
ℝ
}
:
Stab
K₁
A
-
Stab
K₂
A
⊆
Stab
(
K₁
^
8
*
K₂
^
3
)
A
source
theorem
Stab_mul
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K₁ :
ℝ
}
{K₂ :
ℝ
}
:
Stab
K₁
A
*
Stab
K₂
A
⊆
Stab
(
K₁
*
K₂
)
A
source
theorem
Stab_nsmul
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
(n :
ℕ
)
:
(
n
+
1
)
•
Stab
K
A
⊆
Stab
(
K
^
(
8
*
n
+
1
)
)
A
source
theorem
Stab_subset
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(A :
Finset
α
)
{K :
ℝ
}
:
3
•
Stab
K
A
^
2
-
3
•
Stab
K
A
^
2
⊆
Stab
(
K
^
374
)
A
source
theorem
Stab_card_inc
(K :
ℝ
)
(p :
ℕ
)
[inst :
Fact
(
Nat.Prime
p
)
]
(A :
Finset
(
ZMod
p
)
)
:
↑
(
min
(
(
Stab
K
A
)
.card
^
2
)
p
)
/
2
≤
↑
(
Stab
(
K
^
374
)
A
)
.card
source
theorem
Stab_card_inc'
(K :
ℝ
)
(p :
ℕ
)
[
Fact
(
Nat.Prime
p
)
]
(A :
Finset
(
ZMod
p
)
)
(h :
4
≤
(
Stab
K
A
)
.card
)
:
min
(
↑
(
Stab
K
A
)
.card
^
(
3
/
2
)
)
(
↑
p
/
2
)
≤
↑
(
Stab
(
K
^
374
)
A
)
.card
source
theorem
Stab_card_inc_rep
(K :
ℝ
)
(p :
ℕ
)
[inst :
Fact
(
Nat.Prime
p
)
]
(A :
Finset
(
ZMod
p
)
)
(h :
4
≤
(
Stab
K
A
)
.card
)
(n :
ℕ
)
:
min
(
↑
(
Stab
K
A
)
.card
^
(
3
/
2
)
^
n
)
(
↑
p
/
2
)
≤
↑
(
Stab
(
K
^
374
^
n
)
A
)
.card
source
theorem
Stab_full'
(K :
ℝ
)
(p :
ℕ
)
[inst :
Fact
(
Nat.Prime
p
)
]
(A :
Finset
(
ZMod
p
)
)
(β :
ℝ
)
(βpos :
0
<
β
)
(h :
4
≤
(
Stab
K
A
)
.card
)
(h₂ :
↑
p
^
β
≤
↑
(
Stab
K
A
)
.card
)
:
↑
p
/
2
≤
↑
(
Stab
(
K
^
full_C₂
β
)
A
)
.card
source
theorem
Stab_full
(K :
ℝ
)
(p :
ℕ
)
[inst :
Fact
(
Nat.Prime
p
)
]
(A :
Finset
(
ZMod
p
)
)
(β :
ℝ
)
(βpos :
0
<
β
)
(h :
4
≤
(
Stab
K
A
)
.card
)
(h₂ :
↑
p
^
β
≤
↑
(
Stab
K
A
)
.card
)
:
Stab
(
K
^
full_C
β
)
A
=
Finset.univ
source
theorem
Stab_no_full
{α :
Type
u_1}
[
Field
α
]
[
Fintype
α
]
[
DecidableEq
α
]
(K :
ℝ
)
(β :
ℝ
)
(A :
Finset
α
)
(h :
↑
(
Fintype.card
α
)
^
β
≤
↑
A
.card
)
(h₂ :
↑
A
.card
≤
↑
(
Fintype.card
α
)
^
(
1
-
β
)
)
(h₃ :
K
<
↑
(
Fintype.card
α
)
^
β
/
2
)
:
Stab
K
A
≠
Finset.univ
source
theorem
Stab_small
(K :
ℝ
)
(p :
ℕ
)
[inst :
Fact
(
Nat.Prime
p
)
]
(A :
Finset
(
ZMod
p
)
)
(β :
ℝ
)
(βpos :
0
<
β
)
(h :
4
≤
(
Stab
K
A
)
.card
)
(h₂ :
↑
p
^
β
≤
↑
(
Stab
K
A
)
.card
)
(γ :
ℝ
)
(h₃ :
↑
p
^
γ
≤
↑
A
.card
)
(h₄ :
↑
A
.card
≤
↑
p
^
(
1
-
γ
)
)
:
↑
p
^
γ
/
2
≤
K
^
full_C
β