OAI/NumberTheory/Ostmann/Arithmetic/MovingOneGiantDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.oneGiant_product_eq line 18

   Source documentation

   A prime in the giant range cannot be exchanged with any of the regular primes when two complete products agree.

   theorem oneGiant_product_eq {J : Type*} [Fintype J]
       (X Y : ℕ) (hX : X.Prime) (hY : Y.Prime)
       (p q : J → ℕ) (hq : ∀ i, (q i).Prime)
       (hsep : ∀ i, X ≠ q i)
       (he : X * ∏ i, p i = Y * ∏ i, q i) :
       X = Y ∧ (∏ i, p i) = ∏ i, q i := by
   …

2. theorem OAI.Ostmann.movingOneGiant_transform_product line 36

   Source documentation

   The full one-giant Fourier factor splits with its exact CRT cofactor. The regular part is expressed only by its prime product.

   theorem movingOneGiant_transform_product {J : Type*} [Fintype J]
       (X : ℕ) [Fact X.Prime] (p : J → ℕ) [∀ i, Fact (p i).Prime]
       (hp : Function.Injective p)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (D : ℕ) (v : ℤ) :
       movingRegularTransform (movingOneGiantModuli X p)
           (movingOneGiantFactors X p greg ggiant favorable) D v =
         (if favorable X then
           complexUnitPhase (ggiant X ((v : ZMod X) * ((D * ∏ i, p i : ℕ) : ZMod X)⁻¹))
          else 0) * primeProductTransform greg (D * X) (∏ i, p i) v := by
   …

   Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.movingOneGiantModuli, OAI.Ostmann.movingOneGiantFactors, OAI.Ostmann.complexUnitPhase, OAI.Ostmann.primeProductTransform

3. theorem OAI.Ostmann.movingOneGiant_pivot_diagonal_le line 65

   Source documentation

   The surviving giant is constant on every supported diagonal fibre. Its unit phase can therefore be removed after grouping; the regular prime-product transform and the original grouped coefficient remain.

   theorem movingOneGiant_pivot_diagonal_le {A J : Type*} [Fintype A] [Fintype J]
       (X : A → ℕ) [∀ a, Fact (X a).Prime]
       (p : A → J → ℕ) [∀ a i, Fact (p a i).Prime]
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (D : ℕ) (v : A → ℤ) (W : A → ℂ)
       (hinj : ∀ a, W a ≠ 0 → Function.Injective (p a))
       (hv : ∀ a, W a ≠ 0 → v a ≠ 0)
       (hvg : ∀ a, W a ≠ 0 → (v a).natAbs < X a)
       (hvr : ∀ a, W a ≠ 0 → ∀ i, (v a).natAbs < p a i)
       (hsep : ∀ a b, W a ≠ 0 → W b ≠ 0 → ∀ i, X a ≠ p b i) :
       (pivotDiagonal (fun a => X a * ∏ i, p a i) v
         (fun a => W a * movingRegularTransform (movingOneGiantModuli (X a) (p a))
   …

   Mentions: OAI.Ostmann.pivotDiagonal, OAI.Ostmann.movingRegularTransform, OAI.Ostmann.movingOneGiantModuli

4. theorem OAI.Ostmann.movingOneGiant_weighted_pivot_diagonal_le line 144

   Source documentation

   Cauchy on the identified fibre charges exactly its original prior mass. There is no extra frequency cardinality or bound on each giant factor before the diagonal has been grouped.

   theorem movingOneGiant_weighted_pivot_diagonal_le {A J : Type*} [Fintype A] [Fintype J]
       (X : A → ℕ) [∀ a, Fact (X a).Prime]
       (p : A → J → ℕ) [∀ a i, Fact (p a i).Prime]
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (D : ℕ) (v : A → ℤ) (μ : A → ℝ) (W : A → ℂ) (θ : ℕ × ℕ × ℤ → ℝ)
       (hμ : ∀ a, 0 ≤ μ a)
       (hinj : ∀ a, (μ a : ℂ) * W a ≠ 0 → Function.Injective (p a))
       (hv : ∀ a, (μ a : ℂ) * W a ≠ 0 → v a ≠ 0)
       (hvg : ∀ a, (μ a : ℂ) * W a ≠ 0 → (v a).natAbs < X a)
       (hvr : ∀ a, (μ a : ℂ) * W a ≠ 0 → ∀ i, (v a).natAbs < p a i)
       (hsep : ∀ a b, (μ a : ℂ) * W a ≠ 0 → (μ b : ℂ) * W b ≠ 0 → ∀ i, X a ≠ p b i)
       (hmass : ∀ k, (∑ a, if (X a, (∏ i, p a i), v a) = k then μ a else 0) ≤ θ k) :
   …