Decomposition.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact coefficient separation

Finite-set versions of the two algebraic identities used in the prime-decomposition section of An unconditional first moment for cubic Gauss sums (25 September 2026): the distinguished-factor expansion and the normalization at the stopping bin. Elements of s label distinct prime ideals, including conjugate ideals of equal norm. Thus no identification of factors with their norms is made.

theorem OAI.CubicFirstMoment.distinguished_factor_expansion line 23

Source documentation

Expanding the difference of two prime cutoffs independently at every factor. This is the unordered-subset form of eq:distinguished-tuples.

theorem distinguished_factor_expansion {α : Type*} [DecidableEq α] (s : Finset α)
    (small large : α → ℂ) :
    (∏ p ∈ s, (1 - large p)) =
      ∑ t ∈ s.powerset,
        (∏ p ∈ t, (small p - large p)) * ∏ p ∈ s \ t, (1 - small p) := by
…

theorem OAI.CubicFirstMoment.distinguished_factor_expansion_by_card line 36

Source documentation

The same expansion collected by the number of distinguished factors.

theorem distinguished_factor_expansion_by_card {α : Type*} [DecidableEq α] (s : Finset α)
    (small large : α → ℂ) :
    (∏ p ∈ s, (1 - large p)) =
      ∑ k ∈ Finset.range (s.card + 1), ∑ t ∈ s.powersetCard k,
        (∏ p ∈ t, (small p - large p)) * ∏ p ∈ s \ t, (1 - small p) := by
…

theorem OAI.CubicFirstMoment.rough_factor_expansion line 45

Source documentation

A squarefree Möbius expansion, with factors labelled before taking their product. This gives eq:rough-mobius-expansion.

theorem rough_factor_expansion {α : Type*} (s : Finset α) (cutoff : α → ℂ) :
    (∏ p ∈ s, (1 - cutoff p)) =
      ∑ t ∈ s.powerset, (-1 : ℂ) ^ t.card * ∏ p ∈ t, cutoff p := by
…

theorem OAI.CubicFirstMoment.stopping_coefficient_split line 53

Source documentation

Each choice at a fixed stopping bin has the same multiplicative coefficient, since its selected and unselected factors partition the bin.

theorem stopping_coefficient_split {α : Type*} [DecidableEq α]
    (s t : Finset α) (ht : t ⊆ s) (weight : α → ℂ) :
    (∏ p ∈ t, weight p) * (∏ p ∈ s \ t, weight p) =
      ∏ p ∈ s, weight p := by
…

theorem OAI.CubicFirstMoment.stopping_binomial_ne_zero line 62
Source documentation
The reciprocal binomial coefficient is well-defined for every possible count in the final bin.
```
theorem stopping_binomial_ne_zero (n k : ℕ) (hk : k ≤ n) :
    (n.choose k : ℂ) ≠ 0 := by
…
```
theorem OAI.CubicFirstMoment.stopping_bin_weights_sum line 68
Source documentation
The weights assigned to all possible selections in the stopping bin sum to one. This is precisely the scalar in eq:stopping-scalar.
```
theorem stopping_bin_weights_sum {α : Type*} (s : Finset α)
    (k : ℕ) (hk : k ≤ s.card) :
    (∑ _t ∈ s.powersetCard k, (s.card.choose k : ℂ)⁻¹) = 1 := by
…
```

theorem OAI.CubicFirstMoment.stopping_bin_coefficient_identity line 77

Source documentation

Distributing a squarefree coefficient over all choices in the final bin and dividing by their count restores the original coefficient exactly. This is valid for arbitrary complex prime weights, without estimates.

theorem stopping_bin_coefficient_identity {α : Type*} [DecidableEq α]
    (s : Finset α) (k : ℕ) (hk : k ≤ s.card) (weight : α → ℂ) :
    (∑ t ∈ s.powersetCard k,
      (s.card.choose k : ℂ)⁻¹ *
        ((∏ p ∈ t, weight p) * ∏ p ∈ s \ t, weight p)) =
      ∏ p ∈ s, weight p := by
…

theorem OAI.CubicFirstMoment.stopping_crossing_independent line 95

Source documentation

The crossing test only uses the common bin endpoint and the selected count, so it is identical for every selection having that count.

theorem stopping_crossing_independent {α : Type*} (s : Finset α) (k : ℕ)
    (r ell threshold : ℝ) (t : Finset α) (ht : t ∈ s.powersetCard k) :
    (r * ell ^ t.card / ell < threshold ∧ threshold ≤ r * ell ^ t.card) ↔
      (r * ell ^ k / ell < threshold ∧ threshold ≤ r * ell ^ k) := by
…