WeightedPhaseExtraction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Extracting an unweighted interval sum from a weighted phase

def OAI.Ostmann.discreteVariation line 12
theorem OAI.Ostmann.weighted_sum_le_variation line 17
Source documentation
Finite Abel summation bounds a weighted sum by the largest prefix sum and the endpoint-plus-variation of the actual weights.
```
theorem weighted_sum_le_variation (w f : ℕ → ℂ) (N : ℕ) (M : ℝ)
    (hprefix : ∀ n ≤ N, ‖∑ j ∈ Finset.range n, f j‖ ≤ M) :
    ‖∑ j ∈ Finset.range N, w j * f j‖ ≤ discreteVariation w N * M := by
…
```
Mentions: OAI.Ostmann.discreteVariation

theorem OAI.Ostmann.exists_large_prefix_of_weighted_sum line 43

Source documentation

A large weighted sum therefore supplies a nonempty unweighted prefix. For a translated interval the same statement applies after reindexing.

theorem exists_large_prefix_of_weighted_sum (w f : ℕ → ℂ) (N : ℕ) (R : ℝ)
    (hR : 0 < R)
    (hlarge : discreteVariation w N * R < ‖∑ j ∈ Finset.range N, w j * f j‖) :
    ∃ n : ℕ, 0 < n ∧ n ≤ N ∧ R < ‖∑ j ∈ Finset.range n, f j‖ := by
…

Mentions: OAI.Ostmann.discreteVariation