CandidateAdditionClasses.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Covering the actual candidate representations by addition classes

theorem OAI.JointDickman.endpoint_box_exp_bound line 13

theorem OAI.JointDickman.candidatePairRepresentations_addition_cover line 31

Source documentation

Each actual representation is either small at both endpoints, or is in a later grid class with a large addition at one of its endpoints.

theorem candidatePairRepresentations_addition_cover
    {B L T H M : ℕ} {τ C : ℝ} (hB : 5 ≤ B) (hL : 3 ≤ L)
    (hT : (T : ℝ) ≤ Real.exp B) (i t : Fin M) (A D U V : Finset ℕ)
    (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B)
    (hU : U ⊆ auxiliaryPrimes B) (hV : V ⊆ auxiliaryPrimes B)
    {ab : Finset ℕ × Finset ℕ}
    (hab : ab ∈ candidatePairRepresentations B L T H τ C i t (A ∪ U) (D ∪ V)) :
    ab ∈ smallCandidateAlternatives B L T H τ C i t A D U V ∨
      ∃ k ∈ Icc 4 L,
        ab ∈ allLargeLowAlternativePairs B L k (t.val-i.val) τ C (1/(L : ℝ)) A U D V ∨
        ab.swap ∈ allLargeHighAlternativePairs B L k (t.val-i.val) τ C (1/(L : ℝ)) D V A U := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.candidatePairRepresentations, OAI.JointDickman.smallCandidateAlternatives, OAI.JointDickman.allLargeLowAlternativePairs, OAI.JointDickman.allLargeHighAlternativePairs

theorem OAI.JointDickman.candidatePairRepresentations_card_le_addition_classes line 79

Source documentation

A finite cardinal bound retaining every representation and both endpoint orientations. No uniqueness of a coefficient pair is assumed.

theorem candidatePairRepresentations_card_le_addition_classes
    {B L T H M : ℕ} {τ C : ℝ} (hB : 5 ≤ B) (hL : 3 ≤ L)
    (hT : (T : ℝ) ≤ Real.exp B) (i t : Fin M) (A D U V : Finset ℕ)
    (hA : A ⊆ auxiliaryPrimes B) (hD : D ⊆ auxiliaryPrimes B)
    (hU : U ⊆ auxiliaryPrimes B) (hV : V ⊆ auxiliaryPrimes B) :
    (candidatePairRepresentations B L T H τ C i t (A ∪ U) (D ∪ V)).card ≤
      (smallCandidateAlternatives B L T H τ C i t A D U V).card +
      ∑ k ∈ Icc 4 L,
        ((allLargeLowAlternativePairs B L k (t.val-i.val) τ C (1/(L : ℝ)) A U D V).card +
         (allLargeHighAlternativePairs B L k (t.val-i.val) τ C (1/(L : ℝ)) D V A U).card) := by
…