SequenceExponents.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional exponent comparison used in the Fourier gain.

theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_power_exponent_comparison line 19
Source documentation
Raising the finite mean inequality gives the exact fourth-moment cost of changing the coefficient exponent from 4/3 to r.
```
theorem fourth_power_exponent_comparison (a : ι → ℂ) {r : ℝ}
    (hr : 4 / 3 ≤ r) :
    (∑ i, coefficientMass a i) ^ 3 ≤
      (Fintype.card ι : ℝ) ^ (3 - 4 / r) * (∑ i, ‖a i‖ ^ r) ^ (4 / r) := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.coefficientMass
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_power_exponent_comparison_bound line 43
theorem OAI.LipschitzHilbert.PhaseCombinatorics.dimension_cost_le_exp line 56
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_exponent_parameters line 68
theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourth_power_exponent_comparison_exp line 77
def OAI.LipschitzHilbert.PhaseCombinatorics.phaseConstant line 92
Source documentation
The manuscript's absolute phase constant 2⁻⁶⁰.
```
def phaseConstant : ℝ := 1 / 1152921504606846976
```
def OAI.LipschitzHilbert.PhaseCombinatorics.atomThreshold line 95
Source documentation
The manuscript's threshold 2⁻¹⁰ for a dominant coefficient.
```
def atomThreshold : ℝ := 1 / 1024
…
```
theorem OAI.LipschitzHilbert.PhaseCombinatorics.phaseConstant_pos line 98
theorem OAI.LipschitzHilbert.PhaseCombinatorics.atomThreshold_range line 101
theorem OAI.LipschitzHilbert.PhaseCombinatorics.phaseConstant_le_gap line 105
theorem OAI.LipschitzHilbert.PhaseCombinatorics.phaseParameter_range line 109
theorem OAI.LipschitzHilbert.PhaseCombinatorics.deficit_absorbs_exponential line 124
theorem OAI.LipschitzHilbert.PhaseCombinatorics.phaseConstant_exp_le_two line 134