OAI/NumberTheory/Ostmann/Arithmetic/MovingHarmonicDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingOneGiant_harmonic_diagonal_le line 14

   Source documentation

   Distinctness is forced by the coefficient, rather than imposed on the sampling law. The harmonic fibre estimate therefore applies without changing either the original diagonal or its single-branch energy.

   theorem movingOneGiant_harmonic_diagonal_le {A I : Type*} [Fintype A] [Fintype I]
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : I → Finset ℕ)
       (X : A → ℕ) (hX : ∀ a, (X a).Prime)
       (y : A → I → P) (v : A → ℤ) (μ : A → ℝ) (W : A → ℂ)
       (hμ : ∀ a, 0 ≤ μ a) (g : ℕ → ℝ) (hg : ∀ q, 0 ≤ g q)
       (hrow : ∀ a b, X a = X b → y a = y b → v a = v b → a = b)
       (hpoint : ∀ a, μ a ≤ g (X a) * ∏ i, primeSubsetPrior P (Q i) (y a i))
       (hinj : ∀ a, (μ a : ℂ) * W a ≠ 0 → Function.Injective (y 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 < (y a i : ℕ))
       (hsep : ∀ a b, (μ a : ℂ) * W a ≠ 0 → (μ b : ℂ) * W b ≠ 0 →
   …

   Mentions: OAI.Ostmann.primeSubsetPrior