OAI/NumberTheory/JointDickman/Analysis/CanonicalMellinBands.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.canonicalMellinBands line 12
2. lemma OAI.JointDickman.canonical_resolution_ge_two line 22
3. lemma OAI.JointDickman.canonical_band_lower_ge line 30
4. theorem OAI.JointDickman.canonicalMellinBands_valid line 37

   Source documentation

   The entire finite family satisfies the geometric hypotheses of the proved Ramaré partition as soon as its upper endpoints lie below N/2.

   theorem canonicalMellinBands_valid {P Q η : ℝ} {J N : ℕ}
       (hP : 2 * Real.exp 1 ≤ P) (hPQ : P ≤ Q)
       (hlogP : 1 < Real.log P) (hH : 2 ≤ mrtBaseResolution P Q η)
       (hN : ∀ j ∈ range J, 2 * mrtBandUpper Q (j+1) ≤ N) :
       (canonicalMellinBands P Q η).Valid J N := by
   …

   Mentions: OAI.JointDickman.canonicalMellinBands

5. theorem OAI.JointDickman.canonical_initialCost_le line 96
6. lemma OAI.JointDickman.canonical_laterCost_eq line 106
7. theorem OAI.JointDickman.canonical_laterCost_le line 121