OAI/NumberTheory/JointDickman/Analysis/LogPhaseScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.logarithmic_phase_order line 10

   Source documentation

   Choose a bounded derivative order placing the logarithmic phase in the second-derivative scale after differencing.

   theorem logarithmic_phase_order {U Z B : ℝ} (hU : 1 < U) (_hB : 1/2 ≤ B)
       (hlower : U ^ (1/2:ℝ) ≤ |Z|) (hupper : |Z| ≤ U ^ B) :
       ∃ k : ℕ, 1 ≤ k ∧ k ≤ Nat.ceil B + 1 ∧
         U ^ (-(3 : ℝ) / 2) ≤ |Z| * U ^ (-((k : ℝ) + 1)) ∧
         |Z| * U ^ (-((k : ℝ) + 1)) ≤ U ^ (-(1 : ℝ) / 2) := by
   …

2. theorem OAI.JointDickman.logarithmic_shift_product line 48

   Source documentation

   The product of a bounded number of short shifts costs at most U^(1/10).

   theorem logarithmic_shift_product {U : ℝ} (hU : 1 < U) {k : ℕ} (hk : 1 ≤ k)
       (hs : List ℝ) (hlen : hs.length ≤ k)
       (hhs : ∀ h ∈ hs, 1 ≤ h ∧ h ≤ U ^ (1 / (10 * (k : ℝ)))) :
       1 ≤ hs.prod ∧ hs.prod ≤ U ^ ((1 : ℝ) / 10) := by
   …

3. theorem OAI.JointDickman.logarithmic_phase_shift_scale line 70

   Source documentation

   The derivative scale after the short shifts is uniformly a small negative power.

   theorem logarithmic_phase_shift_scale {U Z : ℝ} (hU : 1 < U) {k : ℕ} (hk : 1 ≤ k)
       (hlower : U ^ (-(3 : ℝ) / 2) ≤ |Z| * U ^ (-((k : ℝ) + 1)))
       (hupper : |Z| * U ^ (-((k : ℝ) + 1)) ≤ U ^ (-(1 : ℝ) / 2))
       (hs : List ℝ) (hlen : hs.length ≤ k)
       (hhs : ∀ h ∈ hs, 1 ≤ h ∧ h ≤ U ^ (1 / (10 * (k : ℝ)))) :
       U ^ (-(3 : ℝ) / 2) ≤ |Z| * U ^ (-((k : ℝ) + 1)) * hs.prod ∧
       |Z| * U ^ (-((k : ℝ) + 1)) * hs.prod ≤ U ^ (-(2 : ℝ) / 5) := by
   …