OAI/NumberTheory/Ostmann/Arithmetic/FiniteArithmeticIteration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduled_constituent_interval_step_finite line 9
2. theorem OAI.Ostmann.scheduled_constituent_iteration_finite line 54

   Source documentation

   The initial reserve survives every actual arithmetic step once the explicit diagonals and the sum of the actual losses have been bounded.

   theorem scheduled_constituent_iteration_finite {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ)
       (χ : (Σ i, Fin (size i)) → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : (Σ i, Fin (size i)) → ℕ → ℂ) (pivot : ℕ → (Σ i, Fin (size i)))
       (k : ℕ) (hpivot : ∀ j < k, role (pivot j).1 = .pivot j) (p : ℕ → I)
       (hp : ∀ j < k, role (p j) = .pivot j)
       (hu : ∀ j < k, ∀ i, role i = .pivot j → i = p j)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (hκ : ∀ i q, q ∈ P → ‖κ i q‖ ≤ 1)
       (hQP : ∀ i, Q i ⊆ P) (hQ : ∀ i, (∑ q ∈ Q i, (q : ℝ)⁻¹) ≠ 0)
       (lo hi : I → ℕ) (cellLo cellHi : (Σ i, Fin (size i)) → ℕ)
       (hcell : ∀ i q, q ∈ Q i → cellLo i ≤ q ∧ q ≤ cellHi i)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole