OAI/NumberTheory/JointDickman/Amplification/NativeOrientedEvent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Domination of the actual oriented event by the conditional operator

  1. def OAI.JointDickman.nativeOrientedEvent line 11
  2. def OAI.JointDickman.nativeOrientedMass line 21
  3. theorem OAI.JointDickman.nativeOrientedMass_le line 27

    Source documentation

    The native event forces all four high-prime restrictions and the exact low-prime ratio test. Its two regular remaining sets supply the tail counts.

    theorem nativeOrientedMass_le {B L T i : ℕ} {τ C : ℝ} {A D : Finset ℕ}
    (hB : 0 < B) (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B) :
    nativeOrientedMass B L T τ C (primeTailEndpoint B i) A D ≤
      orientedSplitMass B A D (primeTailEndpoint B i) C T := by
…

    Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.nativeOrientedMass, OAI.JointDickman.primeTailEndpoint, OAI.JointDickman.orientedSplitMass