DyadicBands.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.DyadicBands.InBand line 10
Source documentation
A half-open band on a multiplicative dyadic scale.
```
def InBand (a : ℝ) (j : ℕ) (x : ℝ) : Prop :=
…
```
instance OAI.Problem337.DyadicBands.(instance at line 13) line 13
def OAI.Problem337.DyadicBands.bandCount line 18
Source documentation
Number of dyadic bands needed to cover [a,B].
```
def bandCount (a B : ℝ) : ℕ :=
…
```
lemma OAI.Problem337.DyadicBands.exists_band line 21
lemma OAI.Problem337.DyadicBands.bandCount_le line 39
theorem OAI.Problem337.DyadicBands.sum_le_bandCount_mul line 52
Source documentation
A uniform bound on the weight in each dyadic band bounds the total weight. This only uses coverage, so it is applicable without any injectivity assumption on the scale attached to each element.
```
theorem sum_le_bandCount_mul {ι : Type*} (s : Finset ι)
    (x w : ι → ℝ) {a B A : ℝ} (ha : 0 < a)
    (hrange : ∀ i ∈ s, a ≤ x i ∧ x i ≤ B)
    (hw : ∀ i ∈ s, 0 ≤ w i)
    (hband : ∀ j < bandCount a B,
      (∑ i ∈ s with InBand a j (x i), w i) ≤ A) :
    (∑ i ∈ s, w i) ≤ (bandCount a B : ℝ) * A := by
…
```
Mentions: OAI.Problem337.DyadicBands.bandCount, OAI.Problem337.DyadicBands.InBand

theorem OAI.Problem337.DyadicBands.sum_le_log_budget line 87

Source documentation

Real-valued logarithmic budget for a dyadic partition.

theorem sum_le_log_budget {ι : Type*} (s : Finset ι)
    (x w : ι → ℝ) {a B A : ℝ} (ha : 0 < a) (haB : a ≤ B) (hA : 0 ≤ A)
    (hrange : ∀ i ∈ s, a ≤ x i ∧ x i ≤ B)
    (hw : ∀ i ∈ s, 0 ≤ w i)
    (hband : ∀ j < bandCount a B,
      (∑ i ∈ s with InBand a j (x i), w i) ≤ A) :
    (∑ i ∈ s, w i) ≤ (1 + Real.log (B / a) / Real.log 2) * A := by
…

Mentions: OAI.Problem337.DyadicBands.bandCount, OAI.Problem337.DyadicBands.InBand

lemma OAI.Problem337.DyadicBands.bandCount_le_log line 98
Source documentation
If the entire scale lies below S², only O(log S) bands are needed.
```
lemma bandCount_le_log {a B S : ℝ} (ha : 1 ≤ a) (haB : a ≤ B)
    (hS : 2 ≤ S) (hB : B ≤ S ^ 2) :
    (bandCount a B : ℝ) ≤ (3 / Real.log 2) * Real.log S := by
…
```
Mentions: OAI.Problem337.DyadicBands.bandCount

theorem OAI.Problem337.DyadicBands.sum_le_logS_budget line 126

Source documentation

The uniform intermediate-band contribution has logarithmic total loss.

theorem sum_le_logS_budget {ι : Type*} (s : Finset ι)
    (x w : ι → ℝ) {a B S A : ℝ}
    (ha : 1 ≤ a) (haB : a ≤ B) (hS : 2 ≤ S) (hB : B ≤ S ^ 2)
    (hA : 0 ≤ A) (hrange : ∀ i ∈ s, a ≤ x i ∧ x i ≤ B)
    (hw : ∀ i ∈ s, 0 ≤ w i)
    (hband : ∀ j < bandCount a B,
      (∑ i ∈ s with InBand a j (x i), w i) ≤ A) :
    (∑ i ∈ s, w i) ≤ (3 / Real.log 2) * Real.log S * A := by
…

Mentions: OAI.Problem337.DyadicBands.bandCount, OAI.Problem337.DyadicBands.InBand

theorem OAI.Problem337.DyadicBands.eventually_divisor_band_cover line 139

Source documentation

The precise dyadic cover used for the intermediate-prime range in the uniform divisor moment. The constant is absolute; the threshold depends on D.

theorem eventually_divisor_band_cover (D : ℝ) :
    ∀ᶠ S : ℝ in Filter.atTop, ∀ v : ℝ,
      S / (2 * Real.log S) ≤ v → v ≤ D * S →
      4 * Real.log S ≤ v ^ (15 / 16 : ℝ) →
      ∃ J : ℕ, (J : ℝ) ≤ (3 / Real.log 2) * Real.log S ∧
        ∀ w : ℝ, 4 * Real.log S ≤ w → w < v ^ (15 / 16 : ℝ) →
          ∃ j : ℕ, j < J ∧ InBand (4 * Real.log S) j w := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.v, OAI.Problem337.DyadicBands.InBand