DivisorSquareMean.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

An elementary mean-square bound for the divisor function

The pointwise majorant tau^2 ≤ zeta^4 and the elementary harmonic-sum bound supply the coefficient energy used in finite Type-II estimates.

lemma OAI.Problem337.DivisorSquareMean.square_le_sigma_convolution_prime_pow line 18
theorem OAI.Problem337.DivisorSquareMean.card_divisors_sq_le_convolution line 33
theorem OAI.Problem337.DivisorSquareMean.card_divisors_sq_le_zeta_four line 47
lemma OAI.Problem337.DivisorSquareMean.real_harmonic_eq_sum line 56
lemma OAI.Problem337.DivisorSquareMean.real_harmonic_nonneg line 64
lemma OAI.Problem337.DivisorSquareMean.real_harmonic_mono line 68
theorem OAI.Problem337.DivisorSquareMean.sum_zeta_pow_le_harmonic line 75
Source documentation
The summatory (k+1)-fold divisor function costs at most k harmonic factors.
```
theorem sum_zeta_pow_le_harmonic (k N : ℕ) :
    (∑ n ∈ Ioc 0 N, (ζ ^ (k + 1)) n : ℕ) ≤
      (N : ℝ) * (harmonic N : ℝ) ^ k := by
…
```
theorem OAI.Problem337.DivisorSquareMean.sum_card_divisors_sq_le_harmonic line 104
Source documentation
Sharp elementary harmonic form of the divisor mean-square bound.
```
theorem sum_card_divisors_sq_le_harmonic (N : ℕ) :
    (∑ n ∈ Ioc 0 N, (n.divisors.card : ℝ) ^ 2) ≤
      (N : ℝ) * (harmonic N : ℝ) ^ 3 := by
…
```
theorem OAI.Problem337.DivisorSquareMean.sum_card_divisors_sq_le_log line 122
Source documentation
The classical elementary N (1 + log N)^3 divisor mean square, including N = 0.
```
theorem sum_card_divisors_sq_le_log (N : ℕ) :
    (∑ n ∈ Ioc 0 N, (n.divisors.card : ℝ) ^ 2) ≤
      (N : ℝ) * (1 + Real.log N) ^ 3 := by
…
```

theorem OAI.Problem337.DivisorSquareMean.sum_norm_sq_le_log line 131

Source documentation

Coefficient energy for any divisor-bounded sequence in a seminormed group.

theorem sum_norm_sq_le_log {E : Type*} [SeminormedAddCommGroup E]
    (b : ℕ → E) (N : ℕ)
    (hb : ∀ n ∈ Ioc 0 N, ‖b n‖ ≤ (n.divisors.card : ℝ)) :
    (∑ n ∈ Ioc 0 N, ‖b n‖ ^ 2) ≤ (N : ℝ) * (1 + Real.log N) ^ 3 := by
…

theorem OAI.Problem337.DivisorSquareMean.sum_norm_sq_le_log_of_subset line 139

Source documentation

A finite subinterval/subset version, allowing a uniform coefficient multiplier.

theorem sum_norm_sq_le_log_of_subset {E : Type*} [SeminormedAddCommGroup E]
    (b : ℕ → E) (T : Finset ℕ) (N : ℕ) (B : ℝ)
    (hT : T ⊆ Ioc 0 N)
    (hb : ∀ n ∈ T, ‖b n‖ ≤ B * (n.divisors.card : ℝ)) :
    (∑ n ∈ T, ‖b n‖ ^ 2) ≤ B ^ 2 * ((N : ℝ) * (1 + Real.log N) ^ 3) := by
…