IteratedDifferencing.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.correlationShift line 10
Source documentation
A single multiplicative difference of a complex sequence.
```
def correlationShift (a : ℤ → ℂ) (h : ℤ) : ℤ → ℂ :=
…
```
def OAI.Problem337.iteratedCorrelation line 14
Source documentation
Successive multiplicative differences, in their order of application.
```
def iteratedCorrelation (a : ℤ → ℂ) : List ℤ → ℤ → ℂ
  | [] => a
  | h :: hs => iteratedCorrelation (correlationShift a h) hs
```
Mentions: OAI.Problem337.correlationShift
theorem OAI.Problem337.correlationShift_supported line 18
theorem OAI.Problem337.correlationShift_norm_le_one line 24

def OAI.Problem337.differencingBudget line 33

Source documentation

The elementary square-root budget obtained from repeated differencing.

def differencingBudget (H : ℕ) : ℕ → ℝ → ℝ
  | 0, B => B
  | r + 1, B => Real.sqrt (2 / (H : ℝ) + 2 * differencingBudget H r B)

theorem OAI.Problem337.differencingBudget_nonneg line 37

theorem OAI.Problem337.iterated_differencing_bound line 45

Source documentation

If every terminal r-fold correlation is small, the original sum is bounded by the iterated van der Corput square-root budget.

theorem iterated_differencing_bound (r : ℕ) (N H : ℕ)
    (hH : 1 ≤ H) (hHN : H ≤ N) (B : ℝ) (hB : 0 ≤ B)
    (a : ℤ → ℂ)
    (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0)
    (hnorm : ∀ n : ℤ, ‖a n‖ ≤ 1)
    (hterminal : ∀ hs : List ℤ, hs.length = r →
      (∀ h ∈ hs, 0 < h ∧ h < H) →
      ‖∑ n ∈ Finset.Icc (1 : ℤ) N, iteratedCorrelation a hs n‖ / (N : ℝ) ≤ B) :
    ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a n‖ / (N : ℝ) ≤ differencingBudget H r B := by
…

Mentions: OAI.Problem337.iteratedCorrelation, OAI.Problem337.differencingBudget

theorem OAI.Problem337.differencingBudget_le_rpow line 82
Source documentation
A uniform bound for the square-root budget. Its constant does not grow with the number of differencing steps.
```
theorem differencingBudget_le_rpow (H r : ℕ) {ε B : ℝ}
    (hε : 0 < ε) (hε1 : ε ≤ 1) (hHB : 2 / (H : ℝ) ≤ ε)
    (hB : B ≤ ε) :
    differencingBudget H r B ≤ 3 * ε ^ (1 / (2 : ℝ)^r) := by
…
```
Mentions: OAI.Problem337.differencingBudget

theorem OAI.Problem337.iterated_differencing_power_bound line 112

Source documentation

Power-saving form of iterated van der Corput differencing.

theorem iterated_differencing_power_bound (r : ℕ) (N H : ℕ)
    (hH : 1 ≤ H) (hHN : H ≤ N) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1)
    (hHε : 2 / (H : ℝ) ≤ ε) (a : ℤ → ℂ)
    (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0)
    (hnorm : ∀ n : ℤ, ‖a n‖ ≤ 1)
    (hterminal : ∀ hs : List ℤ, hs.length = r →
      (∀ h ∈ hs, 0 < h ∧ h < H) →
      ‖∑ n ∈ Finset.Icc (1 : ℤ) N, iteratedCorrelation a hs n‖ / (N : ℝ) ≤ ε) :
    ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a n‖ / (N : ℝ) ≤
      3 * ε ^ (1 / (2 : ℝ)^r) :=
…

Mentions: OAI.Problem337.iteratedCorrelation