OAI/NumberTheory/Ostmann/ZeroDensity/FinitePriorDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Absorbing a dominated finite sampling law into a complex multiplier

  1. def OAI.Ostmann.finitePriorDensity line 11
  2. theorem OAI.Ostmann.finitePriorDensity_cancel line 16

    Source documentation

    The scalar is the retained product of one-over-prime line probabilities. It is positive, so a zero dominating prior forces the original summand to vanish.

    theorem finitePriorDensity_cancel {X : Type*} (μ : X → ℝ) (F : X → ℂ)
    (c : X → ℝ) (B : ℝ) (hc : ∀ x, 0 < c x)
    (hbound : ∀ x, ‖F x‖ * c x ≤ B * μ x) (x : X) :
    (μ x : ℂ) * finitePriorDensity μ F x = F x := by
…

    Mentions: OAI.Ostmann.finitePriorDensity

  3. theorem OAI.Ostmann.finitePriorDensity_bound line 31
  4. theorem OAI.Ostmann.finitePriorDensity_ne_zero line 43