LocalValueNormality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Nonnormal preimages at a local residual endpoint, with the actual value envelope.

lemma OAI.TotientAsymptotic.local_value_normality_decay_rate line 13
lemma OAI.TotientAsymptotic.local_value_normality_decay line 50

theorem OAI.TotientAsymptotic.local_nonnormal_witness_count_rate line 57

Source documentation

The singleton-target argument controls arbitrary nonnormal preimages without any assumption on their multiplicity.

theorem local_nonnormal_witness_count_rate {A : ℝ} (hA : 0 ≤ A) (K : ℕ) :
    ∀ᶠ h : ℕ in atTop,∀ (z : ℝ) (d q : ℕ),
      256 ≤ z → 0 ≤ B z → Real.log (B z+4) ≤ A*h → 0 < d →
      ∀ (R Q : Finset ℕ) (F : ℕ → ℕ),Q ⊆ R →
      (∀ n ∈ R,∀ p : ℕ,p.Prime → p ∣ n → IsNormalPrime (localNormalityScale h) p) →
      (∀ p : ℕ,p.Prime → p ∣ q → IsNormalPrime (localNormalityScale h) p) →
      (∀ n ∈ R,(∃ m ∈ R,m≠n ∧ m.totient=n.totient) → ∃ c ∈ R,F n=c*q) →
      (∀ n ∈ Q,∃ p : ℕ,p.Prime ∧ p ∣ F n ∧ ¬IsNormalPrime (localNormalityScale h) p) →
      (∀ n ∈ Q,0<F n ∧ (F n).totient=d*n.totient ∧ ((d*n.totient:ℕ):ℝ)≤z) →
      (Q.card:ℝ) ≤ z/Real.log z*rho^(K*h) := by
…

Mentions: OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.localNormalityScale, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.rho

theorem OAI.TotientAsymptotic.local_nonnormal_witness_count line 105