OAI/NumberTheory/Ostmann/Arithmetic/BulkKernelCellComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.bulk_kernel_cells_joint_comparison line 14

   Source documentation

   The full original conjugate pair, including its sharp support conditions, is compared jointly, retaining every Page correction. The only mass side condition is a finite reciprocal-prime sum.

   theorem PublishedProgressionInput.bulk_kernel_cells_joint_comparison
       (P : PublishedProgressionInput) {σ C : Type*} [Fintype σ] [Fintype C]
       (base : σ → ℝ) (childBound pivotBound : ℕ → ℕ) (order : List σ) (horder : order.Nodup)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (hT : ∀ b i, i ∈ order → (T b).CompensationAbsent i)
       (i₀ : σ) (hi₀ : i₀ ∈ order) (ψ : 𝓢(ℝ, ℂ)) (X lo hi V : ℝ)
       (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (hV : ∀ b, (T b).Frequencies (fun s => |(s : ℝ)| ≤ V))
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0)
       (d r : ℕ) (hsize : ∀ b, (T b).SizeLE d) (hregular : ∀ b, (T b).RegularLengthLE r) (L R : ℝ)
       (Q : ℕ) (hQ : 2 ≤ Q) (q a : σ → C → ℕ) (u v : σ → C → ℝ) (Z : σ → ℝ) (hZ : ∀ i, 0 ≤ Z i)
       (hu : ∀ i c, 1 ≤ u i c) (hq : ∀ i ∈ order, ∀ c, 1 ≤ q i c)
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MovingSlotData