ThreePrimeLocalDensity.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.threePrimeNonzeroResidues line 12
Source documentation
Nonzero residue classes modulo p. For prime p, these are exactly its unit classes.
```
def threePrimeNonzeroResidues (p : ℕ) [NeZero p] : Finset (ZMod p) :=
…
```
def OAI.Problem337.threePrimeLocalPairs line 17
Source documentation
Two-coordinate parametrization of nonzero residue triples with sum u: the third coordinate is u - x - y.
```
def threePrimeLocalPairs (p : ℕ) [NeZero p] (u : ZMod p) :
    Finset (ZMod p × ZMod p) :=
…
```
lemma OAI.Problem337.mem_threePrimeLocalPairs line 22
lemma OAI.Problem337.threePrimeLocalBadPairs_eq_image line 41
lemma OAI.Problem337.threePrimeNonzeroResidues_card line 65
theorem OAI.Problem337.threePrimeLocalPairs_card_balance line 71
Source documentation
Removing the forbidden third-coordinate-zero pairs leaves this exact cardinality balance. This identity uses only the additive residue group.
```
theorem threePrimeLocalPairs_card_balance (p : ℕ) [NeZero p] (u : ZMod p) :
    (threePrimeLocalPairs p u).card +
      ((threePrimeNonzeroResidues p).erase u).card = (p - 1) ^ 2 := by
…
```
Mentions: OAI.Problem337.threePrimeLocalPairs, OAI.Problem337.threePrimeNonzeroResidues

theorem OAI.Problem337.threePrimeLocalPairs_card line 87

Source documentation

Exact count of the local nonzero solutions to a three-term sum.

theorem threePrimeLocalPairs_card (p : ℕ) [NeZero p] (hp : 2 ≤ p)
    (u : ZMod p) :
    (threePrimeLocalPairs p u).card =
      if u = 0 then (p - 1) * (p - 2) else (p - 1) * (p - 2) + 1 := by
…

Mentions: OAI.Problem337.threePrimeLocalPairs

theorem OAI.Problem337.threePrimeLocalPairs_card_real line 109

Source documentation

Polynomial form of the local solution count.

theorem threePrimeLocalPairs_card_real (p : ℕ) [NeZero p] (hp : 2 ≤ p)
    (u : ZMod p) :
    ((threePrimeLocalPairs p u).card : ℝ) =
      (p : ℝ) ^ 2 - 3 * p + 3 - if u = 0 then 1 else 0 := by
…

Mentions: OAI.Problem337.threePrimeLocalPairs

def OAI.Problem337.threePrimeLocalFactor line 119
Source documentation
The local density relative to the heuristic density of three unit classes. The prime hypothesis is used when identifying this with a singular-series factor; the finite expression is defined for every nonzero modulus.
```
def threePrimeLocalFactor (p : ℕ) [NeZero p] (u : ZMod p) : ℝ :=
…
```

theorem OAI.Problem337.threePrimeLocalFactor_eq line 123

Source documentation

The exact local factor of the ternary prime singular series.

theorem threePrimeLocalFactor_eq (p : ℕ) [NeZero p] (hp : 2 ≤ p)
    (u : ZMod p) :
    threePrimeLocalFactor p u =
      if u = 0 then 1 - 1 / ((p : ℝ) - 1) ^ 2
      else 1 + 1 / ((p : ℝ) - 1) ^ 3 := by
…

Mentions: OAI.Problem337.threePrimeLocalFactor

theorem OAI.Problem337.threePrimeLocalFactor_natCast line 134

Source documentation

The natural-number formulation distinguishes primes dividing the target.

theorem threePrimeLocalFactor_natCast (p u : ℕ) [NeZero p] (hp : 2 ≤ p) :
    threePrimeLocalFactor p (u : ZMod p) =
      if p ∣ u then 1 - 1 / ((p : ℝ) - 1) ^ 2
      else 1 + 1 / ((p : ℝ) - 1) ^ 3 := by
…

Mentions: OAI.Problem337.threePrimeLocalFactor

theorem OAI.Problem337.threePrimeLocalFactor_two line 142
Source documentation
An odd target has the positive factor two at the prime two.
```
theorem threePrimeLocalFactor_two (u : ℕ) (hu : Odd u) :
    threePrimeLocalFactor 2 (u : ZMod 2) = 2 := by
…
```
Mentions: OAI.Problem337.threePrimeLocalFactor
def OAI.Problem337.threePrimeLocalTriples line 151
Source documentation
The literal ordered triples underlying the local density.
```
def threePrimeLocalTriples (p : ℕ) [NeZero p] (u : ZMod p) :
    Finset (ZMod p × ZMod p × ZMod p) :=
…
```
theorem OAI.Problem337.threePrimeLocalTriples_eq_image line 157
Source documentation
The third residue is uniquely determined by the first two.
```
theorem threePrimeLocalTriples_eq_image (p : ℕ) [NeZero p] (u : ZMod p) :
    threePrimeLocalTriples p u =
      (threePrimeLocalPairs p u).image (fun t => (t.1, t.2, u - t.1 - t.2)) := by
…
```
Mentions: OAI.Problem337.threePrimeLocalTriples, OAI.Problem337.threePrimeLocalPairs
theorem OAI.Problem337.threePrimeLocalTriples_card line 179
Source documentation
The two-coordinate parametrization does not change the local count.
```
theorem threePrimeLocalTriples_card (p : ℕ) [NeZero p] (u : ZMod p) :
    (threePrimeLocalTriples p u).card = (threePrimeLocalPairs p u).card := by
…
```
Mentions: OAI.Problem337.threePrimeLocalTriples, OAI.Problem337.threePrimeLocalPairs

theorem OAI.Problem337.mem_threePrimeLocalTriples_iff_units line 190

Source documentation

For a prime modulus, the nonzero residue condition is exactly the unit condition used in the prime singular series.

theorem mem_threePrimeLocalTriples_iff_units (p : ℕ) [Fact p.Prime]
    (u : ZMod p) (t : ZMod p × ZMod p × ZMod p) :
    t ∈ threePrimeLocalTriples p u ↔
      IsUnit t.1 ∧ IsUnit t.2.1 ∧ IsUnit t.2.2 ∧ t.1 + t.2.1 + t.2.2 = u := by
…

Mentions: OAI.Problem337.threePrimeLocalTriples

theorem OAI.Problem337.threePrimeLocalPairs_card_pos line 198
Source documentation
There is no local obstruction at a modulus of at least three when only nonzero residue classes are required.
```
theorem threePrimeLocalPairs_card_pos (p : ℕ) [NeZero p] (hp : 3 ≤ p)
    (u : ZMod p) : 0 < (threePrimeLocalPairs p u).card := by
…
```
Mentions: OAI.Problem337.threePrimeLocalPairs
theorem OAI.Problem337.threePrimeLocalFactor_pos_of_three_le line 206
Source documentation
In particular every odd-prime local density is strictly positive.
```
theorem threePrimeLocalFactor_pos_of_three_le (p : ℕ) [NeZero p]
    (hp : 3 ≤ p) (u : ZMod p) : 0 < threePrimeLocalFactor p u := by
…
```
Mentions: OAI.Problem337.threePrimeLocalFactor
theorem OAI.Problem337.threePrimeLocalTriples_nonempty_iff line 215
Source documentation
The only nonzero-residue ternary-sum obstruction is zero modulo two.
```
theorem threePrimeLocalTriples_nonempty_iff (p : ℕ) [NeZero p]
    (hp : 2 ≤ p) (u : ZMod p) :
    (threePrimeLocalTriples p u).Nonempty ↔ p ≠ 2 ∨ u ≠ 0 := by
…
```
Mentions: OAI.Problem337.threePrimeLocalTriples
theorem OAI.Problem337.threePrimeLocalFactor_pos line 227
Source documentation
Every prime local factor is positive for odd natural targets.
```
theorem threePrimeLocalFactor_pos (p u : ℕ) [Fact p.Prime] (hu : Odd u) :
    0 < threePrimeLocalFactor p (u : ZMod p) := by
…
```
Mentions: OAI.Problem337.threePrimeLocalFactor
theorem OAI.Problem337.threePrimeLocalSolubility_iff_odd line 239
Source documentation
Oddness is exactly the local-solubility condition for a sum of three unit residue classes at every prime. This is only a local statement, not a theorem that those residue classes lift simultaneously to three prime integers.
```
theorem threePrimeLocalSolubility_iff_odd (u : ℕ) :
    (∀ p : ℕ, p.Prime → ∃ x y z : ZMod p,
      IsUnit x ∧ IsUnit y ∧ IsUnit z ∧ x + y + z = (u : ZMod p)) ↔ Odd u := by
…
```
lemma OAI.Problem337.sum_zmod_zero_other line 260
theorem OAI.Problem337.sum_threePrimeLocalFactor line 276
Source documentation
The normalized local solution density has exact average one.
```
theorem sum_threePrimeLocalFactor (p : ℕ) [NeZero p] (hp : 2 ≤ p) :
    (∑ u : ZMod p, threePrimeLocalFactor p u) = (p : ℝ) := by
…
```
Mentions: OAI.Problem337.threePrimeLocalFactor
theorem OAI.Problem337.sum_threePrimeLocalFactor_centered_sq line 287
Source documentation
Exact local variance of the ternary density: after dividing by the number of residues, it is (p - 1)⁻⁵.
```
theorem sum_threePrimeLocalFactor_centered_sq (p : ℕ) [NeZero p] (hp : 2 ≤ p) :
    (∑ u : ZMod p, (threePrimeLocalFactor p u - 1) ^ 2) =
      (p : ℝ) / ((p : ℝ) - 1) ^ 5 := by
…
```
Mentions: OAI.Problem337.threePrimeLocalFactor
theorem OAI.Problem337.sum_threePrimeLocalFactor_sq line 303
Source documentation
The exact uncentered second moment, useful with the independent CRT multiplicativity of local densities.
```
theorem sum_threePrimeLocalFactor_sq (p : ℕ) [NeZero p] (hp : 2 ≤ p) :
    (∑ u : ZMod p, (threePrimeLocalFactor p u) ^ 2) =
      (p : ℝ) * (1 + 1 / ((p : ℝ) - 1) ^ 5) := by
…
```
Mentions: OAI.Problem337.threePrimeLocalFactor