OAI/NumberTheory/JointDickman/Probability/SplitChangeEvents.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.twoSiteChangeSet line 12
2. def OAI.JointDickman.twoSiteNoChange line 15
3. def OAI.JointDickman.twoSiteNoHighChange line 18
4. def OAI.JointDickman.twoSiteAddition line 21
5. theorem OAI.JointDickman.twoSiteChangeSet_subset line 25
6. theorem OAI.JointDickman.twoSiteChangeSet_eq_empty line 35
7. theorem OAI.JointDickman.twoSiteChangeSet_swap line 39
8. theorem OAI.JointDickman.twoSiteNoHighChange_swap line 43
9. theorem OAI.JointDickman.twoSite_change_orientations line 50

   Source documentation

   At the largest changed prime, at least one orientation is an addition at one of the two sites.

   theorem twoSite_change_orientations {P : Finset ℕ} (x : TwoSiteSplit P) {p : ℕ} {Y : ℝ}
       (hp : p ∈ twoSiteChangeSet x) (hY : Y / 2 < Real.log p) :
       twoSiteAddition x Y false ∨ twoSiteAddition x Y true ∨
         twoSiteAddition x.swap Y false ∨ twoSiteAddition x.swap Y true := by
   …

   Mentions: OAI.JointDickman.TwoSiteSplit, OAI.JointDickman.twoSiteChangeSet, OAI.JointDickman.twoSiteAddition

10. theorem OAI.JointDickman.largest_changed_prime_shell line 64

    Source documentation

    Every nontrivial change belongs to a single covered dyadic interval; the prime at its top gives one of the four addition orientations.

    theorem largest_changed_prime_shell {B N : ℕ}
        (hB : 1 < B) (hcap : 4 * (B : ℝ) ≤ (2 : ℝ)^N * Real.log (auxiliaryCutoff B))
        (x : TwoSiteSplit (auxiliaryPrimes B)) (hx : ¬ twoSiteNoChange x) :
        ∃ i ∈ Icc 1 N, twoSiteNoHighChange x (primeTailEndpoint B i) ∧
          (twoSiteAddition x (primeTailEndpoint B i) false ∨ twoSiteAddition x (primeTailEndpoint B i) true ∨
            twoSiteAddition x.swap (primeTailEndpoint B i) false ∨ twoSiteAddition x.swap (primeTailEndpoint B i) true) := by
    …

    Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.TwoSiteSplit, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.twoSiteNoChange, OAI.JointDickman.twoSiteNoHighChange, OAI.JointDickman.primeTailEndpoint, OAI.JointDickman.twoSiteAddition