OAI/NumberTheory/Ostmann/Characters/FourierWindowDecay.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.normalizedFourierProfile_norm_window line 10
2. theorem OAI.Ostmann.fourierPolynomialFactor_norm_window line 24
3. theorem OAI.Ostmann.realValueFourierWeight_norm_window line 32
4. theorem OAI.Ostmann.realValueNodeCutoff_norm_bound line 49
5. theorem OAI.Ostmann.realValueKernel_norm_window line 73
6. theorem OAI.Ostmann.realValueKernelPair_norm_window line 89
7. theorem OAI.Ostmann.fourier_window_pair_exp line 101

   Source documentation

   Exact exponential decay of the paired Fourier window budget.

   theorem fourier_window_pair_exp (ψ : 𝓢(ℝ, ℂ)) (n : ℕ) (B Δ : ℝ) :
       ((SchwartzMap.seminorm ℝ 0 0 ψ / Real.sqrt (Real.exp Δ)) ^ (2 ^ n) *
         B ^ (2 ^ n - 1)) ^ 2 =
         ((SchwartzMap.seminorm ℝ 0 0 ψ) ^ (2 ^ n) * B ^ (2 ^ n - 1)) ^ 2 *
           Real.exp (-(2 ^ n : ℕ) * Δ) := by
   …

8. theorem OAI.Ostmann.realValueKernelPair_norm_exp line 113