PrimeFactorPairs.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact primary factor-pair reindexing for a literal squarefree term. The norm ball only makes the right-hand support finite.

theorem OAI.CubicFirstMoment.squarefree_primary_factor_pairs line 15

Source documentation

Every subset of the actual prime factors gives one, and only one, primary factor pair. This retains arbitrary weights on both factors.

theorem squarefree_primary_factor_pairs {n : Eisenstein} (hn : primary n)
    (hs : Squarefree n) {B : ℝ} (hnB : norm n ≤ B)
    (K : Eisenstein → Eisenstein → ℂ) :
    (∑ s ∈ (primaryPrimeFactors n).powerset,
      K (∏ p ∈ s, p) (∏ p ∈ primaryPrimeFactors n \ s, p)) =
    ∑ q ∈ ((primaryElementBall B).product (primaryElementBall B)).filter
        (fun q => q.1*q.2 = n), K q.1 q.2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.primaryElementBall

theorem OAI.CubicFirstMoment.primary_pair_fiber_support line 93

Source documentation

Arbitrary original support remains an exact product-support test after collecting finite primary factor fibres.

theorem primary_pair_fiber_support (S : Finset Eisenstein) (B : ℝ)
    (K : Eisenstein → Eisenstein → ℂ) :
    (∑ n ∈ S,
      ∑ q ∈ ((primaryElementBall B).product (primaryElementBall B)).filter
        (fun q => q.1*q.2 = n), K q.1 q.2) =
    ∑ d ∈ primaryElementBall B, ∑ e ∈ primaryElementBall B,
      if d*e ∈ S then K d e else 0 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall

theorem OAI.CubicFirstMoment.primary_pair_fiber_cutoff line 105

Source documentation

The product cutoff is retained literally when the finite product fibres are collected. No condition on the pair weight is required.

theorem primary_pair_fiber_cutoff (B : ℝ) (K : Eisenstein → Eisenstein → ℂ) :
    (∑ n ∈ primaryElementBall B,
      ∑ q ∈ ((primaryElementBall B).product (primaryElementBall B)).filter
        (fun q => q.1*q.2 = n), K q.1 q.2) =
    ∑ d ∈ primaryElementBall B, ∑ e ∈ primaryElementBall B,
      if norm (d*e) ≤ B then K d e else 0 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.squarefree_primary_subset_cutoff_sum line 123
Source documentation
Full finite reindexing of (m, subset of its prime factors) into independent primary factor pairs. Squarefree support and the sharp product cutoff remain explicit on the right-hand side.
```
theorem squarefree_primary_subset_cutoff_sum (B : ℝ)
    (K : Eisenstein → Eisenstein → ℂ) :
    (∑ n ∈ (primaryElementBall B).filter Squarefree,
      ∑ s ∈ (primaryPrimeFactors n).powerset,
        K (∏ p ∈ s, p) (∏ p ∈ primaryPrimeFactors n \ s, p)) =
    ∑ d ∈ primaryElementBall B, ∑ e ∈ primaryElementBall B,
      if Squarefree (d*e) ∧ norm (d*e) ≤ B then K d e else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.norm