OAI/NumberTheory/Ostmann/Arithmetic/MovingSpectatorCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Pointwise cost of the actual normalized spectator transforms

  1. theorem OAI.Ostmann.normalizedResidueTransform_norm_le_sqrt line 11
  2. theorem OAI.Ostmann.normalizedResidueTransform_norm_le_prime line 22
  3. theorem OAI.Ostmann.moving_spectator_product_cost line 31

    Source documentation

    A common prime upper bound controls all actual pointwise spectator factors. This cost is retained in the cell error, separate from signed gain.

    theorem moving_spectator_product_cost (n m : ℕ) (p : Fin m → ℕ)
    (V : ℝ) (hp : ∀ i, (p i : ℝ) ≤ Real.exp V) :
    (∏ i, (p i : ℝ) ^ (2 ^ (n + 1))) ≤
      Real.exp ((2 ^ (n + 1) : ℕ) * (m : ℝ) * V) := by
…
  4. theorem OAI.Ostmann.moving_spectator_linear_cost line 47
  5. theorem OAI.Ostmann.moving_frozen_residue_coefficient_norm line 70