OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternObservableCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual observable and its uniform pointwise arithmetic cost

  1. theorem OAI.Ostmann.movingPatternPrimeObservable_norm line 38
  2. theorem OAI.Ostmann.movingPattern_pointwise_cost line 73

    Source documentation

    The full pointwise cost from the actual observable is uniform over patterns and prime assignments at fixed depth.

    theorem movingPattern_pointwise_cost (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A lo hi B D F : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) (hF : 0 ≤ F) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ L : ℝ, 1 ≤ L → let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.spectatorBulkCount