RealPhaseEnvelope.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RealPhase.integerDistance line 11
Source documentation
Distance to the nearest integer. The tie convention of round does not affect this distance.
```
def integerDistance (x : ℝ) : ℝ := |x - round x|
```
lemma OAI.Problem337.RealPhase.integerDistance_nonneg line 13
lemma OAI.Problem337.RealPhase.abs_sin_fract line 15
theorem OAI.Problem337.RealPhase.two_integerDistance_le_abs_sin line 25
Source documentation
Jordan's sine inequality in the nearest-integer convention used by Diophantine approximation and minor-arc spacing.
```
theorem two_integerDistance_le_abs_sin (x : ℝ) :
    2 * integerDistance x ≤ |Real.sin (Real.pi * x)| := by
…
```
Mentions: OAI.Problem337.RealPhase.integerDistance
def OAI.Problem337.RealPhase.phase line 46
Source documentation
Period-one complex phase, with the same normalization as the standard cyclic character and the circle-method Fourier sum.
```
def phase (x : ℝ) : ℂ := Complex.exp (Complex.I * (2 * Real.pi * x : ℝ))
```
lemma OAI.Problem337.RealPhase.norm_phase line 48
lemma OAI.Problem337.RealPhase.phase_add line 51
lemma OAI.Problem337.RealPhase.phase_nat_mul line 58
def OAI.Problem337.RealPhase.envelope line 66
Source documentation
A capped geometric envelope with the integer frequencies accounted for explicitly, rather than assigning an invalid reciprocal at distance zero.
```
def envelope (N : ℕ) (x : ℝ) : ℝ :=
…
```
theorem OAI.Problem337.RealPhase.norm_sum_phase_le_envelope line 69
theorem OAI.Problem337.RealPhase.norm_sum_shift_phase_eq line 89
Source documentation
Translating the integer interval and adding a constant phase preserve the norm, so the same envelope handles every interval location.
```
theorem norm_sum_shift_phase_eq (x β t : ℝ) (N : ℕ) :
    ‖∑ n ∈ Finset.range N, phase (x * (t + n) + β)‖ =
      ‖∑ n ∈ Finset.range N, phase ((n : ℝ) * x)‖ := by
…
```
Mentions: OAI.Problem337.RealPhase.phase
theorem OAI.Problem337.RealPhase.norm_sum_shift_phase_le_envelope line 101