OAI/NumberTheory/Ostmann/Characters/PivotArithmeticTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.positivePivotKey line 13

   Source documentation

   Coefficients include their positive-integer support, so the impossible zero-modulus case has an empty coefficient family.

   noncomputable def positivePivotKey {A : ℕ → Type*}
       (hpos : ∀ M, A M → 0 < M) (L : ∀ M, A M → ℕ) (v : ∀ M, A M → ℤ)
       (M : ℕ) (a : A M) : Fin M := by
   …

2. theorem OAI.Ostmann.positivePivotKey_eq_iff line 19
3. theorem OAI.Ostmann.pivot_square_split_of_key line 27
4. theorem OAI.Ostmann.pivot_arithmetic_transfer_real line 59

   Source documentation

   Both Cauchy steps and the prime-to-integer extension are already included. The off-diagonal here is the exact complex expanded sum, not a majorant.

   theorem pivot_arithmetic_transfer_real {A : ℕ → Type*} [∀ M, Fintype (A M)]
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       {n : ℕ} (Q : Fin n → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
       (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
       (S : Finset (Fin n → P)) (hS : ∀ x ∈ S, Function.Injective x)
       (T : Finset ℕ) (hT : ∀ x ∈ S, (∏ i, (x i : ℕ)) ∈ T)
       (row : ∀ x : Fin n → P, Fin (∏ i, (x i : ℕ)) → ℂ)
       (hrow : ∀ x ∈ S, ∀ u, ‖row x u‖ ≤ 1)
       (hpos : ∀ M, A M → 0 < M) (L : ∀ M, A M → ℕ) (v : ∀ M, A M → ℤ)
       (hL : ∀ M, ∀ a : A M, (L M a).Coprime M) (c : ∀ M, A M → ℂ) :
       ‖∑ x ∈ S, (productPrior (fun i => primeSubsetPrior P (Q i)) x : ℂ) *
         ∑ a, row x (positivePivotKey hpos L v (∏ i, (x i : ℕ)) a) *
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.positivePivotKey

5. theorem OAI.Ostmann.pivot_arithmetic_transfer line 87

   Source documentation

   Both Cauchy steps and the prime-to-integer extension are already included. The off-diagonal here is the exact complex expanded sum, not a majorant.

   theorem pivot_arithmetic_transfer {A : ℕ → Type*} [∀ M, Fintype (A M)]
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       {n : ℕ} (Q : Fin n → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
       (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
       (S : Finset (Fin n → P)) (hS : ∀ x ∈ S, Function.Injective x)
       (T : Finset ℕ) (hT : ∀ x ∈ S, (∏ i, (x i : ℕ)) ∈ T)
       (row : ∀ x : Fin n → P, Fin (∏ i, (x i : ℕ)) → ℂ)
       (hrow : ∀ x ∈ S, ∀ u, ‖row x u‖ ≤ 1)
       (hpos : ∀ M, A M → 0 < M) (L : ∀ M, A M → ℕ) (v : ∀ M, A M → ℤ)
       (hL : ∀ M, ∀ a : A M, (L M a).Coprime M) (c : ∀ M, A M → ℂ) :
       ‖∑ x ∈ S, (productPrior (fun i => primeSubsetPrior P (Q i)) x : ℂ) *
         ∑ a, row x (positivePivotKey hpos L v (∏ i, (x i : ℕ)) a) *
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.positivePivotKey