OAI/NumberTheory/Ostmann/Construction/ScheduledArithmeticIteration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledConstituentAmplitude line 12
2. def OAI.Ostmann.scheduledConstituentDiagonal line 22
3. theorem OAI.Ostmann.scheduled_constituent_interval_step line 37

   Source documentation

   The exact natural cutoffs and prime-cell endpoints imply the next step for the actual scheduled amplitude, with its original diagonal intact.

   theorem scheduled_constituent_interval_step {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)))
       (hpivot : ∀ k, role (pivot k).1 = .pivot k)
       (j : ℕ) (p : I) (hp : role p = .pivot j) (hu : ∀ i, role i = .pivot j → i = p)
       (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)
       (V pivotBound : ℕ → ℕ) (hV : Monotone V)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole

4. theorem OAI.Ostmann.scheduled_constituent_iteration line 83

   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 {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)))
       (hpivot : ∀ j, role (pivot j).1 = .pivot j)
       (k : ℕ) (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)) → ℕ)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole