OAI/NumberTheory/Ostmann/Arithmetic/MovingGiantSupportedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_giant_transfer_on_prior line 13

   Source documentation

   The entire Cauchy--Schwarz, positive-integer extension and forced-pivot substitution. The inherited prime laws remain in μ and c; the integer variable has no prime-specific transform attached to it.

   theorem moving_giant_transfer_on_prior {Y A : Type*} [Fintype Y] [Fintype A]
       (P I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPI : P ⊆ I)
       (hI : ∀ p ∈ I, 0 < p)
       (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (hμmass : ∑ y, μ y = 1)
       (w : ℕ → ℝ) (hw : ∀ p ∈ I, 0 ≤ w p) (Z : ℝ) (hZ : 0 ≤ Z)
       (hmass : ∑ p : P, Z * w p / (p : ℝ) = 1)
       (U : Y → ℕ) (hU : ∀ y, 0 < U y)
       (row : ∀ y, (p : P) → Fin ((p : ℕ) * U y) → ℂ)
       (hrow : ∀ y p, (∑ t, ‖row y p t‖ ^ 2) ≤ (p : ℕ) * (U y : ℝ))
       (L : Y → A → ℕ) (v : Y → A → ℤ) (c : Y → ℕ → A → ℂ)
       (hcoprime : ∀ y p, p ∈ I → ∀ a, c y p a ≠ 0 → (L y a).Coprime (p * U y))
       (N H V : ℕ)
   …