PivotIntegerTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Extending an internally distinct pivot total to all integers

theorem OAI.Ostmann.pivot_integer_transfer line 14

Source documentation

The row can depend on the entire pivot tuple. Its coefficient depends only on the total, so no character on the extended integer is introduced.

theorem pivot_integer_transfer (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)
    (B : ∀ M : ℕ, Fin M → ℂ) :
    ‖∑ x ∈ S, (productPrior (fun i => primeSubsetPrior P (Q i)) x : ℂ) *
        ∑ u, row x u * B (∏ i, (x i : ℕ)) u‖ ^ 2 ≤
      ((n.factorial : ℝ) * ∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) *
        ∑ M ∈ T, ∑ u, ‖B M u‖ ^ 2 := by
…

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