OAI/NumberTheory/JointDickman/Arithmetic/PrimeRangeOperators.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.subsetAverage line 11
2. def OAI.JointDickman.keptHighAverage line 15
3. def OAI.JointDickman.noHighAdditionAverage line 20
4. theorem OAI.JointDickman.keptHighAverage_eq line 26
5. theorem OAI.JointDickman.noHighAdditionAverage_eq line 30
6. theorem OAI.JointDickman.subsetAverage_const_mul line 35
7. theorem OAI.JointDickman.subsetAverage_le_const line 43
8. theorem OAI.JointDickman.highNoAdditionMass_nonneg line 52
9. theorem OAI.JointDickman.keptHighAverage_pair_bound line 65

   Source documentation

   Keeping both coefficients' high parts is averaged only after a uniform bound for the two low coefficient choices has been established.

   theorem keptHighAverage_pair_bound (P Q R S : Finset ℕ) (hPQ : Disjoint P Q)
       (hRS : Disjoint R S) (F : Finset ℕ → Finset ℕ → ℝ) (K : ℝ)
       (hF : ∀ A ⊆ P, ∀ D ⊆ R, F A D ≤ K) :
       keptHighAverage P Q (fun A => keptHighAverage R S (F A)) ≤
         (1 / 2 : ℝ)^Q.card * (1 / 2 : ℝ)^S.card * K := by
   …

   Mentions: OAI.JointDickman.keptHighAverage

10. theorem OAI.JointDickman.noHighAdditionAverage_pair_eq line 82

    Source documentation

    The two remaining processes factor into the high no-change mass and exactly their two independent low addition laws.

    theorem noHighAdditionAverage_pair_eq (P Q : Finset ℕ) (hd : Disjoint P Q)
        (q r : ℕ → ℝ) (k : ℝ) (F : Finset ℕ → Finset ℕ → ℝ) :
        noHighAdditionAverage P Q r k (fun V => noHighAdditionAverage P Q q k (fun U => F U V)) =
          highNoAdditionMass Q r k * highNoAdditionMass Q q k *
            subsetAverage P (fun p => r p / 2) (fun V => subsetAverage P (fun p => q p / 2) (fun U => F U V)) := by
    …

    Mentions: OAI.JointDickman.noHighAdditionAverage, OAI.JointDickman.highNoAdditionMass, OAI.JointDickman.subsetAverage