OAI/NumberTheory/JointDickman/Probability/SplitSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.remainingSubsetMass_eq_zero line 12
2. theorem OAI.JointDickman.no_high_changes_retained_added line 23

   Source documentation

   No high coefficient changes force all old high coefficient primes to be kept and prohibit any high additions.

   theorem no_high_changes_retained_added {A R I U : Finset ℕ} {Y : ℝ}
       (hd : Disjoint A R) (hI : I ⊆ A) (hU : U ⊆ R)
       (hno : ∀ p ∈ symmDiff A (I ∪ U), Real.log p ≤ Y) :
       highPrimePart Y I = highPrimePart Y A ∧ highPrimePart Y U = ∅ := by
   …

   Mentions: OAI.JointDickman.highPrimePart

3. theorem OAI.JointDickman.addition_product_log_large line 51

   Source documentation

   A newly added prime in the top half of the shell forces the whole addition product to have logarithm greater than Y/2.

   theorem addition_product_log_large {P A I U : Finset ℕ} {Y : ℝ}
       (hP : ∀ p ∈ P, p.Prime) (hU : U ⊆ P)
       (hadd : ∃ p ∈ (I ∪ U) \ A, Y / 2 < Real.log p) (hI : I ⊆ A) :
       Y / 2 < Real.log (∏ p ∈ U, p : ℕ) := by
   …