CorrelationPhase.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.differencingPhase line 11
Source documentation
The unit complex phase with frequency one.
```
def differencingPhase (x : ℝ) : ℂ :=
…
```
theorem OAI.Problem337.differencingPhase_norm line 14
theorem OAI.Problem337.differencingPhase_sub line 17
def OAI.Problem337.intervalPhase line 26
Source documentation
A phase sequence with zero extension outside a closed integer interval.
```
def intervalPhase (f : ℝ → ℝ) (L U : ℤ) : ℤ → ℂ :=
…
```
theorem OAI.Problem337.correlationShift_intervalPhase line 29
theorem OAI.Problem337.forwardDifference_sub_input line 42
theorem OAI.Problem337.forwardDifference_translate_input line 52
theorem OAI.Problem337.forwardDifference_cons_input line 64
theorem OAI.Problem337.iteratedCorrelation_intervalPhase line 72
Source documentation
Positive iterated correlations of a truncated phase are exactly the differentiated phase on the interval shortened by the total shift.
```
theorem iteratedCorrelation_intervalPhase (hs : List ℤ) (f : ℝ → ℝ) (L U : ℤ)
    (hhs : ∀ h ∈ hs, 0 ≤ h) :
    iteratedCorrelation (intervalPhase f L U) hs =
      intervalPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ))) f) L (U - hs.sum) := by
…
```
Mentions: OAI.Problem337.iteratedCorrelation, OAI.Problem337.intervalPhase, OAI.Problem337.forwardDifference
theorem OAI.Problem337.intervalPhase_sum line 89
Source documentation
A zero-extended interval phase sums to its untruncated phase sum on any larger integer interval. Empty subintervals are included.
```
theorem intervalPhase_sum (f : ℝ → ℝ) (L U A B : ℤ)
    (hAL : A ≤ L) (hUB : U ≤ B) :
    (∑ n ∈ Finset.Icc A B, intervalPhase f L U n) =
      ∑ n ∈ Finset.Icc L U, differencingPhase (f n) := by
…
```
Mentions: OAI.Problem337.intervalPhase, OAI.Problem337.differencingPhase

theorem OAI.Problem337.iteratedCorrelation_intervalPhase_sum line 108

Source documentation

The exact terminal sum after differencing a phase supported on [1,N].

theorem iteratedCorrelation_intervalPhase_sum (hs : List ℤ) (f : ℝ → ℝ) (N : ℕ)
    (hhs : ∀ h ∈ hs, 0 ≤ h) :
    (∑ n ∈ Finset.Icc (1 : ℤ) N, iteratedCorrelation (intervalPhase f 1 N) hs n) =
      ∑ n ∈ Finset.Icc (1 : ℤ) ((N : ℤ) - hs.sum),
        differencingPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ))) f n) := by
…

Mentions: OAI.Problem337.iteratedCorrelation, OAI.Problem337.intervalPhase, OAI.Problem337.differencingPhase, OAI.Problem337.forwardDifference

theorem OAI.Problem337.interval_phase_iterated_power_bound line 120

Source documentation

Reduction of a phase sum to the untruncated forward-difference sums needed by a derivative test. All interval endpoints are explicit.

theorem interval_phase_iterated_power_bound (r N H : ℕ)
    (hH : 1 ≤ H) (hHN : H ≤ N) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1)
    (hHε : 2 / (H : ℝ) ≤ ε) (f : ℝ → ℝ)
    (hterminal : ∀ hs : List ℤ, hs.length = r →
      (∀ h ∈ hs, 0 < h ∧ h < H) →
      ‖∑ n ∈ Finset.Icc (1 : ℤ) ((N : ℤ) - hs.sum),
        differencingPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ))) f n)‖ /
          (N : ℝ) ≤ ε) :
    ‖∑ n ∈ Finset.Icc (1 : ℤ) N, differencingPhase (f n)‖ / (N : ℝ) ≤
      3 * ε ^ (1 / (2 : ℝ)^r) := by
…

Mentions: OAI.Problem337.differencingPhase, OAI.Problem337.forwardDifference

theorem OAI.Problem337.sum_integer_interval_translate line 146

Source documentation

Integer translation of a finite interval sum.

theorem sum_integer_interval_translate {M : Type*} [AddCommMonoid M]
    (f : ℤ → M) (A B t : ℤ) :
    (∑ n ∈ Finset.Icc A B, f (n + t)) =
      ∑ n ∈ Finset.Icc (A + t) (B + t), f n := by
…

theorem OAI.Problem337.phase_sum_integer_translate line 164

theorem OAI.Problem337.translated_interval_phase_power_bound line 171

Source documentation

The phase differencing bound on an arbitrary translated integer interval.

theorem translated_interval_phase_power_bound (r N H : ℕ) (L : ℤ)
    (hH : 1 ≤ H) (hHN : H ≤ N) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1)
    (hHε : 2 / (H : ℝ) ≤ ε) (f : ℝ → ℝ)
    (hterminal : ∀ hs : List ℤ, hs.length = r →
      (∀ h ∈ hs, 0 < h ∧ h < H) →
      ‖∑ n ∈ Finset.Icc L (L + (N : ℤ) - 1 - hs.sum),
        differencingPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ))) f n)‖ /
          (N : ℝ) ≤ ε) :
    ‖∑ n ∈ Finset.Icc L (L + (N : ℤ) - 1), differencingPhase (f n)‖ /
        (N : ℝ) ≤ 3 * ε ^ (1 / (2 : ℝ)^r) := by
…

Mentions: OAI.Problem337.differencingPhase, OAI.Problem337.forwardDifference

theorem OAI.Problem337.interval_phase_ambient_power_bound line 198

Source documentation

Differencing a subinterval inside a larger normalization interval. This permits N = ceil(2U) in a dyadic reciprocal-phase estimate.

theorem interval_phase_ambient_power_bound (r N H : ℕ) (L U : ℤ)
    (hL : 1 ≤ L) (hU : U ≤ N)
    (hH : 1 ≤ H) (hHN : H ≤ N) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1)
    (hHε : 2 / (H : ℝ) ≤ ε) (f : ℝ → ℝ)
    (hterminal : ∀ hs : List ℤ, hs.length = r →
      (∀ h ∈ hs, 0 < h ∧ h < H) →
      ‖∑ n ∈ Finset.Icc L (U - hs.sum),
        differencingPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ))) f n)‖ /
          (N : ℝ) ≤ ε) :
    ‖∑ n ∈ Finset.Icc L U, differencingPhase (f n)‖ / (N : ℝ) ≤
      3 * ε ^ (1 / (2 : ℝ)^r) := by
…

Mentions: OAI.Problem337.differencingPhase, OAI.Problem337.forwardDifference