OAI/NumberTheory/Ostmann/Preliminaries/PhaseDistance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.realAdditivePhase_intCast line 12
2. theorem OAI.Ostmann.realAdditivePhase_sub_int line 19
3. theorem OAI.Ostmann.norm_realAdditivePhase_sub_one line 24
4. theorem OAI.Ostmann.round_distance_le_phase_norm line 31
5. theorem OAI.Ostmann.linear_phase_sum_bound line 46
6. theorem OAI.Ostmann.linear_phase_sum_distance_bound line 66

   Source documentation

   The multiplicative form remains valid at integral phases, so no division by zero or exceptional phase needs to enter the packing argument.

   theorem linear_phase_sum_distance_bound (x : ℝ) (N : ℕ) :
       ‖∑ j ∈ Finset.range N, realAdditivePhase x ^ j‖ ≤ N ∧
         2 * |x - (round x : ℤ)| *
           ‖∑ j ∈ Finset.range N, realAdditivePhase x ^ j‖ ≤ 1 := by
   …

   Mentions: OAI.Ostmann.realAdditivePhase