OAI/NumberTheory/Ostmann/Construction/InitialAtomGuards.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.initial_atom_units_iff line 12
2. theorem OAI.Ostmann.initial_atom_pairwise line 22
3. theorem OAI.Ostmann.fullAtomTransferWeight_initial line 36
4. theorem OAI.Ostmann.initial_atom_total line 57
5. theorem OAI.Ostmann.normalizedFourierProfile_even_original line 68

   Source documentation

   The chosen even cutoff makes the negative recursive Fourier convention identical to the original positive-frequency Poisson convention.

   theorem normalizedFourierProfile_even_original (ψ : ℝ → ℂ)
       (heven : ∀ t, ψ (-t) = ψ t) (X M v : ℝ) (hX : X ≠ 0) (hM : M ≠ 0) :
       normalizedFourierProfile ψ v (M / X) =
         (Real.sqrt (X / M) : ℂ) * ψ (v * X / M) := by
   …

   Mentions: OAI.Ostmann.normalizedFourierProfile