DyadicChangeScales.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite dyadic decomposition by the largest changed prime

theorem OAI.JointDickman.dyadic_cover_endpoint line 14
Source documentation
One dyadic upper endpoint covers a fixed positive interval, with at most a factor-two overshoot.
```
theorem dyadic_cover_endpoint {L X : ℝ} (hL : 0 < L) (hLX : L ≤ X) :
    ∃ N : ℕ, 0 < N ∧ X ≤ (2 : ℝ)^N * L ∧ (2 : ℝ)^N * L ≤ 2 * X := by
…
```

theorem OAI.JointDickman.dyadic_shell_cover line 25

Source documentation

Every changed logarithm above the cutoff belongs to an actual dyadic shell, including equality at an upper endpoint.

theorem dyadic_shell_cover {L x : ℝ} {N : ℕ} (_hL : 0 < L) (hx : L < x)
    (hcap : x ≤ (2 : ℝ)^N * L) :
    ∃ i ∈ Icc 1 N, ((2 : ℝ)^i * L) / 2 < x ∧ x ≤ (2 : ℝ)^i * L := by
…

theorem OAI.JointDickman.dyadic_shell_unique line 48

Source documentation

No overlap occurs between distinct dyadic shells.

theorem dyadic_shell_unique {L x : ℝ} {i j : ℕ} (hL : 0 < L)
    (hi : ((2 : ℝ)^i * L) / 2 < x ∧ x ≤ (2 : ℝ)^i * L)
    (hj : ((2 : ℝ)^j * L) / 2 < x ∧ x ≤ (2 : ℝ)^j * L) : i = j := by
…