OAI/NumberTheory/Ostmann/Arithmetic/IntervalArithmeticStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.constituentPrimeGuardedAmplitude_interval_step line 14

   Source documentation

   The integer-pivot support, inherited interval tests and branch product bounds follow from the original cell endpoints.

   theorem constituentPrimeGuardedAmplitude_interval_step {I D : Type*} [Fintype I] [Fintype D]
       (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)
       (n : ℕ) (p : I) (hp : role p = .pivot n) (hu : ∀ i, role i = .pivot n → 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)
       (childBound pivotBound : ℕ → ℕ) (leaf : ScheduleAtomState role → ℤ → ℂ)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomState