SequenceNorms.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of finite sequence norms and the small-remainder estimate.

theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_rpow_le_rpow_sum line 16
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_powers_exponent_comparison line 32
def OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm line 44
Source documentation
A sequence norm is written as a real power of its finite power sum.
```
def sequenceNorm (a : ι → ℂ) (r : ℝ) : ℝ := (∑ i, ‖a i‖ ^ r) ^ (1 / r)
```
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm_nonneg line 46
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm_rpow line 49
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm_mono line 57
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_squares_le_sequenceNorm_sq line 69
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm_fourth_le_mass_cube line 76
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm_le_one_div_sixtyfour line 86
Source documentation
The exact numerical smallness needed for the dominant coefficient case.
```
theorem sequenceNorm_le_one_div_sixtyfour (a : ι → ℂ) {r : ℝ}
    (hr : 4 / 3 ≤ r) (hsmall : ∑ i, coefficientMass a i ≤ 1 / 1023) :
    sequenceNorm a r ≤ 1 / 64 := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.coefficientMass, OAI.LipschitzHilbert.PhaseCombinatorics.sequenceNorm